%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n009.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:18:56 PM UTC 2026
% Result : Unsatisfiable 11.19s 2.64s
% Output : Refutation 12.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 63
% Syntax : Number of formulae : 259 ( 159 unt; 18 def)
% Number of atoms : 387 ( 230 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 326 ( 198 ~; 110 |; 0 &)
% ( 18 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 20 ( 18 usr; 19 prp; 0-2 aty)
% Number of functors : 48 ( 48 usr; 45 con; 0-3 aty)
% Number of variables : 33 ( 0 sgn 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(f632,plain,
elem_38 = select(earray_66,elem_37),
inference(superposition,[],[f1,f631]) ).
fof(f691,plain,
! [X0] :
( select(a,X0) = select(earray_42,X0)
| elem_34 = X0 ),
inference(superposition,[],[f2,f560]) ).
fof(f695,plain,
! [X0] :
( select(earray_42,X0) = select(earray_44,X0)
| elem_31 = X0 ),
inference(superposition,[],[f2,f561]) ).
fof(f696,plain,
! [X0] :
( select(earray_44,X0) = select(earray_46,X0)
| elem_28 = X0 ),
inference(superposition,[],[f2,f562]) ).
fof(f697,plain,
! [X0] :
( select(earray_46,X0) = select(earray_48,X0)
| elem_25 = X0 ),
inference(superposition,[],[f2,f563]) ).
fof(f698,plain,
! [X0] :
( select(earray_48,X0) = select(earray_50,X0)
| elem_22 = X0 ),
inference(superposition,[],[f2,f564]) ).
fof(f699,plain,
! [X0] :
( select(earray_50,X0) = select(earray_52,X0)
| elem_19 = X0 ),
inference(superposition,[],[f2,f565]) ).
fof(f700,plain,
! [X0] :
( select(earray_52,X0) = select(earray_54,X0)
| elem_16 = X0 ),
inference(superposition,[],[f2,f566]) ).
fof(f701,plain,
! [X0] :
( select(earray_54,X0) = select(earray_56,X0)
| elem_13 = X0 ),
inference(superposition,[],[f2,f567]) ).
fof(f702,plain,
! [X0] :
( select(earray_56,X0) = select(earray_58,X0)
| elem_10 = X0 ),
inference(superposition,[],[f2,f568]) ).
fof(f703,plain,
! [X0] :
( select(earray_58,X0) = select(earray_60,X0)
| elem_7 = X0 ),
inference(superposition,[],[f2,f570]) ).
fof(f705,plain,
! [X0] :
( select(earray_60,X0) = select(earray_62,X0)
| elem_4 = X0 ),
inference(superposition,[],[f2,f571]) ).
fof(f706,plain,
! [X0] :
( select(earray_62,X0) = select(earray_64,X0)
| elem_0 = X0 ),
inference(superposition,[],[f2,f572]) ).
fof(f707,plain,
! [X0] :
( select(earray_66,X0) = select(earray_64,X0)
| i = X0 ),
inference(superposition,[],[f2,f573]) ).
fof(f724,plain,
( elem_38 = select(earray_64,elem_37)
| elem_37 = i ),
inference(superposition,[],[f707,f632]) ).
fof(f729,definition,
( spl0_1
<=> elem_37 = i ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f733,definition,
( spl0_2
<=> elem_38 = select(earray_64,elem_37) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f735,plain,
( elem_38 = select(earray_64,elem_37)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f737,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f724,f733,f729]) ).
fof(f744,plain,
elem_34 != elem_37,
inference(superposition,[],[f548,f596]) ).
fof(f749,plain,
i != s(s(s(s(s(s(s(s(s(s(s(s(elem_0)))))))))))),
inference(superposition,[],[f536,f575]) ).
fof(f773,plain,
i != s(s(s(s(s(s(s(s(s(s(s(elem_4))))))))))),
inference(forward_demodulation,[],[f749,f598]) ).
fof(f784,plain,
i != s(s(s(s(s(s(s(s(s(s(elem_7)))))))))),
inference(forward_demodulation,[],[f773,f627]) ).
fof(f794,plain,
i != s(s(s(s(s(s(s(s(s(elem_10))))))))),
inference(forward_demodulation,[],[f784,f577]) ).
fof(f803,plain,
i != s(s(s(s(s(s(s(s(elem_13)))))))),
inference(forward_demodulation,[],[f794,f579]) ).
fof(f811,plain,
i != s(s(s(s(s(s(s(elem_16))))))),
inference(forward_demodulation,[],[f803,f581]) ).
fof(f818,plain,
i != s(s(s(s(s(s(elem_19)))))),
inference(forward_demodulation,[],[f811,f583]) ).
fof(f824,plain,
i != s(s(s(s(s(elem_22))))),
inference(forward_demodulation,[],[f818,f586]) ).
fof(f829,plain,
i != s(s(s(s(elem_25)))),
inference(forward_demodulation,[],[f824,f588]) ).
fof(f833,plain,
i != s(s(s(elem_28))),
inference(forward_demodulation,[],[f829,f590]) ).
fof(f836,plain,
i != s(s(elem_31)),
inference(forward_demodulation,[],[f833,f592]) ).
fof(f838,plain,
i != s(elem_34),
inference(forward_demodulation,[],[f836,f594]) ).
fof(f839,plain,
elem_37 != i,
inference(forward_demodulation,[],[f838,f596]) ).
fof(f840,plain,
~ spl0_1,
inference(avatar_split_clause,[],[f839,f729]) ).
fof(f883,plain,
( elem_38 = select(earray_62,elem_37)
| elem_0 = elem_37
| ~ spl0_2 ),
inference(superposition,[],[f735,f706]) ).
fof(f886,definition,
( spl0_3
<=> elem_0 = elem_37 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f890,definition,
( spl0_4
<=> elem_38 = select(earray_62,elem_37) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f892,plain,
( elem_38 = select(earray_62,elem_37)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f890]) ).
fof(f894,plain,
( spl0_3
| spl0_4
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f883,f733,f890,f886]) ).
fof(f895,plain,
( elem_38 = select(earray_60,elem_37)
| elem_37 = elem_4
| ~ spl0_4 ),
inference(superposition,[],[f892,f705]) ).
fof(f898,definition,
( spl0_5
<=> elem_37 = elem_4 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f900,plain,
( elem_37 = elem_4
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f898]) ).
fof(f902,definition,
( spl0_6
<=> elem_38 = select(earray_60,elem_37) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f904,plain,
( elem_38 = select(earray_60,elem_37)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f902]) ).
fof(f906,plain,
( spl0_5
| spl0_6
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f895,f890,f902,f898]) ).
fof(f915,plain,
elem_10 != s(s(s(s(s(s(s(s(s(s(elem_13)))))))))),
inference(superposition,[],[f538,f579]) ).
fof(f917,plain,
elem_10 != s(s(s(s(s(s(s(s(elem_13)))))))),
inference(superposition,[],[f540,f579]) ).
fof(f933,plain,
elem_10 != s(s(s(s(s(s(s(elem_16))))))),
inference(forward_demodulation,[],[f917,f581]) ).
fof(f935,plain,
elem_10 != s(s(s(s(s(s(s(s(s(elem_16))))))))),
inference(forward_demodulation,[],[f915,f581]) ).
fof(f944,plain,
elem_10 != s(s(s(s(s(s(elem_19)))))),
inference(forward_demodulation,[],[f933,f583]) ).
fof(f946,plain,
elem_10 != s(s(s(s(s(s(s(s(elem_19)))))))),
inference(forward_demodulation,[],[f935,f583]) ).
fof(f954,plain,
elem_10 != s(s(s(s(s(elem_22))))),
inference(forward_demodulation,[],[f944,f586]) ).
fof(f956,plain,
elem_10 != s(s(s(s(s(s(s(elem_22))))))),
inference(forward_demodulation,[],[f946,f586]) ).
fof(f963,plain,
elem_10 != s(s(s(s(elem_25)))),
inference(forward_demodulation,[],[f954,f588]) ).
fof(f965,plain,
elem_10 != s(s(s(s(s(s(elem_25)))))),
inference(forward_demodulation,[],[f956,f588]) ).
fof(f971,plain,
elem_10 != s(s(s(elem_28))),
inference(forward_demodulation,[],[f963,f590]) ).
fof(f973,plain,
elem_10 != s(s(s(s(s(elem_28))))),
inference(forward_demodulation,[],[f965,f590]) ).
fof(f978,plain,
elem_10 != s(s(elem_31)),
inference(forward_demodulation,[],[f971,f592]) ).
fof(f980,plain,
elem_10 != s(s(s(s(elem_31)))),
inference(forward_demodulation,[],[f973,f592]) ).
fof(f984,plain,
elem_10 != s(elem_34),
inference(forward_demodulation,[],[f978,f594]) ).
fof(f986,plain,
elem_10 != s(s(s(elem_34))),
inference(forward_demodulation,[],[f980,f594]) ).
fof(f989,plain,
elem_10 != elem_37,
inference(forward_demodulation,[],[f984,f596]) ).
fof(f991,plain,
elem_10 != s(s(elem_37)),
inference(forward_demodulation,[],[f986,f596]) ).
fof(f996,plain,
( elem_10 != s(s(elem_4))
| ~ spl0_5 ),
inference(forward_demodulation,[],[f991,f900]) ).
fof(f1000,plain,
( elem_10 != s(elem_7)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f996,f627]) ).
fof(f1003,plain,
( $false
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f1000,f577]) ).
fof(f1004,plain,
~ spl0_5,
inference(avatar_contradiction_clause,[],[f1003]) ).
fof(f1007,plain,
( elem_38 = select(earray_58,elem_37)
| elem_37 = elem_7
| ~ spl0_6 ),
inference(superposition,[],[f904,f703]) ).
fof(f1010,definition,
( spl0_7
<=> elem_37 = elem_7 ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f1012,plain,
( elem_37 = elem_7
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f1010]) ).
fof(f1014,definition,
( spl0_8
<=> elem_38 = select(earray_58,elem_37) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f1016,plain,
( elem_38 = select(earray_58,elem_37)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f1014]) ).
fof(f1018,plain,
( spl0_7
| spl0_8
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f1007,f902,f1014,f1010]) ).
fof(f1037,plain,
elem_22 != s(s(s(s(s(s(s(s(s(elem_25))))))))),
inference(superposition,[],[f539,f588]) ).
fof(f1042,plain,
elem_22 != s(s(s(s(elem_25)))),
inference(superposition,[],[f544,f588]) ).
fof(f1050,plain,
elem_22 != s(s(s(elem_28))),
inference(forward_demodulation,[],[f1042,f590]) ).
fof(f1055,plain,
elem_22 != s(s(s(s(s(s(s(s(elem_28)))))))),
inference(forward_demodulation,[],[f1037,f590]) ).
fof(f1061,plain,
elem_22 != s(s(elem_31)),
inference(forward_demodulation,[],[f1050,f592]) ).
fof(f1066,plain,
elem_22 != s(s(s(s(s(s(s(elem_31))))))),
inference(forward_demodulation,[],[f1055,f592]) ).
fof(f1071,plain,
elem_22 != s(elem_34),
inference(forward_demodulation,[],[f1061,f594]) ).
fof(f1076,plain,
elem_22 != s(s(s(s(s(s(elem_34)))))),
inference(forward_demodulation,[],[f1066,f594]) ).
fof(f1080,plain,
elem_22 != elem_37,
inference(forward_demodulation,[],[f1071,f596]) ).
fof(f1085,plain,
elem_22 != s(s(s(s(s(elem_37))))),
inference(forward_demodulation,[],[f1076,f596]) ).
fof(f1094,plain,
( elem_22 != s(s(s(s(s(elem_7)))))
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1085,f1012]) ).
fof(f1102,plain,
( elem_22 != s(s(s(s(elem_10))))
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1094,f577]) ).
fof(f1109,plain,
( elem_22 != s(s(s(elem_13)))
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1102,f579]) ).
fof(f1115,plain,
( elem_22 != s(s(elem_16))
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1109,f581]) ).
fof(f1120,plain,
( elem_22 != s(elem_19)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1115,f583]) ).
fof(f1124,plain,
( $false
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1120,f586]) ).
fof(f1125,plain,
~ spl0_7,
inference(avatar_contradiction_clause,[],[f1124]) ).
fof(f1130,plain,
( elem_38 = select(earray_56,elem_37)
| elem_10 = elem_37
| ~ spl0_8 ),
inference(superposition,[],[f702,f1016]) ).
fof(f1131,plain,
( elem_38 = select(earray_56,elem_37)
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f1130,f989]) ).
fof(f1133,plain,
( elem_38 = select(earray_54,elem_37)
| elem_13 = elem_37
| ~ spl0_8 ),
inference(superposition,[],[f1131,f701]) ).
fof(f1136,definition,
( spl0_9
<=> elem_13 = elem_37 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f1138,plain,
( elem_13 = elem_37
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f1136]) ).
fof(f1140,definition,
( spl0_10
<=> elem_38 = select(earray_54,elem_37) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f1142,plain,
( elem_38 = select(earray_54,elem_37)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f1140]) ).
fof(f1144,plain,
( spl0_9
| spl0_10
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f1133,f1014,f1140,f1136]) ).
fof(f1159,plain,
elem_13 != s(s(s(s(s(s(s(elem_16))))))),
inference(superposition,[],[f541,f581]) ).
fof(f1173,plain,
elem_13 != s(s(s(s(s(s(elem_19)))))),
inference(forward_demodulation,[],[f1159,f583]) ).
fof(f1184,plain,
elem_13 != s(s(s(s(s(elem_22))))),
inference(forward_demodulation,[],[f1173,f586]) ).
fof(f1194,plain,
elem_13 != s(s(s(s(elem_25)))),
inference(forward_demodulation,[],[f1184,f588]) ).
fof(f1203,plain,
elem_13 != s(s(s(elem_28))),
inference(forward_demodulation,[],[f1194,f590]) ).
fof(f1211,plain,
elem_13 != s(s(elem_31)),
inference(forward_demodulation,[],[f1203,f592]) ).
fof(f1218,plain,
elem_13 != s(elem_34),
inference(forward_demodulation,[],[f1211,f594]) ).
fof(f1224,plain,
elem_13 != elem_37,
inference(forward_demodulation,[],[f1218,f596]) ).
fof(f1230,plain,
( $false
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f1224,f1138]) ).
fof(f1231,plain,
~ spl0_9,
inference(avatar_contradiction_clause,[],[f1230]) ).
fof(f1237,plain,
( elem_38 = select(earray_52,elem_37)
| elem_16 = elem_37
| ~ spl0_10 ),
inference(superposition,[],[f1142,f700]) ).
fof(f1240,definition,
( spl0_11
<=> elem_16 = elem_37 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f1242,plain,
( elem_16 = elem_37
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f1240]) ).
fof(f1244,definition,
( spl0_12
<=> elem_38 = select(earray_52,elem_37) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f1246,plain,
( elem_38 = select(earray_52,elem_37)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f1244]) ).
fof(f1248,plain,
( spl0_11
| spl0_12
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f1237,f1140,f1244,f1240]) ).
fof(f1359,plain,
elem_16 != s(s(s(s(s(s(elem_19)))))),
inference(superposition,[],[f542,f583]) ).
fof(f1371,plain,
elem_16 != s(s(s(s(s(elem_22))))),
inference(forward_demodulation,[],[f1359,f586]) ).
fof(f1382,plain,
elem_16 != s(s(s(s(elem_25)))),
inference(forward_demodulation,[],[f1371,f588]) ).
fof(f1392,plain,
elem_16 != s(s(s(elem_28))),
inference(forward_demodulation,[],[f1382,f590]) ).
fof(f1401,plain,
elem_16 != s(s(elem_31)),
inference(forward_demodulation,[],[f1392,f592]) ).
fof(f1409,plain,
elem_16 != s(elem_34),
inference(forward_demodulation,[],[f1401,f594]) ).
fof(f1416,plain,
elem_16 != elem_37,
inference(forward_demodulation,[],[f1409,f596]) ).
fof(f1423,plain,
( $false
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f1416,f1242]) ).
fof(f1424,plain,
~ spl0_11,
inference(avatar_contradiction_clause,[],[f1423]) ).
fof(f1431,plain,
( elem_38 = select(earray_50,elem_37)
| elem_19 = elem_37
| ~ spl0_12 ),
inference(superposition,[],[f1246,f699]) ).
fof(f1434,definition,
( spl0_13
<=> elem_19 = elem_37 ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f1436,plain,
( elem_19 = elem_37
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f1434]) ).
fof(f1438,definition,
( spl0_14
<=> elem_38 = select(earray_50,elem_37) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f1440,plain,
( elem_38 = select(earray_50,elem_37)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f1438]) ).
fof(f1442,plain,
( spl0_13
| spl0_14
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f1431,f1244,f1438,f1434]) ).
fof(f1461,plain,
elem_19 != s(s(s(s(s(elem_22))))),
inference(superposition,[],[f543,f586]) ).
fof(f1471,plain,
elem_19 != s(s(s(s(elem_25)))),
inference(forward_demodulation,[],[f1461,f588]) ).
fof(f1482,plain,
elem_19 != s(s(s(elem_28))),
inference(forward_demodulation,[],[f1471,f590]) ).
fof(f1492,plain,
elem_19 != s(s(elem_31)),
inference(forward_demodulation,[],[f1482,f592]) ).
fof(f1501,plain,
elem_19 != s(elem_34),
inference(forward_demodulation,[],[f1492,f594]) ).
fof(f1509,plain,
elem_19 != elem_37,
inference(forward_demodulation,[],[f1501,f596]) ).
fof(f1517,plain,
( $false
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f1509,f1436]) ).
fof(f1518,plain,
~ spl0_13,
inference(avatar_contradiction_clause,[],[f1517]) ).
fof(f1527,plain,
( elem_38 = select(earray_48,elem_37)
| elem_22 = elem_37
| ~ spl0_14 ),
inference(superposition,[],[f698,f1440]) ).
fof(f1528,plain,
( elem_38 = select(earray_48,elem_37)
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1527,f1080]) ).
fof(f1530,plain,
( elem_38 = select(earray_46,elem_37)
| elem_25 = elem_37
| ~ spl0_14 ),
inference(superposition,[],[f1528,f697]) ).
fof(f1533,definition,
( spl0_15
<=> elem_25 = elem_37 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f1535,plain,
( elem_25 = elem_37
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f1533]) ).
fof(f1537,definition,
( spl0_16
<=> elem_38 = select(earray_46,elem_37) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f1539,plain,
( elem_38 = select(earray_46,elem_37)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f1537]) ).
fof(f1541,plain,
( spl0_15
| spl0_16
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f1530,f1438,f1537,f1533]) ).
fof(f1750,plain,
elem_28 != s(s(s(elem_31))),
inference(superposition,[],[f545,f592]) ).
fof(f1751,plain,
elem_28 != s(s(elem_31)),
inference(superposition,[],[f546,f592]) ).
fof(f1755,plain,
elem_28 != s(elem_34),
inference(forward_demodulation,[],[f1751,f594]) ).
fof(f1756,plain,
elem_28 != s(s(elem_34)),
inference(forward_demodulation,[],[f1750,f594]) ).
fof(f1766,plain,
elem_28 != elem_37,
inference(forward_demodulation,[],[f1755,f596]) ).
fof(f1767,plain,
elem_28 != s(elem_37),
inference(forward_demodulation,[],[f1756,f596]) ).
fof(f1778,plain,
( elem_28 != s(elem_25)
| ~ spl0_15 ),
inference(forward_demodulation,[],[f1767,f1535]) ).
fof(f1788,plain,
( $false
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1778,f590]) ).
fof(f1789,plain,
~ spl0_15,
inference(avatar_contradiction_clause,[],[f1788]) ).
fof(f1800,plain,
( elem_38 = select(earray_44,elem_37)
| elem_28 = elem_37
| ~ spl0_16 ),
inference(superposition,[],[f696,f1539]) ).
fof(f1801,plain,
( elem_38 = select(earray_44,elem_37)
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1800,f1766]) ).
fof(f1803,plain,
( elem_38 = select(earray_42,elem_37)
| elem_31 = elem_37
| ~ spl0_16 ),
inference(superposition,[],[f1801,f695]) ).
fof(f1806,definition,
( spl0_17
<=> elem_31 = elem_37 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f1808,plain,
( elem_31 = elem_37
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f1806]) ).
fof(f1810,definition,
( spl0_18
<=> elem_38 = select(earray_42,elem_37) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f1812,plain,
( elem_38 = select(earray_42,elem_37)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f1810]) ).
fof(f1814,plain,
( spl0_17
| spl0_18
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f1803,f1537,f1810,f1806]) ).
fof(f1833,plain,
elem_0 != s(s(s(s(s(s(s(s(s(s(s(elem_4))))))))))),
inference(superposition,[],[f537,f598]) ).
fof(f1855,plain,
elem_0 != s(s(s(s(s(s(s(s(s(s(elem_7)))))))))),
inference(forward_demodulation,[],[f1833,f627]) ).
fof(f1866,plain,
elem_0 != s(s(s(s(s(s(s(s(s(elem_10))))))))),
inference(forward_demodulation,[],[f1855,f577]) ).
fof(f1876,plain,
elem_0 != s(s(s(s(s(s(s(s(elem_13)))))))),
inference(forward_demodulation,[],[f1866,f579]) ).
fof(f1885,plain,
elem_0 != s(s(s(s(s(s(s(elem_16))))))),
inference(forward_demodulation,[],[f1876,f581]) ).
fof(f1893,plain,
elem_0 != s(s(s(s(s(s(elem_19)))))),
inference(forward_demodulation,[],[f1885,f583]) ).
fof(f1900,plain,
elem_0 != s(s(s(s(s(elem_22))))),
inference(forward_demodulation,[],[f1893,f586]) ).
fof(f1906,plain,
elem_0 != s(s(s(s(elem_25)))),
inference(forward_demodulation,[],[f1900,f588]) ).
fof(f1911,plain,
elem_0 != s(s(s(elem_28))),
inference(forward_demodulation,[],[f1906,f590]) ).
fof(f1915,plain,
elem_0 != s(s(elem_31)),
inference(forward_demodulation,[],[f1911,f592]) ).
fof(f1918,plain,
elem_0 != s(elem_34),
inference(forward_demodulation,[],[f1915,f594]) ).
fof(f1920,plain,
elem_0 != elem_37,
inference(forward_demodulation,[],[f1918,f596]) ).
fof(f1936,plain,
elem_31 != s(elem_34),
inference(superposition,[],[f547,f594]) ).
fof(f1938,plain,
elem_31 != elem_37,
inference(forward_demodulation,[],[f1936,f596]) ).
fof(f1950,plain,
( $false
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1938,f1808]) ).
fof(f1951,plain,
~ spl0_17,
inference(avatar_contradiction_clause,[],[f1950]) ).
fof(f1963,plain,
~ spl0_3,
inference(avatar_split_clause,[],[f1920,f886]) ).
fof(f1964,plain,
( elem_38 = select(a,elem_37)
| elem_34 = elem_37
| ~ spl0_18 ),
inference(superposition,[],[f1812,f691]) ).
fof(f1967,plain,
( elem_38 = select(a,elem_37)
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1964,f744]) ).
fof(f1969,plain,
( elem_38 = elem_40
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1967,f599]) ).
fof(f1972,plain,
( $false
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1969,f630]) ).
fof(f1973,plain,
~ spl0_18,
inference(avatar_contradiction_clause,[],[f1972]) ).
cnf(s2,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f737]) ).
cnf(s3,plain,
~ spl0_1,
inference(sat_conversion,[],[f840]) ).
cnf(s5,plain,
( ~ spl0_2
| spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f894]) ).
cnf(s7,plain,
( ~ spl0_4
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f906]) ).
cnf(s8,plain,
~ spl0_5,
inference(sat_conversion,[],[f1004]) ).
cnf(s10,plain,
( ~ spl0_6
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f1018]) ).
cnf(s11,plain,
~ spl0_7,
inference(sat_conversion,[],[f1125]) ).
cnf(s13,plain,
( ~ spl0_8
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f1144]) ).
cnf(s14,plain,
~ spl0_9,
inference(sat_conversion,[],[f1231]) ).
cnf(s16,plain,
( ~ spl0_10
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f1248]) ).
cnf(s17,plain,
~ spl0_11,
inference(sat_conversion,[],[f1424]) ).
cnf(s19,plain,
( ~ spl0_12
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f1442]) ).
cnf(s20,plain,
~ spl0_13,
inference(sat_conversion,[],[f1518]) ).
cnf(s22,plain,
( ~ spl0_14
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f1541]) ).
cnf(s23,plain,
~ spl0_15,
inference(sat_conversion,[],[f1789]) ).
cnf(s25,plain,
( ~ spl0_16
| spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f1814]) ).
cnf(s26,plain,
~ spl0_17,
inference(sat_conversion,[],[f1951]) ).
cnf(s27,plain,
~ spl0_3,
inference(sat_conversion,[],[f1963]) ).
cnf(s29,plain,
~ spl0_18,
inference(sat_conversion,[],[f1973]) ).
cnf(s30,plain,
~ spl0_16,
inference(rat,[],[s25,s29,s26]) ).
cnf(s31,plain,
~ spl0_14,
inference(rat,[],[s22,s30,s23]) ).
cnf(s32,plain,
~ spl0_12,
inference(rat,[],[s19,s31,s20]) ).
cnf(s33,plain,
~ spl0_10,
inference(rat,[],[s16,s32,s17]) ).
cnf(s34,plain,
~ spl0_8,
inference(rat,[],[s13,s33,s14]) ).
cnf(s35,plain,
~ spl0_6,
inference(rat,[],[s10,s34,s11]) ).
cnf(s36,plain,
~ spl0_4,
inference(rat,[],[s7,s35,s8]) ).
cnf(s37,plain,
~ spl0_2,
inference(rat,[],[s5,s36,s27]) ).
cnf(s38,plain,
$false,
inference(rat,[],[s2,s37,s3]) ).
fof(f1974,plain,
$false,
inference(avatar_sat_refutation,[],[s38]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV567-1.013 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.19 % Computer : n009.cluster.edu
% 0.06/0.19 % Model : x86_64 x86_64
% 0.06/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.19 % Memory : 8046.5625MB
% 0.06/0.19 % OS : Linux 6.8.0-71-generic
% 0.06/0.19 % CPULimit : 300
% 0.06/0.19 % WCLimit : 300
% 0.06/0.19 % DateTime : Mon Sep 28 11:52:39 UTC 2026
% 0.06/0.20 % CPUTime :
% 0.06/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.23 Running first-order theorem proving
% 0.06/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.00/2.06 % (2986338)Input is clausal, will run a generic CNF schedule.
% 8.00/2.06 % (2986347)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1775801452:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2996 on theBenchmark for (2996ds/114Mi)
% 8.00/2.06 % (2986347)Instruction limit reached!
% 8.00/2.06 % (2986347)------------------------------
% 8.00/2.06 % (2986347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.00/2.06 % (2986347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/2.06 % (2986347)CaDiCaL version: 2.1.3
% 8.00/2.06 % (2986347)Termination reason: Instruction limit
% 8.00/2.06 % (2986347)Termination phase: Property scanning
% 8.00/2.06 % (2986347)Time elapsed: 0.024 s
% 8.00/2.06 % (2986347)Peak memory usage: 84 MB
% 8.00/2.06 % (2986347)Instructions burned: 117 (million)
% 8.00/2.06 % (2986344)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1999788869:i=132376:av=off_2996 on theBenchmark for (2996ds/132376Mi)
% 8.00/2.06 % (2986348)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1620234687:s2a=on:i=180:gtg=position_2996 on theBenchmark for (2996ds/180Mi)
% 8.00/2.06 % (2986343)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2518206061:i=140167_2996 on theBenchmark for (2996ds/140167Mi)
% 8.00/2.06 % (2986345)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1267799700:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2996 on theBenchmark for (2996ds/137899Mi)
% 8.00/2.06 % (2986349)dis-21_1_sil=8000:lcm=predicate:random_seed=1980230510:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2996 on theBenchmark for (2996ds/117Mi)
% 8.00/2.06 % (2986346)lrs+10_1_sil=8000:sp=occurrence:random_seed=2225067838:i=107:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/107Mi)
% 8.00/2.06 % (2986349)Instruction limit reached!
% 8.00/2.06 % (2986349)------------------------------
% 8.00/2.06 % (2986349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.00/2.06 % (2986349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/2.06 % (2986349)CaDiCaL version: 2.1.3
% 8.00/2.06 % (2986349)Termination reason: Instruction limit
% 8.00/2.06 % (2986349)Termination phase: Property scanning
% 8.00/2.06 % (2986349)Time elapsed: 0.039 s
% 8.00/2.06 % (2986349)Peak memory usage: 84 MB
% 8.00/2.06 % (2986349)Instructions burned: 117 (million)
% 8.00/2.06 % (2986346)Instruction limit reached!
% 8.00/2.06 % (2986346)------------------------------
% 8.00/2.06 % (2986346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.00/2.06 % (2986346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/2.06 % (2986346)CaDiCaL version: 2.1.3
% 8.00/2.06 % (2986346)Termination reason: Instruction limit
% 8.00/2.06 % (2986346)Termination phase: Property scanning
% 8.00/2.06 % (2986346)Time elapsed: 0.040 s
% 8.00/2.06 % (2986346)Peak memory usage: 84 MB
% 8.00/2.06 % (2986346)Instructions burned: 110 (million)
% 8.00/2.06 % (2986348)Instruction limit reached!
% 8.00/2.06 % (2986348)------------------------------
% 8.00/2.06 % (2986348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.00/2.06 % (2986348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/2.06 % (2986348)CaDiCaL version: 2.1.3
% 8.00/2.06 % (2986348)Termination reason: Instruction limit
% 8.00/2.06 % (2986348)Termination phase: SInE selection
% 8.00/2.06 % (2986348)Time elapsed: 0.058 s
% 8.00/2.06 % (2986348)Peak memory usage: 84 MB
% 8.00/2.06 % (2986348)Instructions burned: 180 (million)
% 8.00/2.06 % (2986351)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2984650277:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 8.00/2.06 % (2986351)Instruction limit reached!
% 8.00/2.06 % (2986351)------------------------------
% 8.00/2.06 % (2986351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.00/2.06 % (2986351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.00/2.06 % (2986351)CaDiCaL version: 2.1.3
% 8.00/2.06 % (2986351)Termination reason: Instruction limit
% 8.00/2.06 % (2986351)Termination phase: Property scanning
% 8.00/2.06 % (2986351)Time elapsed: 0.027 s
% 8.00/2.06 % (2986351)Peak memory usage: 84 MB
% 8.00/2.06 % (2986351)Instructions burned: 149 (million)
% 11.19/2.64 % (2986359)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2758949329:st=4:i=219:sd=3:ss=axioms_2994 on theBenchmark for (2994ds/219Mi)
% 11.19/2.64 % (2986358)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1060925571:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2994 on theBenchmark for (2994ds/189Mi)
% 11.19/2.64 % (2986360)lrs+10_64_to=lpo:sil=8000:random_seed=2686921133:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 11.19/2.64 % (2986362)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=948683123:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 11.19/2.64 % (2986360)Instruction limit reached!
% 11.19/2.64 % (2986360)------------------------------
% 11.19/2.64 % (2986360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.64 % (2986360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.64 % (2986360)CaDiCaL version: 2.1.3
% 11.19/2.64 % (2986360)Termination reason: Instruction limit
% 11.19/2.64 % (2986360)Termination phase: Property scanning
% 11.19/2.64 % (2986360)Time elapsed: 0.041 s
% 11.19/2.64 % (2986360)Peak memory usage: 85 MB
% 11.19/2.64 % (2986360)Instructions burned: 129 (million)
% 11.19/2.64 % (2986358)Instruction limit reached!
% 11.19/2.64 % (2986358)------------------------------
% 11.19/2.64 % (2986358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.64 % (2986358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.64 % (2986358)CaDiCaL version: 2.1.3
% 11.19/2.64 % (2986358)Termination reason: Instruction limit
% 11.19/2.64 % (2986358)Termination phase: Property scanning
% 11.19/2.64 % (2986358)Time elapsed: 0.076 s
% 11.19/2.64 % (2986358)Peak memory usage: 84 MB
% 11.19/2.64 % (2986358)Instructions burned: 190 (million)
% 11.19/2.64 % (2986359)Instruction limit reached!
% 11.19/2.64 % (2986359)------------------------------
% 11.19/2.64 % (2986359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.64 % (2986359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.64 % (2986359)CaDiCaL version: 2.1.3
% 11.19/2.64 % (2986359)Termination reason: Instruction limit
% 11.19/2.64 % (2986359)Termination phase: Property scanning
% 11.19/2.64 % (2986359)Time elapsed: 0.077 s
% 11.19/2.64 % (2986359)Peak memory usage: 84 MB
% 11.19/2.64 % (2986359)Instructions burned: 219 (million)
% 11.19/2.64 % (2986362)Instruction limit reached!
% 11.19/2.64 % (2986362)------------------------------
% 11.19/2.64 % (2986362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.64 % (2986362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.64 % (2986362)CaDiCaL version: 2.1.3
% 11.19/2.64 % (2986362)Termination reason: Instruction limit
% 11.19/2.64 % (2986362)Termination phase: Saturation
% 11.19/2.64 % (2986362)Time elapsed: 0.034 s
% 11.19/2.64 % (2986362)Peak memory usage: 87 MB
% 11.19/2.64 % (2986362)Instructions burned: 199 (million)
% 11.19/2.64 % (2986370)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3780634553:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 11.19/2.64 % (2986367)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1708268168:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi)
% 11.19/2.64 % (2986370)Instruction limit reached!
% 11.19/2.64 % (2986370)------------------------------
% 11.19/2.64 % (2986370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.64 % (2986370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.64 % (2986370)CaDiCaL version: 2.1.3
% 11.19/2.64 % (2986370)Termination reason: Instruction limit
% 11.19/2.64 % (2986370)Termination phase: Property scanning
% 11.19/2.64 % (2986370)Time elapsed: 0.018 s
% 11.19/2.64 % (2986370)Peak memory usage: 85 MB
% 11.19/2.64 % (2986370)Instructions burned: 112 (million)
% 11.19/2.64 % (2986369)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=173159274:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 11.19/2.64 % (2986368)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3288418803:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 11.19/2.64 % (2986367)Instruction limit reached!
% 11.19/2.64 % (2986367)------------------------------
% 11.19/2.64 % (2986367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.64 % (2986367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.64 % (2986367)CaDiCaL version: 2.1.3
% 11.19/2.64 % (2986367)Termination reason: Instruction limit
% 11.19/2.64 % (2986367)Termination phase: Property scanning
% 11.19/2.64 % (2986367)Time elapsed: 0.049 s
% 11.19/2.64 % (2986367)Peak memory usage: 84 MB
% 11.19/2.64 % (2986367)Instructions burned: 157 (million)
% 11.19/2.64 % (2986369)Instruction limit reached!
% 11.19/2.64 % (2986369)------------------------------
% 11.19/2.64 % (2986369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.64 % (2986369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.64 % (2986369)CaDiCaL version: 2.1.3
% 11.19/2.64 % (2986369)Termination reason: Instruction limit
% 11.19/2.64 % (2986369)Termination phase: Property scanning
% 11.19/2.64 % (2986369)Time elapsed: 0.047 s
% 11.19/2.64 % (2986369)Peak memory usage: 84 MB
% 11.19/2.64 % (2986369)Instructions burned: 108 (million)
% 11.19/2.64 % (2986373)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1100653400:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 11.19/2.64 % (2986373)Instruction limit reached!
% 11.19/2.64 % (2986373)------------------------------
% 11.19/2.64 % (2986373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.64 % (2986373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.64 % (2986373)CaDiCaL version: 2.1.3
% 11.19/2.64 % (2986373)Termination reason: Instruction limit
% 11.19/2.64 % (2986373)Termination phase: Property scanning
% 11.19/2.64 % (2986373)Time elapsed: 0.040 s
% 11.19/2.64 % (2986373)Peak memory usage: 84 MB
% 11.19/2.64 % (2986373)Instructions burned: 246 (million)
% 11.19/2.64 % (2986376)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1320404571:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 11.19/2.64 % (2986377)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=408667055:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 11.19/2.64 % (2986379)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2141648430:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 11.19/2.64 % (2986377)Instruction limit reached!
% 11.19/2.64 % (2986377)------------------------------
% 11.19/2.64 % (2986377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.64 % (2986377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.64 % (2986377)CaDiCaL version: 2.1.3
% 11.19/2.64 % (2986377)Termination reason: Instruction limit
% 11.19/2.64 % (2986377)Termination phase: Property scanning
% 11.19/2.64 % (2986377)Time elapsed: 0.048 s
% 11.19/2.64 % (2986377)Peak memory usage: 84 MB
% 11.19/2.64 % (2986377)Instructions burned: 134 (million)
% 11.19/2.64 % (2986379)Instruction limit reached!
% 11.19/2.64 % (2986379)------------------------------
% 11.19/2.64 % (2986379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.64 % (2986379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.64 % (2986379)CaDiCaL version: 2.1.3
% 11.19/2.64 % (2986379)Termination reason: Instruction limit
% 11.19/2.64 % (2986379)Termination phase: Saturation
% 11.19/2.64 % (2986379)Time elapsed: 0.085 s
% 11.19/2.64 % (2986379)Peak memory usage: 88 MB
% 11.19/2.64 % (2986379)Instructions burned: 504 (million)
% 11.19/2.64 % (2986383)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2746324653:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 11.19/2.64 % (2986384)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=725602600:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 11.19/2.64 % (2986383)Instruction limit reached!
% 11.19/2.64 % (2986383)------------------------------
% 11.19/2.64 % (2986383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.64 % (2986383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.64 % (2986383)CaDiCaL version: 2.1.3
% 11.19/2.64 % (2986383)Termination reason: Instruction limit
% 11.19/2.64 % (2986383)Termination phase: Saturation
% 11.19/2.64 % (2986383)Time elapsed: 0.061 s
% 11.19/2.64 % (2986383)Peak memory usage: 87 MB
% 11.19/2.64 % (2986383)Instructions burned: 191 (million)
% 11.19/2.64 % (2986384)Instruction limit reached!
% 11.19/2.64 % (2986384)------------------------------
% 11.19/2.64 % (2986384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.64 % (2986384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.64 % (2986384)CaDiCaL version: 2.1.3
% 11.19/2.64 % (2986384)Termination reason: Instruction limit
% 11.19/2.64 % (2986384)Termination phase: Saturation
% 11.19/2.64 % (2986384)Time elapsed: 0.046 s
% 11.19/2.64 % (2986384)Peak memory usage: 87 MB
% 11.19/2.64 % (2986384)Instructions burned: 265 (million)
% 11.19/2.64 % (2986387)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=393354084:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 11.19/2.64 % (2986388)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1930131233:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi)
% 11.19/2.64 % (2986387)Instruction limit reached!
% 11.19/2.64 % (2986387)------------------------------
% 11.19/2.64 % (2986387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.64 % (2986387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.64 % (2986387)CaDiCaL version: 2.1.3
% 11.19/2.64 % (2986387)Termination reason: Instruction limit
% 11.19/2.64 % (2986387)Termination phase: Property scanning
% 11.19/2.64 % (2986387)Time elapsed: 0.049 s
% 11.19/2.64 % (2986387)Peak memory usage: 84 MB
% 11.19/2.64 % (2986387)Instructions burned: 158 (million)
% 11.19/2.64 % (2986343)First to succeed.
% 11.19/2.64 % (2986343)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2986338"
% 11.19/2.64 % (2986391)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1797617671:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi)
% 11.19/2.64 % (2986391)Instruction limit reached!
% 11.19/2.64 % (2986391)------------------------------
% 11.19/2.64 % (2986391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.19/2.64 % (2986391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.19/2.64 % (2986391)CaDiCaL version: 2.1.3
% 11.19/2.64 % (2986391)Termination reason: Instruction limit
% 11.19/2.64 % (2986391)Termination phase: Saturation
% 11.19/2.64 % (2986391)Time elapsed: 0.198 s
% 11.19/2.64 % (2986391)Peak memory usage: 89 MB
% 11.19/2.64 % (2986391)Instructions burned: 537 (million)
% 11.19/2.64 % (2986343)Refutation found. Thanks to Tanya!
% 11.19/2.64 % SZS status Unsatisfiable for theBenchmark
% 11.19/2.64 % SZS output start Proof for theBenchmark
% See solution above
% 12.51/2.85 % (2986343)------------------------------
% 12.51/2.85 % (2986343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.85 % (2986343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.85 % (2986343)CaDiCaL version: 2.1.3
% 12.51/2.85 % (2986343)Termination reason: Refutation
% 12.51/2.85 % (2986343)Time elapsed: 1.203 s
% 12.51/2.85 % (2986343)Peak memory usage: 133 MB
% 12.51/2.85 % (2986343)Instructions burned: 2217 (million)
% 12.51/2.85 % (2986343)------------------------------
% 12.51/2.85 % (2986343)------------------------------
% 12.51/2.85 % (2986338)Success in time 1.968 s
% 12.51/2.85 % Vampire exiting
%------------------------------------------------------------------------------