%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV567-1.014 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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 12.23s 3.01s
% Output : Refutation 14.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 64
% Syntax : Number of formulae : 274 ( 168 unt; 16 def)
% Number of atoms : 407 ( 251 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 350 ( 217 ~; 117 |; 0 &)
% ( 16 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 18 ( 16 usr; 17 prp; 0-2 aty)
% Number of functors : 51 ( 51 usr; 48 con; 0-3 aty)
% Number of variables : 35 ( 0 sgn 35 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',a2) ).
fof(f619,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as14) ).
fof(f620,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as13) ).
fof(f621,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as12) ).
fof(f622,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as11) ).
fof(f623,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as10) ).
fof(f624,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as9) ).
fof(f625,axiom,
! [X0] : s(s(s(s(s(s(s(s(X0)))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as8) ).
fof(f626,axiom,
! [X0] : s(s(s(s(s(s(s(X0))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as7) ).
fof(f627,axiom,
! [X0] : s(s(s(s(s(s(X0)))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as6) ).
fof(f628,axiom,
! [X0] : s(s(s(s(s(X0))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as5) ).
fof(f629,axiom,
! [X0] : s(s(s(s(X0)))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as4) ).
fof(f630,axiom,
! [X0] : s(s(s(X0))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as3) ).
fof(f631,axiom,
! [X0] : s(s(X0)) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as2) ).
fof(f632,axiom,
! [X0] : s(X0) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as1) ).
fof(f644,axiom,
earray_42 = store(earray_39,elem_40,elem_41),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp11) ).
fof(f645,axiom,
earray_45 = store(a,elem_37,elem_44),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp12) ).
fof(f646,axiom,
earray_47 = store(earray_45,elem_34,elem_46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp13) ).
fof(f647,axiom,
earray_49 = store(earray_47,elem_31,elem_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp14) ).
fof(f648,axiom,
earray_51 = store(earray_49,elem_28,elem_50),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp15) ).
fof(f649,axiom,
earray_53 = store(earray_51,elem_25,elem_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp16) ).
fof(f650,axiom,
earray_55 = store(earray_53,elem_22,elem_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp17) ).
fof(f651,axiom,
earray_57 = store(earray_55,elem_19,elem_56),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp18) ).
fof(f652,axiom,
earray_59 = store(earray_57,elem_16,elem_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp19) ).
fof(f654,axiom,
earray_61 = store(earray_59,elem_13,elem_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp21) ).
fof(f655,axiom,
earray_63 = store(earray_61,elem_10,elem_62),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp22) ).
fof(f656,axiom,
earray_65 = store(earray_63,elem_7,elem_64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp23) ).
fof(f657,axiom,
earray_67 = store(earray_65,elem_4,elem_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp24) ).
fof(f658,axiom,
earray_69 = store(earray_67,elem_0,elem_68),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp25) ).
fof(f659,axiom,
earray_71 = store(earray_69,i,elem_70),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp26) ).
fof(f661,axiom,
elem_0 = s(i),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp28) ).
fof(f663,axiom,
elem_10 = s(elem_7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp30) ).
fof(f665,axiom,
elem_13 = s(elem_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp32) ).
fof(f667,axiom,
elem_16 = s(elem_13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp34) ).
fof(f669,axiom,
elem_19 = s(elem_16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp36) ).
fof(f672,axiom,
elem_22 = s(elem_19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp39) ).
fof(f674,axiom,
elem_25 = s(elem_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp41) ).
fof(f676,axiom,
elem_28 = s(elem_25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp43) ).
fof(f678,axiom,
elem_31 = s(elem_28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp45) ).
fof(f680,axiom,
elem_34 = s(elem_31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp47) ).
fof(f682,axiom,
elem_37 = s(elem_34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp49) ).
fof(f684,axiom,
elem_4 = s(elem_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp51) ).
fof(f685,axiom,
elem_40 = s(elem_37),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp52) ).
fof(f687,axiom,
elem_43 = select(a,elem_40),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp54) ).
fof(f715,axiom,
elem_7 = s(elem_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp69) ).
fof(f719,axiom,
earray_42 = earray_71,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp72) ).
fof(f720,negated_conjecture,
elem_41 != elem_43,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f721,plain,
store(earray_39,elem_40,elem_41) = earray_71,
inference(definition_unfolding,[],[f644,f719]) ).
fof(f722,plain,
elem_41 = select(earray_71,elem_40),
inference(superposition,[],[f1,f721]) ).
fof(f783,plain,
! [X0] :
( select(a,X0) = select(earray_45,X0)
| elem_37 = X0 ),
inference(superposition,[],[f2,f645]) ).
fof(f788,plain,
! [X0] :
( select(earray_45,X0) = select(earray_47,X0)
| elem_34 = X0 ),
inference(superposition,[],[f2,f646]) ).
fof(f789,plain,
! [X0] :
( select(earray_47,X0) = select(earray_49,X0)
| elem_31 = X0 ),
inference(superposition,[],[f2,f647]) ).
fof(f790,plain,
! [X0] :
( select(earray_49,X0) = select(earray_51,X0)
| elem_28 = X0 ),
inference(superposition,[],[f2,f648]) ).
fof(f791,plain,
! [X0] :
( select(earray_51,X0) = select(earray_53,X0)
| elem_25 = X0 ),
inference(superposition,[],[f2,f649]) ).
fof(f792,plain,
! [X0] :
( select(earray_53,X0) = select(earray_55,X0)
| elem_22 = X0 ),
inference(superposition,[],[f2,f650]) ).
fof(f793,plain,
! [X0] :
( select(earray_55,X0) = select(earray_57,X0)
| elem_19 = X0 ),
inference(superposition,[],[f2,f651]) ).
fof(f794,plain,
! [X0] :
( select(earray_57,X0) = select(earray_59,X0)
| elem_16 = X0 ),
inference(superposition,[],[f2,f652]) ).
fof(f795,plain,
! [X0] :
( select(earray_59,X0) = select(earray_61,X0)
| elem_13 = X0 ),
inference(superposition,[],[f2,f654]) ).
fof(f797,plain,
! [X0] :
( select(earray_61,X0) = select(earray_63,X0)
| elem_10 = X0 ),
inference(superposition,[],[f2,f655]) ).
fof(f798,plain,
! [X0] :
( select(earray_63,X0) = select(earray_65,X0)
| elem_7 = X0 ),
inference(superposition,[],[f2,f656]) ).
fof(f799,plain,
! [X0] :
( select(earray_65,X0) = select(earray_67,X0)
| elem_4 = X0 ),
inference(superposition,[],[f2,f657]) ).
fof(f800,plain,
! [X0] :
( select(earray_67,X0) = select(earray_69,X0)
| elem_0 = X0 ),
inference(superposition,[],[f2,f658]) ).
fof(f801,plain,
! [X0] :
( select(earray_71,X0) = select(earray_69,X0)
| i = X0 ),
inference(superposition,[],[f2,f659]) ).
fof(f820,plain,
( elem_41 = select(earray_69,elem_40)
| elem_40 = i ),
inference(superposition,[],[f801,f722]) ).
fof(f825,definition,
( spl0_1
<=> elem_40 = i ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f827,plain,
( elem_40 = i
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f825]) ).
fof(f829,definition,
( spl0_2
<=> elem_41 = select(earray_69,elem_40) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f831,plain,
( elem_41 = select(earray_69,elem_40)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f829]) ).
fof(f833,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f820,f829,f825]) ).
fof(f840,plain,
elem_37 != elem_40,
inference(superposition,[],[f632,f685]) ).
fof(f891,plain,
( elem_41 = select(earray_67,elem_40)
| elem_0 = elem_40
| ~ spl0_2 ),
inference(superposition,[],[f831,f800]) ).
fof(f894,definition,
( spl0_3
<=> elem_0 = elem_40 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f896,plain,
( elem_0 = elem_40
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f894]) ).
fof(f898,definition,
( spl0_4
<=> elem_41 = select(earray_67,elem_40) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f900,plain,
( elem_41 = select(earray_67,elem_40)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f898]) ).
fof(f902,plain,
( spl0_3
| spl0_4
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f891,f829,f898,f894]) ).
fof(f999,plain,
elem_10 != s(s(s(s(s(s(s(s(s(s(s(s(elem_13)))))))))))),
inference(superposition,[],[f620,f665]) ).
fof(f1002,plain,
elem_10 != s(s(s(s(s(s(s(s(s(elem_13))))))))),
inference(superposition,[],[f623,f665]) ).
fof(f1020,plain,
elem_10 != s(s(s(s(s(s(s(s(elem_16)))))))),
inference(forward_demodulation,[],[f1002,f667]) ).
fof(f1023,plain,
elem_10 != s(s(s(s(s(s(s(s(s(s(s(elem_16))))))))))),
inference(forward_demodulation,[],[f999,f667]) ).
fof(f1031,plain,
elem_10 != s(s(s(s(s(s(s(elem_19))))))),
inference(forward_demodulation,[],[f1020,f669]) ).
fof(f1034,plain,
elem_10 != s(s(s(s(s(s(s(s(s(s(elem_19)))))))))),
inference(forward_demodulation,[],[f1023,f669]) ).
fof(f1041,plain,
elem_10 != s(s(s(s(s(s(elem_22)))))),
inference(forward_demodulation,[],[f1031,f672]) ).
fof(f1044,plain,
elem_10 != s(s(s(s(s(s(s(s(s(elem_22))))))))),
inference(forward_demodulation,[],[f1034,f672]) ).
fof(f1050,plain,
elem_10 != s(s(s(s(s(elem_25))))),
inference(forward_demodulation,[],[f1041,f674]) ).
fof(f1053,plain,
elem_10 != s(s(s(s(s(s(s(s(elem_25)))))))),
inference(forward_demodulation,[],[f1044,f674]) ).
fof(f1058,plain,
elem_10 != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f1050,f676]) ).
fof(f1061,plain,
elem_10 != s(s(s(s(s(s(s(elem_28))))))),
inference(forward_demodulation,[],[f1053,f676]) ).
fof(f1065,plain,
elem_10 != s(s(s(elem_31))),
inference(forward_demodulation,[],[f1058,f678]) ).
fof(f1068,plain,
elem_10 != s(s(s(s(s(s(elem_31)))))),
inference(forward_demodulation,[],[f1061,f678]) ).
fof(f1071,plain,
elem_10 != s(s(elem_34)),
inference(forward_demodulation,[],[f1065,f680]) ).
fof(f1074,plain,
elem_10 != s(s(s(s(s(elem_34))))),
inference(forward_demodulation,[],[f1068,f680]) ).
fof(f1076,plain,
elem_10 != s(elem_37),
inference(forward_demodulation,[],[f1071,f682]) ).
fof(f1079,plain,
elem_10 != s(s(s(s(elem_37)))),
inference(forward_demodulation,[],[f1074,f682]) ).
fof(f1080,plain,
elem_10 != elem_40,
inference(forward_demodulation,[],[f1076,f685]) ).
fof(f1083,plain,
elem_10 != s(s(s(elem_40))),
inference(forward_demodulation,[],[f1079,f685]) ).
fof(f1087,plain,
( elem_10 != s(s(s(elem_0)))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1083,f896]) ).
fof(f1090,plain,
( elem_10 != s(s(elem_4))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1087,f684]) ).
fof(f1092,plain,
( elem_10 != s(elem_7)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1090,f715]) ).
fof(f1093,plain,
( $false
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f1092,f663]) ).
fof(f1094,plain,
~ spl0_3,
inference(avatar_contradiction_clause,[],[f1093]) ).
fof(f1095,plain,
( elem_41 = select(earray_65,elem_40)
| elem_40 = elem_4
| ~ spl0_4 ),
inference(superposition,[],[f900,f799]) ).
fof(f1098,definition,
( spl0_5
<=> elem_40 = elem_4 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f1100,plain,
( elem_40 = elem_4
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f1098]) ).
fof(f1102,definition,
( spl0_6
<=> elem_41 = select(earray_65,elem_40) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f1104,plain,
( elem_41 = select(earray_65,elem_40)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f1102]) ).
fof(f1106,plain,
( spl0_5
| spl0_6
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f1095,f898,f1102,f1098]) ).
fof(f1122,plain,
elem_22 != s(s(s(s(s(s(s(s(s(s(s(elem_25))))))))))),
inference(superposition,[],[f621,f674]) ).
fof(f1128,plain,
elem_22 != s(s(s(s(s(elem_25))))),
inference(superposition,[],[f627,f674]) ).
fof(f1138,plain,
elem_22 != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f1128,f676]) ).
fof(f1144,plain,
elem_22 != s(s(s(s(s(s(s(s(s(s(elem_28)))))))))),
inference(forward_demodulation,[],[f1122,f676]) ).
fof(f1149,plain,
elem_22 != s(s(s(elem_31))),
inference(forward_demodulation,[],[f1138,f678]) ).
fof(f1155,plain,
elem_22 != s(s(s(s(s(s(s(s(s(elem_31))))))))),
inference(forward_demodulation,[],[f1144,f678]) ).
fof(f1159,plain,
elem_22 != s(s(elem_34)),
inference(forward_demodulation,[],[f1149,f680]) ).
fof(f1165,plain,
elem_22 != s(s(s(s(s(s(s(s(elem_34)))))))),
inference(forward_demodulation,[],[f1155,f680]) ).
fof(f1168,plain,
elem_22 != s(elem_37),
inference(forward_demodulation,[],[f1159,f682]) ).
fof(f1174,plain,
elem_22 != s(s(s(s(s(s(s(elem_37))))))),
inference(forward_demodulation,[],[f1165,f682]) ).
fof(f1176,plain,
elem_22 != elem_40,
inference(forward_demodulation,[],[f1168,f685]) ).
fof(f1182,plain,
elem_22 != s(s(s(s(s(s(elem_40)))))),
inference(forward_demodulation,[],[f1174,f685]) ).
fof(f1190,plain,
( elem_22 != s(s(s(s(s(s(elem_4))))))
| ~ spl0_5 ),
inference(forward_demodulation,[],[f1182,f1100]) ).
fof(f1197,plain,
( elem_22 != s(s(s(s(s(elem_7)))))
| ~ spl0_5 ),
inference(forward_demodulation,[],[f1190,f715]) ).
fof(f1203,plain,
( elem_22 != s(s(s(s(elem_10))))
| ~ spl0_5 ),
inference(forward_demodulation,[],[f1197,f663]) ).
fof(f1208,plain,
( elem_22 != s(s(s(elem_13)))
| ~ spl0_5 ),
inference(forward_demodulation,[],[f1203,f665]) ).
fof(f1212,plain,
( elem_22 != s(s(elem_16))
| ~ spl0_5 ),
inference(forward_demodulation,[],[f1208,f667]) ).
fof(f1215,plain,
( elem_22 != s(elem_19)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f1212,f669]) ).
fof(f1217,plain,
( $false
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f1215,f672]) ).
fof(f1218,plain,
~ spl0_5,
inference(avatar_contradiction_clause,[],[f1217]) ).
fof(f1220,plain,
( elem_41 = select(earray_63,elem_40)
| elem_40 = elem_7
| ~ spl0_6 ),
inference(superposition,[],[f1104,f798]) ).
fof(f1223,definition,
( spl0_7
<=> elem_40 = elem_7 ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f1225,plain,
( elem_40 = elem_7
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f1223]) ).
fof(f1227,definition,
( spl0_8
<=> elem_41 = select(earray_63,elem_40) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f1229,plain,
( elem_41 = select(earray_63,elem_40)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f1227]) ).
fof(f1231,plain,
( spl0_7
| spl0_8
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f1220,f1102,f1227,f1223]) ).
fof(f1333,plain,
elem_13 != s(s(s(s(s(s(s(s(s(s(elem_16)))))))))),
inference(superposition,[],[f622,f667]) ).
fof(f1335,plain,
elem_13 != s(s(s(s(s(s(s(s(elem_16)))))))),
inference(superposition,[],[f624,f667]) ).
fof(f1351,plain,
elem_13 != s(s(s(s(s(s(s(elem_19))))))),
inference(forward_demodulation,[],[f1335,f669]) ).
fof(f1353,plain,
elem_13 != s(s(s(s(s(s(s(s(s(elem_19))))))))),
inference(forward_demodulation,[],[f1333,f669]) ).
fof(f1362,plain,
elem_13 != s(s(s(s(s(s(elem_22)))))),
inference(forward_demodulation,[],[f1351,f672]) ).
fof(f1364,plain,
elem_13 != s(s(s(s(s(s(s(s(elem_22)))))))),
inference(forward_demodulation,[],[f1353,f672]) ).
fof(f1372,plain,
elem_13 != s(s(s(s(s(elem_25))))),
inference(forward_demodulation,[],[f1362,f674]) ).
fof(f1374,plain,
elem_13 != s(s(s(s(s(s(s(elem_25))))))),
inference(forward_demodulation,[],[f1364,f674]) ).
fof(f1381,plain,
elem_13 != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f1372,f676]) ).
fof(f1383,plain,
elem_13 != s(s(s(s(s(s(elem_28)))))),
inference(forward_demodulation,[],[f1374,f676]) ).
fof(f1389,plain,
elem_13 != s(s(s(elem_31))),
inference(forward_demodulation,[],[f1381,f678]) ).
fof(f1391,plain,
elem_13 != s(s(s(s(s(elem_31))))),
inference(forward_demodulation,[],[f1383,f678]) ).
fof(f1396,plain,
elem_13 != s(s(elem_34)),
inference(forward_demodulation,[],[f1389,f680]) ).
fof(f1398,plain,
elem_13 != s(s(s(s(elem_34)))),
inference(forward_demodulation,[],[f1391,f680]) ).
fof(f1402,plain,
elem_13 != s(elem_37),
inference(forward_demodulation,[],[f1396,f682]) ).
fof(f1404,plain,
elem_13 != s(s(s(elem_37))),
inference(forward_demodulation,[],[f1398,f682]) ).
fof(f1407,plain,
elem_13 != elem_40,
inference(forward_demodulation,[],[f1402,f685]) ).
fof(f1409,plain,
elem_13 != s(s(elem_40)),
inference(forward_demodulation,[],[f1404,f685]) ).
fof(f1414,plain,
( elem_13 != s(s(elem_7))
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1409,f1225]) ).
fof(f1418,plain,
( elem_13 != s(elem_10)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1414,f663]) ).
fof(f1421,plain,
( $false
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1418,f665]) ).
fof(f1422,plain,
~ spl0_7,
inference(avatar_contradiction_clause,[],[f1421]) ).
fof(f1426,plain,
( elem_41 = select(earray_61,elem_40)
| elem_10 = elem_40
| ~ spl0_8 ),
inference(superposition,[],[f797,f1229]) ).
fof(f1427,plain,
( elem_41 = select(earray_61,elem_40)
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f1426,f1080]) ).
fof(f1430,plain,
( elem_41 = select(earray_59,elem_40)
| elem_13 = elem_40
| ~ spl0_8 ),
inference(superposition,[],[f795,f1427]) ).
fof(f1431,plain,
( elem_41 = select(earray_59,elem_40)
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f1430,f1407]) ).
fof(f1433,plain,
( elem_41 = select(earray_57,elem_40)
| elem_16 = elem_40
| ~ spl0_8 ),
inference(superposition,[],[f1431,f794]) ).
fof(f1436,definition,
( spl0_9
<=> elem_16 = elem_40 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f1438,plain,
( elem_16 = elem_40
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f1436]) ).
fof(f1440,definition,
( spl0_10
<=> elem_41 = select(earray_57,elem_40) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f1442,plain,
( elem_41 = select(earray_57,elem_40)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f1440]) ).
fof(f1444,plain,
( spl0_9
| spl0_10
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f1433,f1227,f1440,f1436]) ).
fof(f1462,plain,
elem_16 != s(s(s(s(s(s(s(elem_19))))))),
inference(superposition,[],[f625,f669]) ).
fof(f1476,plain,
elem_16 != s(s(s(s(s(s(elem_22)))))),
inference(forward_demodulation,[],[f1462,f672]) ).
fof(f1487,plain,
elem_16 != s(s(s(s(s(elem_25))))),
inference(forward_demodulation,[],[f1476,f674]) ).
fof(f1497,plain,
elem_16 != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f1487,f676]) ).
fof(f1506,plain,
elem_16 != s(s(s(elem_31))),
inference(forward_demodulation,[],[f1497,f678]) ).
fof(f1514,plain,
elem_16 != s(s(elem_34)),
inference(forward_demodulation,[],[f1506,f680]) ).
fof(f1521,plain,
elem_16 != s(elem_37),
inference(forward_demodulation,[],[f1514,f682]) ).
fof(f1527,plain,
elem_16 != elem_40,
inference(forward_demodulation,[],[f1521,f685]) ).
fof(f1533,plain,
( $false
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f1527,f1438]) ).
fof(f1534,plain,
~ spl0_9,
inference(avatar_contradiction_clause,[],[f1533]) ).
fof(f1540,plain,
( elem_41 = select(earray_55,elem_40)
| elem_19 = elem_40
| ~ spl0_10 ),
inference(superposition,[],[f1442,f793]) ).
fof(f1543,definition,
( spl0_11
<=> elem_19 = elem_40 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f1545,plain,
( elem_19 = elem_40
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f1543]) ).
fof(f1547,definition,
( spl0_12
<=> elem_41 = select(earray_55,elem_40) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f1549,plain,
( elem_41 = select(earray_55,elem_40)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f1547]) ).
fof(f1551,plain,
( spl0_11
| spl0_12
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f1540,f1440,f1547,f1543]) ).
fof(f1662,plain,
elem_19 != s(s(s(s(s(s(elem_22)))))),
inference(superposition,[],[f626,f672]) ).
fof(f1674,plain,
elem_19 != s(s(s(s(s(elem_25))))),
inference(forward_demodulation,[],[f1662,f674]) ).
fof(f1685,plain,
elem_19 != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f1674,f676]) ).
fof(f1695,plain,
elem_19 != s(s(s(elem_31))),
inference(forward_demodulation,[],[f1685,f678]) ).
fof(f1704,plain,
elem_19 != s(s(elem_34)),
inference(forward_demodulation,[],[f1695,f680]) ).
fof(f1712,plain,
elem_19 != s(elem_37),
inference(forward_demodulation,[],[f1704,f682]) ).
fof(f1719,plain,
elem_19 != elem_40,
inference(forward_demodulation,[],[f1712,f685]) ).
fof(f1726,plain,
( $false
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f1719,f1545]) ).
fof(f1727,plain,
~ spl0_11,
inference(avatar_contradiction_clause,[],[f1726]) ).
fof(f1735,plain,
( elem_41 = select(earray_53,elem_40)
| elem_22 = elem_40
| ~ spl0_12 ),
inference(superposition,[],[f792,f1549]) ).
fof(f1736,plain,
( elem_41 = select(earray_53,elem_40)
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f1735,f1176]) ).
fof(f1738,plain,
( elem_41 = select(earray_51,elem_40)
| elem_25 = elem_40
| ~ spl0_12 ),
inference(superposition,[],[f1736,f791]) ).
fof(f1741,definition,
( spl0_13
<=> elem_25 = elem_40 ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f1743,plain,
( elem_25 = elem_40
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f1741]) ).
fof(f1745,definition,
( spl0_14
<=> elem_41 = select(earray_51,elem_40) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f1747,plain,
( elem_41 = select(earray_51,elem_40)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f1745]) ).
fof(f1749,plain,
( spl0_13
| spl0_14
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f1738,f1547,f1745,f1741]) ).
fof(f1864,plain,
elem_28 != s(s(s(s(elem_31)))),
inference(superposition,[],[f628,f678]) ).
fof(f1865,plain,
elem_28 != s(s(s(elem_31))),
inference(superposition,[],[f629,f678]) ).
fof(f1871,plain,
elem_28 != s(s(elem_34)),
inference(forward_demodulation,[],[f1865,f680]) ).
fof(f1872,plain,
elem_28 != s(s(s(elem_34))),
inference(forward_demodulation,[],[f1864,f680]) ).
fof(f1882,plain,
elem_28 != s(elem_37),
inference(forward_demodulation,[],[f1871,f682]) ).
fof(f1883,plain,
elem_28 != s(s(elem_37)),
inference(forward_demodulation,[],[f1872,f682]) ).
fof(f1892,plain,
elem_28 != elem_40,
inference(forward_demodulation,[],[f1882,f685]) ).
fof(f1893,plain,
elem_28 != s(elem_40),
inference(forward_demodulation,[],[f1883,f685]) ).
fof(f1903,plain,
( elem_28 != s(elem_25)
| ~ spl0_13 ),
inference(forward_demodulation,[],[f1893,f1743]) ).
fof(f1912,plain,
( $false
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f1903,f676]) ).
fof(f1913,plain,
~ spl0_13,
inference(avatar_contradiction_clause,[],[f1912]) ).
fof(f1923,plain,
( elem_41 = select(earray_49,elem_40)
| elem_28 = elem_40
| ~ spl0_14 ),
inference(superposition,[],[f790,f1747]) ).
fof(f1924,plain,
( elem_41 = select(earray_49,elem_40)
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1923,f1892]) ).
fof(f1926,plain,
( elem_41 = select(earray_47,elem_40)
| elem_31 = elem_40
| ~ spl0_14 ),
inference(superposition,[],[f1924,f789]) ).
fof(f1929,definition,
( spl0_15
<=> elem_31 = elem_40 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f1931,plain,
( elem_31 = elem_40
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f1929]) ).
fof(f1933,definition,
( spl0_16
<=> elem_41 = select(earray_47,elem_40) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f1935,plain,
( elem_41 = select(earray_47,elem_40)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f1933]) ).
fof(f1937,plain,
( spl0_15
| spl0_16
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f1926,f1745,f1933,f1929]) ).
fof(f1965,plain,
elem_34 != s(s(elem_37)),
inference(superposition,[],[f630,f682]) ).
fof(f1966,plain,
elem_34 != s(elem_37),
inference(superposition,[],[f631,f682]) ).
fof(f1968,plain,
elem_34 != elem_40,
inference(forward_demodulation,[],[f1966,f685]) ).
fof(f1969,plain,
elem_34 != s(elem_40),
inference(forward_demodulation,[],[f1965,f685]) ).
fof(f1981,plain,
( elem_34 != s(elem_31)
| ~ spl0_15 ),
inference(forward_demodulation,[],[f1969,f1931]) ).
fof(f1992,plain,
( $false
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1981,f680]) ).
fof(f1993,plain,
~ spl0_15,
inference(avatar_contradiction_clause,[],[f1992]) ).
fof(f2005,plain,
( elem_41 = select(earray_45,elem_40)
| elem_34 = elem_40
| ~ spl0_16 ),
inference(superposition,[],[f788,f1935]) ).
fof(f2006,plain,
( elem_41 = select(earray_45,elem_40)
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2005,f1968]) ).
fof(f2008,plain,
( elem_41 = select(a,elem_40)
| elem_37 = elem_40
| ~ spl0_16 ),
inference(superposition,[],[f2006,f783]) ).
fof(f2011,plain,
( elem_41 = select(a,elem_40)
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2008,f840]) ).
fof(f2013,plain,
( elem_41 = elem_43
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2011,f687]) ).
fof(f2016,plain,
( $false
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2013,f720]) ).
fof(f2017,plain,
~ spl0_16,
inference(avatar_contradiction_clause,[],[f2016]) ).
fof(f4321,plain,
i != s(s(s(s(s(s(s(s(s(s(s(s(s(elem_0))))))))))))),
inference(superposition,[],[f619,f661]) ).
fof(f4328,plain,
i != s(s(s(s(s(s(s(s(s(s(s(s(elem_4)))))))))))),
inference(forward_demodulation,[],[f4321,f684]) ).
fof(f4370,plain,
i != s(s(s(s(s(s(s(s(s(s(s(elem_7))))))))))),
inference(forward_demodulation,[],[f4328,f715]) ).
fof(f4412,plain,
i != s(s(s(s(s(s(s(s(s(s(elem_10)))))))))),
inference(forward_demodulation,[],[f4370,f663]) ).
fof(f4454,plain,
i != s(s(s(s(s(s(s(s(s(elem_13))))))))),
inference(forward_demodulation,[],[f4412,f665]) ).
fof(f4496,plain,
i != s(s(s(s(s(s(s(s(elem_16)))))))),
inference(forward_demodulation,[],[f4454,f667]) ).
fof(f4538,plain,
i != s(s(s(s(s(s(s(elem_19))))))),
inference(forward_demodulation,[],[f4496,f669]) ).
fof(f4580,plain,
i != s(s(s(s(s(s(elem_22)))))),
inference(forward_demodulation,[],[f4538,f672]) ).
fof(f4622,plain,
i != s(s(s(s(s(elem_25))))),
inference(forward_demodulation,[],[f4580,f674]) ).
fof(f4664,plain,
i != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f4622,f676]) ).
fof(f4706,plain,
i != s(s(s(elem_31))),
inference(forward_demodulation,[],[f4664,f678]) ).
fof(f4748,plain,
i != s(s(elem_34)),
inference(forward_demodulation,[],[f4706,f680]) ).
fof(f4790,plain,
i != s(elem_37),
inference(forward_demodulation,[],[f4748,f682]) ).
fof(f4832,plain,
elem_40 != i,
inference(forward_demodulation,[],[f4790,f685]) ).
fof(f4886,plain,
( $false
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f4832,f827]) ).
fof(f4887,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[],[f4886]) ).
cnf(s2,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f833]) ).
cnf(s4,plain,
( ~ spl0_2
| spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f902]) ).
cnf(s5,plain,
~ spl0_3,
inference(sat_conversion,[],[f1094]) ).
cnf(s7,plain,
( ~ spl0_4
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f1106]) ).
cnf(s8,plain,
~ spl0_5,
inference(sat_conversion,[],[f1218]) ).
cnf(s10,plain,
( ~ spl0_6
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f1231]) ).
cnf(s11,plain,
~ spl0_7,
inference(sat_conversion,[],[f1422]) ).
cnf(s13,plain,
( ~ spl0_8
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f1444]) ).
cnf(s14,plain,
~ spl0_9,
inference(sat_conversion,[],[f1534]) ).
cnf(s16,plain,
( ~ spl0_10
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f1551]) ).
cnf(s17,plain,
~ spl0_11,
inference(sat_conversion,[],[f1727]) ).
cnf(s19,plain,
( ~ spl0_12
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f1749]) ).
cnf(s20,plain,
~ spl0_13,
inference(sat_conversion,[],[f1913]) ).
cnf(s22,plain,
( ~ spl0_14
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f1937]) ).
cnf(s23,plain,
~ spl0_15,
inference(sat_conversion,[],[f1993]) ).
cnf(s25,plain,
~ spl0_16,
inference(sat_conversion,[],[f2017]) ).
cnf(s39,plain,
~ spl0_1,
inference(sat_conversion,[],[f4887]) ).
cnf(s40,plain,
~ spl0_14,
inference(rat,[],[s22,s25,s23]) ).
cnf(s41,plain,
~ spl0_12,
inference(rat,[],[s19,s40,s20]) ).
cnf(s42,plain,
~ spl0_10,
inference(rat,[],[s16,s41,s17]) ).
cnf(s43,plain,
~ spl0_8,
inference(rat,[],[s13,s42,s14]) ).
cnf(s44,plain,
~ spl0_6,
inference(rat,[],[s10,s43,s11]) ).
cnf(s45,plain,
~ spl0_4,
inference(rat,[],[s7,s44,s8]) ).
cnf(s46,plain,
~ spl0_2,
inference(rat,[],[s4,s45,s5]) ).
cnf(s47,plain,
$false,
inference(rat,[],[s2,s46,s39]) ).
fof(f4913,plain,
$false,
inference(avatar_sat_refutation,[],[s47]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV567-1.014 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n003.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.19 % DateTime : Mon Sep 28 11:55:12 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.49/2.00 % (1534485)Input is clausal, will run a generic CNF schedule.
% 3.49/2.00 % (1534494)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=382211161:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2995 on theBenchmark for (2995ds/114Mi)
% 3.49/2.00 % (1534494)Instruction limit reached!
% 3.49/2.00 % (1534494)------------------------------
% 3.49/2.00 % (1534494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.49/2.00 % (1534494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/2.00 % (1534494)CaDiCaL version: 2.1.3
% 3.49/2.00 % (1534494)Termination reason: Instruction limit
% 3.49/2.00 % (1534494)Termination phase: Property scanning
% 3.49/2.00 % (1534494)Time elapsed: 0.025 s
% 3.49/2.00 % (1534494)Peak memory usage: 84 MB
% 3.49/2.00 % (1534494)Instructions burned: 120 (million)
% 3.49/2.00 % (1534490)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=2913223066:i=140167_2995 on theBenchmark for (2995ds/140167Mi)
% 3.49/2.00 % (1534496)dis-21_1_sil=8000:lcm=predicate:random_seed=1845468846:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2995 on theBenchmark for (2995ds/117Mi)
% 3.49/2.00 % (1534493)lrs+10_1_sil=8000:sp=occurrence:random_seed=1562485197:i=107:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/107Mi)
% 3.49/2.00 % (1534492)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3547400214:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2995 on theBenchmark for (2995ds/137899Mi)
% 3.49/2.00 % (1534491)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2309281964:i=132376:av=off_2995 on theBenchmark for (2995ds/132376Mi)
% 3.49/2.00 % (1534495)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2375290342:s2a=on:i=180:gtg=position_2995 on theBenchmark for (2995ds/180Mi)
% 3.49/2.00 % (1534493)Instruction limit reached!
% 3.49/2.00 % (1534493)------------------------------
% 3.49/2.00 % (1534493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.49/2.00 % (1534493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/2.00 % (1534493)CaDiCaL version: 2.1.3
% 3.49/2.00 % (1534493)Termination reason: Instruction limit
% 3.49/2.00 % (1534493)Termination phase: Property scanning
% 3.49/2.00 % (1534493)Time elapsed: 0.041 s
% 3.49/2.00 % (1534493)Peak memory usage: 84 MB
% 3.49/2.00 % (1534493)Instructions burned: 108 (million)
% 3.49/2.00 % (1534496)Instruction limit reached!
% 3.49/2.00 % (1534496)------------------------------
% 3.49/2.00 % (1534496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.49/2.00 % (1534496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/2.00 % (1534496)CaDiCaL version: 2.1.3
% 3.49/2.00 % (1534496)Termination reason: Instruction limit
% 3.49/2.00 % (1534496)Termination phase: Property scanning
% 3.49/2.00 % (1534496)Time elapsed: 0.041 s
% 3.49/2.00 % (1534496)Peak memory usage: 84 MB
% 3.49/2.00 % (1534496)Instructions burned: 119 (million)
% 3.49/2.00 % (1534495)Instruction limit reached!
% 3.49/2.00 % (1534495)------------------------------
% 3.49/2.00 % (1534495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.49/2.00 % (1534495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/2.00 % (1534495)CaDiCaL version: 2.1.3
% 3.49/2.00 % (1534495)Termination reason: Instruction limit
% 3.49/2.00 % (1534495)Termination phase: Property scanning
% 3.49/2.00 % (1534495)Time elapsed: 0.057 s
% 3.49/2.00 % (1534495)Peak memory usage: 84 MB
% 3.49/2.00 % (1534495)Instructions burned: 182 (million)
% 3.49/2.00 % (1534499)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=1758926158:i=143:sd=2:aac=none:ss=axioms:sgt=16_2994 on theBenchmark for (2994ds/143Mi)
% 3.49/2.00 % (1534499)Instruction limit reached!
% 3.49/2.00 % (1534499)------------------------------
% 3.49/2.00 % (1534499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.49/2.00 % (1534499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/2.00 % (1534499)CaDiCaL version: 2.1.3
% 3.49/2.00 % (1534499)Termination reason: Instruction limit
% 3.49/2.00 % (1534499)Termination phase: Property scanning
% 3.49/2.00 % (1534499)Time elapsed: 0.027 s
% 3.49/2.00 % (1534499)Peak memory usage: 84 MB
% 3.49/2.00 % (1534499)Instructions burned: 145 (million)
% 12.23/3.01 % (1534506)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2328013541:st=4:i=219:sd=3:ss=axioms_2993 on theBenchmark for (2993ds/219Mi)
% 12.23/3.01 % (1534505)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2281406986:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2993 on theBenchmark for (2993ds/189Mi)
% 12.23/3.01 % (1534509)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1549741211:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 12.23/3.01 % (1534508)lrs+10_64_to=lpo:sil=8000:random_seed=4032534171:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 12.23/3.01 % (1534509)Instruction limit reached!
% 12.23/3.01 % (1534509)------------------------------
% 12.23/3.01 % (1534509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534509)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534509)Termination reason: Instruction limit
% 12.23/3.01 % (1534509)Termination phase: Property scanning
% 12.23/3.01 % (1534509)Time elapsed: 0.032 s
% 12.23/3.01 % (1534509)Peak memory usage: 85 MB
% 12.23/3.01 % (1534509)Instructions burned: 198 (million)
% 12.23/3.01 % (1534508)Instruction limit reached!
% 12.23/3.01 % (1534508)------------------------------
% 12.23/3.01 % (1534508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534508)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534508)Termination reason: Instruction limit
% 12.23/3.01 % (1534508)Termination phase: Property scanning
% 12.23/3.01 % (1534508)Time elapsed: 0.039 s
% 12.23/3.01 % (1534508)Peak memory usage: 85 MB
% 12.23/3.01 % (1534508)Instructions burned: 126 (million)
% 12.23/3.01 % (1534506)Instruction limit reached!
% 12.23/3.01 % (1534506)------------------------------
% 12.23/3.01 % (1534506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534506)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534506)Termination reason: Instruction limit
% 12.23/3.01 % (1534506)Termination phase: Property scanning
% 12.23/3.01 % (1534506)Time elapsed: 0.079 s
% 12.23/3.01 % (1534506)Peak memory usage: 84 MB
% 12.23/3.01 % (1534506)Instructions burned: 221 (million)
% 12.23/3.01 % (1534505)Instruction limit reached!
% 12.23/3.01 % (1534505)------------------------------
% 12.23/3.01 % (1534505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534505)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534505)Termination reason: Instruction limit
% 12.23/3.01 % (1534505)Termination phase: Property scanning
% 12.23/3.01 % (1534505)Time elapsed: 0.082 s
% 12.23/3.01 % (1534505)Peak memory usage: 84 MB
% 12.23/3.01 % (1534505)Instructions burned: 192 (million)
% 12.23/3.01 % (1534514)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2683227614:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi)
% 12.23/3.01 % (1534514)Instruction limit reached!
% 12.23/3.01 % (1534514)------------------------------
% 12.23/3.01 % (1534514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534514)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534514)Termination reason: Instruction limit
% 12.23/3.01 % (1534514)Termination phase: Property scanning
% 12.23/3.01 % (1534514)Time elapsed: 0.026 s
% 12.23/3.01 % (1534514)Peak memory usage: 84 MB
% 12.23/3.01 % (1534514)Instructions burned: 158 (million)
% 12.23/3.01 % (1534515)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1664924907:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 12.23/3.01 % (1534517)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1064699061:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 12.23/3.01 % (1534516)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=3931540116:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 12.23/3.01 % (1534519)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=345790573:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 12.23/3.01 % (1534517)Instruction limit reached!
% 12.23/3.01 % (1534517)------------------------------
% 12.23/3.01 % (1534517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534517)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534517)Termination reason: Instruction limit
% 12.23/3.01 % (1534517)Termination phase: Property scanning
% 12.23/3.01 % (1534517)Time elapsed: 0.034 s
% 12.23/3.01 % (1534517)Peak memory usage: 85 MB
% 12.23/3.01 % (1534517)Instructions burned: 108 (million)
% 12.23/3.01 % (1534516)Instruction limit reached!
% 12.23/3.01 % (1534516)------------------------------
% 12.23/3.01 % (1534516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534516)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534516)Termination reason: Instruction limit
% 12.23/3.01 % (1534516)Termination phase: SInE selection
% 12.23/3.01 % (1534516)Time elapsed: 0.046 s
% 12.23/3.01 % (1534516)Peak memory usage: 84 MB
% 12.23/3.01 % (1534516)Instructions burned: 106 (million)
% 12.23/3.01 % (1534519)Instruction limit reached!
% 12.23/3.01 % (1534519)------------------------------
% 12.23/3.01 % (1534519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534519)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534519)Termination reason: Instruction limit
% 12.23/3.01 % (1534519)Termination phase: Property scanning
% 12.23/3.01 % (1534519)Time elapsed: 0.040 s
% 12.23/3.01 % (1534519)Peak memory usage: 84 MB
% 12.23/3.01 % (1534519)Instructions burned: 245 (million)
% 12.23/3.01 % (1534526)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=63018632:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 12.23/3.01 % (1534524)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3024197788:cond=fast:i=5208:av=off_2989 on theBenchmark for (2989ds/5208Mi)
% 12.23/3.01 % (1534525)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4206120722:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 12.23/3.01 % (1534526)Instruction limit reached!
% 12.23/3.01 % (1534526)------------------------------
% 12.23/3.01 % (1534526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534526)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534526)Termination reason: Instruction limit
% 12.23/3.01 % (1534526)Termination phase: Saturation
% 12.23/3.01 % (1534526)Time elapsed: 0.086 s
% 12.23/3.01 % (1534526)Peak memory usage: 88 MB
% 12.23/3.01 % (1534526)Instructions burned: 502 (million)
% 12.23/3.01 % (1534525)Instruction limit reached!
% 12.23/3.01 % (1534525)------------------------------
% 12.23/3.01 % (1534525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534525)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534525)Termination reason: Instruction limit
% 12.23/3.01 % (1534525)Termination phase: Property scanning
% 12.23/3.01 % (1534525)Time elapsed: 0.049 s
% 12.23/3.01 % (1534525)Peak memory usage: 84 MB
% 12.23/3.01 % (1534525)Instructions burned: 135 (million)
% 12.23/3.01 % (1534530)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2402554208:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 12.23/3.01 % (1534530)Instruction limit reached!
% 12.23/3.01 % (1534530)------------------------------
% 12.23/3.01 % (1534530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534530)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534530)Termination reason: Instruction limit
% 12.23/3.01 % (1534530)Termination phase: Property scanning
% 12.23/3.01 % (1534530)Time elapsed: 0.032 s
% 12.23/3.01 % (1534530)Peak memory usage: 85 MB
% 12.23/3.01 % (1534530)Instructions burned: 196 (million)
% 12.23/3.01 % (1534531)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2669620158:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 12.23/3.01 % (1534533)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4275264692:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 12.23/3.01 % (1534531)Instruction limit reached!
% 12.23/3.01 % (1534531)------------------------------
% 12.23/3.01 % (1534531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534531)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534531)Termination reason: Instruction limit
% 12.23/3.01 % (1534531)Termination phase: Saturation
% 12.23/3.01 % (1534531)Time elapsed: 0.085 s
% 12.23/3.01 % (1534531)Peak memory usage: 87 MB
% 12.23/3.01 % (1534531)Instructions burned: 265 (million)
% 12.23/3.01 % (1534533)Instruction limit reached!
% 12.23/3.01 % (1534533)------------------------------
% 12.23/3.01 % (1534533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534533)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534533)Termination reason: Instruction limit
% 12.23/3.01 % (1534533)Termination phase: Property scanning
% 12.23/3.01 % (1534533)Time elapsed: 0.026 s
% 12.23/3.01 % (1534533)Peak memory usage: 84 MB
% 12.23/3.01 % (1534533)Instructions burned: 159 (million)
% 12.23/3.01 % (1534537)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1178710115:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi)
% 12.23/3.01 % (1534536)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=3104741148:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi)
% 12.23/3.01 % (1534537)Instruction limit reached!
% 12.23/3.01 % (1534537)------------------------------
% 12.23/3.01 % (1534537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534537)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534537)Termination reason: Instruction limit
% 12.23/3.01 % (1534537)Termination phase: Saturation
% 12.23/3.01 % (1534537)Time elapsed: 0.096 s
% 12.23/3.01 % (1534537)Peak memory usage: 88 MB
% 12.23/3.01 % (1534537)Instructions burned: 538 (million)
% 12.23/3.01 % (1534540)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3675480511:i=180:bd=preordered:av=off_2983 on theBenchmark for (2983ds/180Mi)
% 12.23/3.01 % (1534540)Instruction limit reached!
% 12.23/3.01 % (1534540)------------------------------
% 12.23/3.01 % (1534540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.01 % (1534540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.01 % (1534540)CaDiCaL version: 2.1.3
% 12.23/3.01 % (1534540)Termination reason: Instruction limit
% 12.23/3.01 % (1534540)Termination phase: Property scanning
% 12.23/3.01 % (1534540)Time elapsed: 0.030 s
% 12.23/3.01 % (1534540)Peak memory usage: 85 MB
% 12.23/3.01 % (1534540)Instructions burned: 186 (million)
% 12.23/3.01 % (1534542)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=4181209714:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2982 on theBenchmark for (2982ds/10307Mi)
% 12.23/3.01 % (1534490)First to succeed.
% 12.23/3.01 % (1534490)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1534485"
% 12.23/3.01 % (1534491)Also succeeded, but the first one will report.
% 12.23/3.01 % (1534515)Also succeeded, but the first one will report.
% 12.23/3.01 % (1534490)Refutation found. Thanks to Tanya!
% 12.23/3.01 % SZS status Unsatisfiable for theBenchmark
% 12.23/3.01 % SZS output start Proof for theBenchmark
% See solution above
% 14.55/3.23 % (1534490)------------------------------
% 14.55/3.23 % (1534490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/3.23 % (1534490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/3.23 % (1534490)CaDiCaL version: 2.1.3
% 14.55/3.23 % (1534490)Termination reason: Refutation
% 14.55/3.23 % (1534490)Time elapsed: 1.507 s
% 14.55/3.23 % (1534490)Peak memory usage: 138 MB
% 14.55/3.23 % (1534490)Instructions burned: 2855 (million)
% 14.55/3.23 % (1534490)------------------------------
% 14.55/3.23 % (1534490)------------------------------
% 14.55/3.23 % (1534485)Success in time 2.344 s
% 14.55/3.23 % Vampire exiting
%------------------------------------------------------------------------------