%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR039-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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 09:44:32 AM UTC 2026
% Result : Unsatisfiable 134.43s 25.17s
% Output : Refutation 134.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 34
% Syntax : Number of formulae : 174 ( 174 unt; 0 def)
% Number of atoms : 174 ( 173 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 1 ( 1 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 31 con; 0-4 aty)
% Number of variables : 74 ( 74 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq4(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f2,axiom,
! [X2,X0,X1] : ifeq3(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom_001) ).
fof(f28,axiom,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_14) ).
fof(f29,plain,
true = genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
inference(reorient_equations,[],[f28]) ).
fof(f46,axiom,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_23) ).
fof(f47,plain,
true = genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
inference(reorient_equations,[],[f46]) ).
fof(f82,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_41) ).
fof(f83,plain,
true = genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(reorient_equations,[],[f82]) ).
fof(f86,axiom,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_43) ).
fof(f87,plain,
true = genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
inference(reorient_equations,[],[f86]) ).
fof(f144,axiom,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_72) ).
fof(f145,plain,
true = genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
inference(reorient_equations,[],[f144]) ).
fof(f156,axiom,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_78) ).
fof(f157,plain,
true = genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
inference(reorient_equations,[],[f156]) ).
fof(f218,axiom,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_109) ).
fof(f219,plain,
true = genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
inference(reorient_equations,[],[f218]) ).
fof(f290,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_145) ).
fof(f291,plain,
true = genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(reorient_equations,[],[f290]) ).
fof(f304,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_152) ).
fof(f305,plain,
true = disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(reorient_equations,[],[f304]) ).
fof(f346,axiom,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_175) ).
fof(f347,plain,
true = genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
inference(reorient_equations,[],[f346]) ).
fof(f360,axiom,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_182) ).
fof(f361,plain,
true = genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
inference(reorient_equations,[],[f360]) ).
fof(f378,axiom,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_191) ).
fof(f379,plain,
true = genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
inference(reorient_equations,[],[f378]) ).
fof(f412,axiom,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_208) ).
fof(f413,plain,
true = genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
inference(reorient_equations,[],[f412]) ).
fof(f506,axiom,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_255) ).
fof(f507,plain,
true = genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
inference(reorient_equations,[],[f506]) ).
fof(f566,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_285) ).
fof(f567,plain,
true = genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(reorient_equations,[],[f566]) ).
fof(f684,axiom,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_345) ).
fof(f685,plain,
true = genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
inference(reorient_equations,[],[f684]) ).
fof(f690,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_348) ).
fof(f691,plain,
true = genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(reorient_equations,[],[f690]) ).
fof(f696,axiom,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_351) ).
fof(f697,plain,
true = genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
inference(reorient_equations,[],[f696]) ).
fof(f700,axiom,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_353) ).
fof(f701,plain,
true = genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
inference(reorient_equations,[],[f700]) ).
fof(f732,axiom,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_370) ).
fof(f733,plain,
true = genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
inference(reorient_equations,[],[f732]) ).
fof(f736,axiom,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_372) ).
fof(f737,plain,
true = genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
inference(reorient_equations,[],[f736]) ).
fof(f744,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_376) ).
fof(f745,plain,
true = genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(reorient_equations,[],[f744]) ).
fof(f750,axiom,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_379) ).
fof(f751,plain,
true = genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
inference(reorient_equations,[],[f750]) ).
fof(f762,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_385) ).
fof(f763,plain,
true = genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(reorient_equations,[],[f762]) ).
fof(f826,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_417) ).
fof(f827,plain,
true = genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(reorient_equations,[],[f826]) ).
fof(f944,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_476) ).
fof(f945,plain,
true = genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(reorient_equations,[],[f944]) ).
fof(f958,axiom,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_483) ).
fof(f959,plain,
true = genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
inference(reorient_equations,[],[f958]) ).
fof(f2202,axiom,
! [X2,X0,X1] : ifeq4(genls(X0,X1),true,ifeq4(genls(X2,X0),true,genls(X2,X1),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_1109) ).
fof(f2203,plain,
! [X2,X0,X1] : true = ifeq4(genls(X0,X1),true,ifeq4(genls(X2,X0),true,genls(X2,X1),true),true),
inference(reorient_equations,[],[f2202]) ).
fof(f2224,axiom,
! [X0,X1] : ifeq4(disjointwith(X0,X1),true,disjointwith(X1,X0),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_1120) ).
fof(f2225,plain,
! [X0,X1] : true = ifeq4(disjointwith(X0,X1),true,disjointwith(X1,X0),true),
inference(reorient_equations,[],[f2224]) ).
fof(f2226,axiom,
! [X2,X0,X1] : ifeq4(genls(X0,X1),true,ifeq4(disjointwith(X2,X1),true,disjointwith(X2,X0),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_1121) ).
fof(f2227,plain,
! [X2,X0,X1] : true = ifeq4(genls(X0,X1),true,ifeq4(disjointwith(X2,X1),true,disjointwith(X2,X0),true),true),
inference(reorient_equations,[],[f2226]) ).
fof(f2268,negated_conjecture,
ifeq3(disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),true,a,b) = b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query89_1) ).
fof(f2269,plain,
b = ifeq3(disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),true,a,b),
inference(reorient_equations,[],[f2268]) ).
fof(f2270,negated_conjecture,
a != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f66685,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_6_92162,X0),true,ifeq4(true,true,genls(c_tptpcol_7_93186,X0),true),true),
inference(superposition,[],[f2203,f29]) ).
fof(f66687,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_5_90114,X0),true,ifeq4(true,true,genls(c_tptpcol_6_92162,X0),true),true),
inference(superposition,[],[f2203,f827]) ).
fof(f66721,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_2_65537,X0),true,ifeq4(true,true,genls(c_tptpcol_3_81921,X0),true),true),
inference(superposition,[],[f2203,f83]) ).
fof(f66750,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_11_93764,X0),true,ifeq4(true,true,genls(c_tptpcol_12_93765,X0),true),true),
inference(superposition,[],[f2203,f145]) ).
fof(f66752,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_10_93700,X0),true,ifeq4(true,true,genls(c_tptpcol_11_93764,X0),true),true),
inference(superposition,[],[f2203,f737]) ).
fof(f66762,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_12_93765,X0),true,ifeq4(true,true,genls(c_tptpcol_13_93766,X0),true),true),
inference(superposition,[],[f2203,f157]) ).
fof(f66830,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_14_93774,X0),true,ifeq4(true,true,genls(c_tptpcol_15_93775,X0),true),true),
inference(superposition,[],[f2203,f361]) ).
fof(f66832,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_13_93766,X0),true,ifeq4(true,true,genls(c_tptpcol_14_93774,X0),true),true),
inference(superposition,[],[f2203,f379]) ).
fof(f66923,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_7_93186,X0),true,ifeq4(true,true,genls(c_tptpcol_8_93698,X0),true),true),
inference(superposition,[],[f2203,f685]) ).
fof(f66934,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_8_93698,X0),true,ifeq4(true,true,genls(c_tptpcol_9_93699,X0),true),true),
inference(superposition,[],[f2203,f733]) ).
fof(f66936,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_9_93699,X0),true,ifeq4(true,true,genls(c_tptpcol_10_93700,X0),true),true),
inference(superposition,[],[f2203,f751]) ).
fof(f66938,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_3_81921,X0),true,ifeq4(true,true,genls(c_tptpcol_4_90113,X0),true),true),
inference(superposition,[],[f2203,f745]) ).
fof(f66957,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_4_90113,X0),true,ifeq4(true,true,genls(c_tptpcol_5_90114,X0),true),true),
inference(superposition,[],[f2203,f945]) ).
fof(f67622,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_4_90113,X0),true,genls(c_tptpcol_5_90114,X0),true),
inference(forward_demodulation,[],[f66957,f1]) ).
fof(f67641,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_3_81921,X0),true,genls(c_tptpcol_4_90113,X0),true),
inference(forward_demodulation,[],[f66938,f1]) ).
fof(f67643,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_9_93699,X0),true,genls(c_tptpcol_10_93700,X0),true),
inference(forward_demodulation,[],[f66936,f1]) ).
fof(f67645,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_8_93698,X0),true,genls(c_tptpcol_9_93699,X0),true),
inference(forward_demodulation,[],[f66934,f1]) ).
fof(f67656,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_7_93186,X0),true,genls(c_tptpcol_8_93698,X0),true),
inference(forward_demodulation,[],[f66923,f1]) ).
fof(f67747,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_13_93766,X0),true,genls(c_tptpcol_14_93774,X0),true),
inference(forward_demodulation,[],[f66832,f1]) ).
fof(f67749,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_14_93774,X0),true,genls(c_tptpcol_15_93775,X0),true),
inference(forward_demodulation,[],[f66830,f1]) ).
fof(f67817,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_12_93765,X0),true,genls(c_tptpcol_13_93766,X0),true),
inference(forward_demodulation,[],[f66762,f1]) ).
fof(f67827,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_10_93700,X0),true,genls(c_tptpcol_11_93764,X0),true),
inference(forward_demodulation,[],[f66752,f1]) ).
fof(f67829,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_11_93764,X0),true,genls(c_tptpcol_12_93765,X0),true),
inference(forward_demodulation,[],[f66750,f1]) ).
fof(f67858,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_2_65537,X0),true,genls(c_tptpcol_3_81921,X0),true),
inference(forward_demodulation,[],[f66721,f1]) ).
fof(f67892,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_5_90114,X0),true,genls(c_tptpcol_6_92162,X0),true),
inference(forward_demodulation,[],[f66687,f1]) ).
fof(f67894,plain,
! [X0] : true = ifeq4(genls(c_tptpcol_6_92162,X0),true,genls(c_tptpcol_7_93186,X0),true),
inference(forward_demodulation,[],[f66685,f1]) ).
fof(f70108,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(X0,c_tptpcol_4_16387),true,disjointwith(X0,c_tptpcol_5_16388),true),true),
inference(superposition,[],[f2227,f47]) ).
fof(f70110,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(X0,c_tptpcol_3_16386),true,disjointwith(X0,c_tptpcol_4_16387),true),true),
inference(superposition,[],[f2227,f567]) ).
fof(f70136,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(X0,c_tptpcol_9_18439),true,disjointwith(X0,c_tptpcol_10_18567),true),true),
inference(superposition,[],[f2227,f87]) ).
fof(f70138,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(X0,c_tptpcol_8_18438),true,disjointwith(X0,c_tptpcol_9_18439),true),true),
inference(superposition,[],[f2227,f507]) ).
fof(f70189,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(X0,c_tptpcol_11_18631),true,disjointwith(X0,c_tptpcol_12_18663),true),true),
inference(superposition,[],[f2227,f219]) ).
fof(f70191,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(X0,c_tptpcol_10_18567),true,disjointwith(X0,c_tptpcol_11_18631),true),true),
inference(superposition,[],[f2227,f347]) ).
fof(f70219,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(X0,c_tptpcol_1_1),true,disjointwith(X0,c_tptpcol_2_2),true),true),
inference(superposition,[],[f2227,f291]) ).
fof(f70258,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(X0,c_tptpcol_12_18663),true,disjointwith(X0,c_tptpcol_13_18664),true),true),
inference(superposition,[],[f2227,f413]) ).
fof(f70268,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(X0,c_tptpcol_2_2),true,disjointwith(X0,c_tptpcol_3_16386),true),true),
inference(superposition,[],[f2227,f763]) ).
fof(f70287,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(X0,c_tptpcol_7_18437),true,disjointwith(X0,c_tptpcol_8_18438),true),true),
inference(superposition,[],[f2227,f701]) ).
fof(f70336,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(X0,c_tptpcol_5_16388),true,disjointwith(X0,c_tptpcol_6_18436),true),true),
inference(superposition,[],[f2227,f697]) ).
fof(f70338,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(X0,c_tptpcol_6_18436),true,disjointwith(X0,c_tptpcol_7_18437),true),true),
inference(superposition,[],[f2227,f959]) ).
fof(f70399,plain,
! [X0] : true = ifeq4(genls(X0,c_tptpcol_1_65536),true,ifeq4(true,true,disjointwith(c_tptpcol_1_1,X0),true),true),
inference(superposition,[],[f2227,f305]) ).
fof(f70425,plain,
! [X0] : true = ifeq4(genls(X0,c_tptpcol_1_65536),true,disjointwith(c_tptpcol_1_1,X0),true),
inference(forward_demodulation,[],[f70399,f1]) ).
fof(f70486,plain,
! [X0] : true = ifeq4(disjointwith(X0,c_tptpcol_6_18436),true,disjointwith(X0,c_tptpcol_7_18437),true),
inference(forward_demodulation,[],[f70338,f1]) ).
fof(f70488,plain,
! [X0] : true = ifeq4(disjointwith(X0,c_tptpcol_5_16388),true,disjointwith(X0,c_tptpcol_6_18436),true),
inference(forward_demodulation,[],[f70336,f1]) ).
fof(f70537,plain,
! [X0] : true = ifeq4(disjointwith(X0,c_tptpcol_7_18437),true,disjointwith(X0,c_tptpcol_8_18438),true),
inference(forward_demodulation,[],[f70287,f1]) ).
fof(f70556,plain,
! [X0] : true = ifeq4(disjointwith(X0,c_tptpcol_2_2),true,disjointwith(X0,c_tptpcol_3_16386),true),
inference(forward_demodulation,[],[f70268,f1]) ).
fof(f70566,plain,
! [X0] : true = ifeq4(disjointwith(X0,c_tptpcol_12_18663),true,disjointwith(X0,c_tptpcol_13_18664),true),
inference(forward_demodulation,[],[f70258,f1]) ).
fof(f70605,plain,
! [X0] : true = ifeq4(disjointwith(X0,c_tptpcol_1_1),true,disjointwith(X0,c_tptpcol_2_2),true),
inference(forward_demodulation,[],[f70219,f1]) ).
fof(f70633,plain,
! [X0] : true = ifeq4(disjointwith(X0,c_tptpcol_10_18567),true,disjointwith(X0,c_tptpcol_11_18631),true),
inference(forward_demodulation,[],[f70191,f1]) ).
fof(f70635,plain,
! [X0] : true = ifeq4(disjointwith(X0,c_tptpcol_11_18631),true,disjointwith(X0,c_tptpcol_12_18663),true),
inference(forward_demodulation,[],[f70189,f1]) ).
fof(f70686,plain,
! [X0] : true = ifeq4(disjointwith(X0,c_tptpcol_8_18438),true,disjointwith(X0,c_tptpcol_9_18439),true),
inference(forward_demodulation,[],[f70138,f1]) ).
fof(f70688,plain,
! [X0] : true = ifeq4(disjointwith(X0,c_tptpcol_9_18439),true,disjointwith(X0,c_tptpcol_10_18567),true),
inference(forward_demodulation,[],[f70136,f1]) ).
fof(f70714,plain,
! [X0] : true = ifeq4(disjointwith(X0,c_tptpcol_3_16386),true,disjointwith(X0,c_tptpcol_4_16387),true),
inference(forward_demodulation,[],[f70110,f1]) ).
fof(f70716,plain,
! [X0] : true = ifeq4(disjointwith(X0,c_tptpcol_4_16387),true,disjointwith(X0,c_tptpcol_5_16388),true),
inference(forward_demodulation,[],[f70108,f1]) ).
fof(f364433,plain,
true = ifeq4(true,true,genls(c_tptpcol_3_81921,c_tptpcol_1_65536),true),
inference(superposition,[],[f67858,f691]) ).
fof(f364439,plain,
true = genls(c_tptpcol_3_81921,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f364433,f1]) ).
fof(f364444,plain,
true = ifeq4(true,true,genls(c_tptpcol_4_90113,c_tptpcol_1_65536),true),
inference(superposition,[],[f67641,f364439]) ).
fof(f364479,plain,
true = genls(c_tptpcol_4_90113,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f364444,f1]) ).
fof(f364547,plain,
true = ifeq4(true,true,genls(c_tptpcol_5_90114,c_tptpcol_1_65536),true),
inference(superposition,[],[f67622,f364479]) ).
fof(f364582,plain,
true = genls(c_tptpcol_5_90114,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f364547,f1]) ).
fof(f380910,plain,
true = ifeq4(true,true,genls(c_tptpcol_6_92162,c_tptpcol_1_65536),true),
inference(superposition,[],[f67892,f364582]) ).
fof(f380922,plain,
true = genls(c_tptpcol_6_92162,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f380910,f1]) ).
fof(f382743,plain,
true = ifeq4(true,true,genls(c_tptpcol_7_93186,c_tptpcol_1_65536),true),
inference(superposition,[],[f67894,f380922]) ).
fof(f382753,plain,
true = genls(c_tptpcol_7_93186,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f382743,f1]) ).
fof(f383337,plain,
true = ifeq4(true,true,genls(c_tptpcol_8_93698,c_tptpcol_1_65536),true),
inference(superposition,[],[f67656,f382753]) ).
fof(f383372,plain,
true = genls(c_tptpcol_8_93698,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f383337,f1]) ).
fof(f383737,plain,
true = ifeq4(true,true,genls(c_tptpcol_9_93699,c_tptpcol_1_65536),true),
inference(superposition,[],[f67645,f383372]) ).
fof(f383772,plain,
true = genls(c_tptpcol_9_93699,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f383737,f1]) ).
fof(f384225,plain,
true = ifeq4(true,true,genls(c_tptpcol_10_93700,c_tptpcol_1_65536),true),
inference(superposition,[],[f67643,f383772]) ).
fof(f384260,plain,
true = genls(c_tptpcol_10_93700,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f384225,f1]) ).
fof(f385677,plain,
true = ifeq4(true,true,genls(c_tptpcol_11_93764,c_tptpcol_1_65536),true),
inference(superposition,[],[f67827,f384260]) ).
fof(f385713,plain,
true = genls(c_tptpcol_11_93764,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f385677,f1]) ).
fof(f387541,plain,
true = ifeq4(true,true,genls(c_tptpcol_12_93765,c_tptpcol_1_65536),true),
inference(superposition,[],[f67829,f385713]) ).
fof(f387577,plain,
true = genls(c_tptpcol_12_93765,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f387541,f1]) ).
fof(f393154,plain,
true = ifeq4(true,true,genls(c_tptpcol_13_93766,c_tptpcol_1_65536),true),
inference(superposition,[],[f67817,f387577]) ).
fof(f393189,plain,
true = genls(c_tptpcol_13_93766,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f393154,f1]) ).
fof(f396096,plain,
true = ifeq4(true,true,genls(c_tptpcol_14_93774,c_tptpcol_1_65536),true),
inference(superposition,[],[f67747,f393189]) ).
fof(f396131,plain,
true = genls(c_tptpcol_14_93774,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f396096,f1]) ).
fof(f398331,plain,
true = ifeq4(true,true,genls(c_tptpcol_15_93775,c_tptpcol_1_65536),true),
inference(superposition,[],[f67749,f396131]) ).
fof(f398367,plain,
true = genls(c_tptpcol_15_93775,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f398331,f1]) ).
fof(f410596,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_1_1,c_tptpcol_15_93775),true),
inference(superposition,[],[f70425,f398367]) ).
fof(f410652,plain,
true = disjointwith(c_tptpcol_1_1,c_tptpcol_15_93775),
inference(forward_demodulation,[],[f410596,f1]) ).
fof(f415749,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_1_1),true),
inference(superposition,[],[f2225,f410652]) ).
fof(f415760,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_1_1),
inference(forward_demodulation,[],[f415749,f1]) ).
fof(f419437,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_2_2),true),
inference(superposition,[],[f70605,f415760]) ).
fof(f419493,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_2_2),
inference(forward_demodulation,[],[f419437,f1]) ).
fof(f426446,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_3_16386),true),
inference(superposition,[],[f70556,f419493]) ).
fof(f426467,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f426446,f1]) ).
fof(f474903,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_4_16387),true),
inference(superposition,[],[f70714,f426467]) ).
fof(f474959,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_4_16387),
inference(forward_demodulation,[],[f474903,f1]) ).
fof(f506219,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_5_16388),true),
inference(superposition,[],[f70716,f474959]) ).
fof(f506242,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_5_16388),
inference(forward_demodulation,[],[f506219,f1]) ).
fof(f510823,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_6_18436),true),
inference(superposition,[],[f70488,f506242]) ).
fof(f510843,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_6_18436),
inference(forward_demodulation,[],[f510823,f1]) ).
fof(f515407,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_7_18437),true),
inference(superposition,[],[f70486,f510843]) ).
fof(f515427,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_7_18437),
inference(forward_demodulation,[],[f515407,f1]) ).
fof(f519501,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_8_18438),true),
inference(superposition,[],[f70537,f515427]) ).
fof(f519522,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_8_18438),
inference(forward_demodulation,[],[f519501,f1]) ).
fof(f523321,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_9_18439),true),
inference(superposition,[],[f70686,f519522]) ).
fof(f523342,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_9_18439),
inference(forward_demodulation,[],[f523321,f1]) ).
fof(f526420,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_10_18567),true),
inference(superposition,[],[f70688,f523342]) ).
fof(f526441,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_10_18567),
inference(forward_demodulation,[],[f526420,f1]) ).
fof(f529009,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_11_18631),true),
inference(superposition,[],[f70633,f526441]) ).
fof(f529029,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_11_18631),
inference(forward_demodulation,[],[f529009,f1]) ).
fof(f531503,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_12_18663),true),
inference(superposition,[],[f70635,f529029]) ).
fof(f531524,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_12_18663),
inference(forward_demodulation,[],[f531503,f1]) ).
fof(f533157,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),true),
inference(superposition,[],[f70566,f531524]) ).
fof(f533177,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),
inference(forward_demodulation,[],[f533157,f1]) ).
fof(f534547,plain,
b = ifeq3(true,true,a,b),
inference(superposition,[],[f2269,f533177]) ).
fof(f534569,plain,
a = b,
inference(forward_demodulation,[],[f534547,f2]) ).
fof(f534570,plain,
$false,
inference(forward_subsumption_resolution,[],[f534569,f2270]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR039-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.28 % Computer : n011.cluster.edu
% 0.12/0.28 % Model : x86_64 x86_64
% 0.12/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.28 % Memory : 8046.5625MB
% 0.12/0.28 % OS : Linux 6.8.0-71-generic
% 0.12/0.28 % CPULimit : 300
% 0.12/0.28 % WCLimit : 300
% 0.12/0.28 % DateTime : Mon Sep 28 22:14:46 UTC 2026
% 0.12/0.28 % CPUTime :
% 0.12/0.29 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.28/0.34 Running first-order model finding
% 0.28/0.34 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.05/4.24 % (3841496)Will run a generic schedule for satisfiability detection.
% 27.05/4.24 % (3841505)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2579981815:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 27.05/4.24 % (3841502)% WARNING: option uhcvi not known.
% 27.05/4.24 % (3841502)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1562860024:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 27.05/4.24 % (3841507)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=10930101:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 27.05/4.24 % (3841501)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3800523048_2999 on theBenchmark for (2999ds/0Mi)
% 27.05/4.24 % (3841506)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2940121217:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 27.05/4.24 % (3841504)dis+10_1_sil=32000:sp=arity:random_seed=1331506834:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 27.05/4.24 % (3841503)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=330938996:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 27.05/4.24 % (3841505)Instruction limit reached!
% 27.05/4.24 % (3841505)------------------------------
% 27.05/4.24 % (3841505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.05/4.24 % (3841505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.05/4.24 % (3841505)CaDiCaL version: 2.1.3
% 27.05/4.24 % (3841505)Termination reason: Instruction limit
% 27.05/4.24 % (3841505)Termination phase: Saturation
% 27.05/4.24 % (3841505)Time elapsed: 0.054 s
% 27.05/4.24 % (3841505)Peak memory usage: 14 MB
% 27.05/4.24 % (3841505)Instructions burned: 117 (million)
% 27.05/4.24 % (3841515)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=778637135:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 27.05/4.24 % (3841504)Instruction limit reached!
% 27.05/4.24 % (3841504)------------------------------
% 27.05/4.24 % (3841504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.05/4.24 % (3841504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.05/4.24 % (3841504)CaDiCaL version: 2.1.3
% 27.05/4.24 % (3841504)Termination reason: Instruction limit
% 27.05/4.24 % (3841504)Termination phase: Saturation
% 27.05/4.24 % (3841504)Time elapsed: 0.094 s
% 27.05/4.24 % (3841504)Peak memory usage: 13 MB
% 27.05/4.24 % (3841504)Instructions burned: 104 (million)
% 27.05/4.24 % (3841506)Instruction limit reached!
% 27.05/4.24 % (3841506)------------------------------
% 27.05/4.24 % (3841506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.05/4.24 % (3841506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.05/4.24 % (3841506)CaDiCaL version: 2.1.3
% 27.05/4.24 % (3841506)Termination reason: Instruction limit
% 27.05/4.24 % (3841506)Termination phase: Saturation
% 27.05/4.24 % (3841506)Time elapsed: 0.135 s
% 27.05/4.24 % (3841506)Peak memory usage: 14 MB
% 27.05/4.24 % (3841506)Instructions burned: 132 (million)
% 27.05/4.24 % (3841507)Instruction limit reached!
% 27.05/4.24 % (3841507)------------------------------
% 27.05/4.24 % (3841507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.05/4.24 % (3841507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.05/4.24 % (3841507)CaDiCaL version: 2.1.3
% 27.05/4.24 % (3841507)Termination reason: Instruction limit
% 27.05/4.24 % (3841507)Termination phase: Saturation
% 27.05/4.24 % (3841507)Time elapsed: 0.144 s
% 27.05/4.24 % (3841507)Peak memory usage: 13 MB
% 27.05/4.24 % (3841507)Instructions burned: 159 (million)
% 27.05/4.24 % (3841517)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2832500320:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 27.05/4.24 % TRYING [1]
% 27.05/4.24 % (3841519)ott-21_1_sil=16000:fs=off:random_seed=3869725487:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 27.05/4.24 % TRYING [2]
% 27.05/4.24 % (3841518)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=375821700:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 27.05/4.24 % TRYING [1]
% 27.05/4.24 % TRYING [2]
% 27.05/4.24 % TRYING [3]
% 27.05/4.24 % (3841517)Instruction limit reached!
% 27.05/4.24 % (3841517)------------------------------
% 27.05/4.24 % (3841517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.05/4.24 % (3841517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.89/9.48 % (3841517)CaDiCaL version: 2.1.3
% 63.89/9.48 % (3841517)Termination reason: Instruction limit
% 63.89/9.48 % (3841517)Termination phase: Saturation
% 63.89/9.48 % (3841517)Time elapsed: 0.130 s
% 63.89/9.48 % (3841517)Peak memory usage: 14 MB
% 63.89/9.48 % (3841517)Instructions burned: 132 (million)
% 63.89/9.48 % (3841523)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3509393094:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 63.89/9.48 % (3841515)Instruction limit reached!
% 63.89/9.48 % (3841515)------------------------------
% 63.89/9.48 % (3841515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.89/9.48 % (3841515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.89/9.48 % (3841515)CaDiCaL version: 2.1.3
% 63.89/9.48 % (3841515)Termination reason: Instruction limit
% 63.89/9.48 % (3841515)Termination phase: Finite model building constraint generation
% 63.89/9.48 % (3841515)Time elapsed: 0.281 s
% 63.89/9.48 % (3841515)Peak memory usage: 30 MB
% 63.89/9.48 % (3841515)Instructions burned: 714 (million)
% 63.89/9.48 % TRYING [3]
% 63.89/9.48 % (3841519)Instruction limit reached!
% 63.89/9.48 % (3841519)------------------------------
% 63.89/9.48 % (3841519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.89/9.48 % (3841519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.89/9.48 % (3841519)CaDiCaL version: 2.1.3
% 63.89/9.48 % (3841519)Termination reason: Instruction limit
% 63.89/9.48 % (3841519)Termination phase: Saturation
% 63.89/9.48 % (3841519)Time elapsed: 0.168 s
% 63.89/9.48 % (3841519)Peak memory usage: 15 MB
% 63.89/9.48 % (3841519)Instructions burned: 180 (million)
% 63.89/9.48 % (3841525)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2955857591:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 63.89/9.48 % (3841526)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4189329880:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 63.89/9.48 % TRYING [1]
% 63.89/9.48 % TRYING [2]
% 63.89/9.48 % TRYING [3]
% 63.89/9.48 % (3841525)Instruction limit reached!
% 63.89/9.48 % (3841525)------------------------------
% 63.89/9.48 % (3841525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.89/9.48 % (3841525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.89/9.48 % (3841525)CaDiCaL version: 2.1.3
% 63.89/9.48 % (3841525)Termination reason: Instruction limit
% 63.89/9.48 % (3841525)Termination phase: Finite model building constraint generation
% 63.89/9.48 % (3841525)Time elapsed: 0.340 s
% 63.89/9.48 % (3841525)Peak memory usage: 31 MB
% 63.89/9.48 % (3841525)Instructions burned: 869 (million)
% 63.89/9.48 % (3841529)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3128032281:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 63.89/9.48 % (3841523)Instruction limit reached!
% 63.89/9.48 % (3841523)------------------------------
% 63.89/9.48 % (3841523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.89/9.48 % (3841523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.89/9.48 % (3841523)CaDiCaL version: 2.1.3
% 63.89/9.48 % (3841523)Termination reason: Instruction limit
% 63.89/9.48 % (3841523)Termination phase: Saturation
% 63.89/9.48 % (3841523)Time elapsed: 0.455 s
% 63.89/9.48 % (3841523)Peak memory usage: 18 MB
% 63.89/9.48 % (3841523)Instructions burned: 478 (million)
% 63.89/9.48 % (3841518)Instruction limit reached!
% 63.89/9.48 % (3841518)------------------------------
% 63.89/9.48 % (3841518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.89/9.48 % (3841518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.89/9.48 % (3841518)CaDiCaL version: 2.1.3
% 63.89/9.48 % (3841518)Termination reason: Instruction limit
% 63.89/9.48 % (3841518)Termination phase: Saturation
% 63.89/9.48 % (3841518)Time elapsed: 0.621 s
% 63.89/9.48 % (3841518)Peak memory usage: 20 MB
% 63.89/9.48 % (3841518)Instructions burned: 684 (million)
% 63.89/9.48 % (3841531)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=808496268:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 63.89/9.48 % (3841532)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3199399174:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 63.89/9.48 % (3841529)Instruction limit reached!
% 63.89/9.48 % (3841529)------------------------------
% 63.89/9.48 % (3841529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.25/13.46 % (3841529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.25/13.46 % (3841529)CaDiCaL version: 2.1.3
% 92.25/13.46 % (3841529)Termination reason: Instruction limit
% 92.25/13.46 % (3841529)Termination phase: Finite model building constraint generation
% 92.25/13.46 % (3841529)Time elapsed: 0.471 s
% 92.25/13.46 % (3841529)Peak memory usage: 95 MB
% 92.25/13.46 % (3841529)Instructions burned: 890 (million)
% 92.25/13.46 % (3841535)fmb+10_1_sil=64000:random_seed=989988978:i=22061:nm=2:gsp=on_2986 on theBenchmark for (2986ds/22061Mi)
% 92.25/13.46 % (3841526)Instruction limit reached!
% 92.25/13.46 % (3841526)------------------------------
% 92.25/13.46 % (3841526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.25/13.46 % (3841526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.25/13.46 % (3841526)CaDiCaL version: 2.1.3
% 92.25/13.46 % (3841526)Termination reason: Instruction limit
% 92.25/13.46 % (3841526)Termination phase: Saturation
% 92.25/13.46 % (3841526)Time elapsed: 0.947 s
% 92.25/13.46 % (3841526)Peak memory usage: 23 MB
% 92.25/13.46 % (3841526)Instructions burned: 1179 (million)
% 92.25/13.46 % (3841537)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=331400992:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi)
% 92.25/13.46 % (3841531)Instruction limit reached!
% 92.25/13.46 % (3841531)------------------------------
% 92.25/13.46 % (3841531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.25/13.46 % (3841531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.25/13.46 % (3841531)CaDiCaL version: 2.1.3
% 92.25/13.46 % (3841531)Termination reason: Instruction limit
% 92.25/13.46 % (3841531)Termination phase: Saturation
% 92.25/13.46 % (3841531)Time elapsed: 0.603 s
% 92.25/13.46 % (3841531)Peak memory usage: 22 MB
% 92.25/13.46 % (3841531)Instructions burned: 693 (million)
% 92.25/13.46 % TRYING [1]
% 92.25/13.46 % TRYING [2]
% 92.25/13.46 % TRYING [4]
% 92.25/13.46 % (3841539)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2133624222:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 92.25/13.46 % TRYING [20]
% 92.25/13.46 % (3841532)Instruction limit reached!
% 92.25/13.46 % (3841532)------------------------------
% 92.25/13.46 % (3841532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.25/13.46 % (3841532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.25/13.46 % (3841532)CaDiCaL version: 2.1.3
% 92.25/13.46 % (3841532)Termination reason: Instruction limit
% 92.25/13.46 % (3841532)Termination phase: Saturation
% 92.25/13.46 % (3841532)Time elapsed: 0.757 s
% 92.25/13.46 % (3841532)Peak memory usage: 24 MB
% 92.25/13.46 % (3841532)Instructions burned: 879 (million)
% 92.25/13.46 % TRYING [3]
% 92.25/13.46 % (3841541)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=604007537:i=5131_2982 on theBenchmark for (2982ds/5131Mi)
% 92.25/13.46 % TRYING [8]
% 92.25/13.46 % (3841539)Instruction limit reached!
% 92.25/13.46 % (3841539)------------------------------
% 92.25/13.46 % (3841539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.25/13.46 % (3841539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.25/13.46 % (3841539)CaDiCaL version: 2.1.3
% 92.25/13.46 % (3841539)Termination reason: Instruction limit
% 92.25/13.46 % (3841539)Termination phase: Finite model building constraint generation
% 92.25/13.46 % (3841539)Time elapsed: 0.642 s
% 92.25/13.46 % (3841539)Peak memory usage: 54 MB
% 92.25/13.46 % (3841539)Instructions burned: 921 (million)
% 92.25/13.46 % (3841543)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3091977397:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi)
% 92.25/13.46 % TRYING [4]
% 92.25/13.46 % (3841543)Instruction limit reached!
% 92.25/13.46 % (3841543)------------------------------
% 92.25/13.46 % (3841543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.25/13.46 % (3841543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.25/13.46 % (3841543)CaDiCaL version: 2.1.3
% 92.25/13.46 % (3841543)Termination reason: Instruction limit
% 92.25/13.46 % (3841543)Termination phase: Saturation
% 92.25/13.46 % (3841543)Time elapsed: 1.282 s
% 92.25/13.46 % (3841543)Peak memory usage: 26 MB
% 92.25/13.46 % (3841543)Instructions burned: 1472 (million)
% 92.25/13.46 % (3841545)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3391280427:i=6324_2964 on theBenchmark for (2964ds/6324Mi)
% 92.25/13.46 % (3841545)Cannot represent all propositional literals internally
% 92.25/13.46 % (3841545)Refutation not found, incomplete strategy
% 92.25/13.46 % (3841545)------------------------------
% 134.43/25.16 % (3841545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.16 % (3841545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.16 % (3841545)CaDiCaL version: 2.1.3
% 134.43/25.16 % (3841545)Termination reason: Refutation not found, incomplete strategy
% 134.43/25.16 % (3841545)Time elapsed: 0.236 s
% 134.43/25.16 % (3841545)Peak memory usage: 16 MB
% 134.43/25.16 % (3841545)Instructions burned: 256 (million)
% 134.43/25.16 % (3841545)------------------------------
% 134.43/25.16 % (3841545)------------------------------
% 134.43/25.16 % (3841547)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2954346828:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 134.43/25.16 % TRYING [5]
% 134.43/25.16 % TRYING [16]
% 134.43/25.16 % (3841547)Instruction limit reached!
% 134.43/25.16 % (3841547)------------------------------
% 134.43/25.16 % (3841547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.16 % (3841547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.16 % (3841547)CaDiCaL version: 2.1.3
% 134.43/25.16 % (3841547)Termination reason: Instruction limit
% 134.43/25.16 % (3841547)Termination phase: Finite model building constraint generation
% 134.43/25.16 % (3841547)Time elapsed: 1.464 s
% 134.43/25.16 % (3841547)Peak memory usage: 104 MB
% 134.43/25.16 % (3841547)Instructions burned: 2174 (million)
% 134.43/25.16 % (3841549)ott-2_1_sil=16000:newcnf=on:random_seed=1188408801:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2945 on theBenchmark for (2945ds/869Mi)
% 134.43/25.16 % (3841549)Instruction limit reached!
% 134.43/25.16 % (3841549)------------------------------
% 134.43/25.16 % (3841549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.16 % (3841549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.16 % (3841549)CaDiCaL version: 2.1.3
% 134.43/25.16 % (3841549)Termination reason: Instruction limit
% 134.43/25.16 % (3841549)Termination phase: Saturation
% 134.43/25.16 % (3841549)Time elapsed: 0.830 s
% 134.43/25.16 % (3841549)Peak memory usage: 29 MB
% 134.43/25.16 % (3841549)Instructions burned: 870 (million)
% 134.43/25.16 % (3841551)ott+10_1_sil=32000:tgt=ground:random_seed=2066696645:i=5114:av=off_2936 on theBenchmark for (2936ds/5114Mi)
% 134.43/25.16 % (3841541)Instruction limit reached!
% 134.43/25.16 % (3841541)------------------------------
% 134.43/25.16 % (3841541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.16 % (3841541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.16 % (3841541)CaDiCaL version: 2.1.3
% 134.43/25.16 % (3841541)Termination reason: Instruction limit
% 134.43/25.16 % (3841541)Termination phase: Saturation
% 134.43/25.16 % (3841541)Time elapsed: 4.764 s
% 134.43/25.16 % (3841541)Peak memory usage: 58 MB
% 134.43/25.16 % (3841541)Instructions burned: 5132 (million)
% 134.43/25.16 % (3841553)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2888844304:i=54282_2934 on theBenchmark for (2934ds/54282Mi)
% 134.43/25.16 % TRYING [1]
% 134.43/25.16 % TRYING [2]
% 134.43/25.16 % TRYING [3]
% 134.43/25.16 % (3841537)Instruction limit reached!
% 134.43/25.16 % (3841537)------------------------------
% 134.43/25.16 % (3841537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.16 % (3841537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.16 % (3841537)CaDiCaL version: 2.1.3
% 134.43/25.16 % (3841537)Termination reason: Instruction limit
% 134.43/25.17 % (3841537)Termination phase: Finite model building constraint generation
% 134.43/25.17 % (3841537)Time elapsed: 6.045 s
% 134.43/25.17 % (3841537)Peak memory usage: 529 MB
% 134.43/25.17 % (3841537)Instructions burned: 9516 (million)
% 134.43/25.17 % (3841555)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4060742231:i=3512:aac=none_2923 on theBenchmark for (2923ds/3512Mi)
% 134.43/25.17 % TRYING [4]
% 134.43/25.17 % TRYING [6]
% 134.43/25.17 % (3841535)Instruction limit reached!
% 134.43/25.17 % (3841535)------------------------------
% 134.43/25.17 % (3841535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.17 % (3841535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.17 % (3841535)CaDiCaL version: 2.1.3
% 134.43/25.17 % (3841535)Termination reason: Instruction limit
% 134.43/25.17 % (3841535)Termination phase: Finite model building constraint generation
% 134.43/25.17 % (3841535)Time elapsed: 7.666 s
% 134.43/25.17 % (3841535)Peak memory usage: 338 MB
% 134.43/25.17 % (3841535)Instructions burned: 22064 (million)
% 134.43/25.17 % (3841710)dis+21_1_sil=32000:sas=cadical:random_seed=3593047259:i=3773:amm=off_2908 on theBenchmark for (2908ds/3773Mi)
% 134.43/25.17 % TRYING [5]
% 134.43/25.17 % (3841555)Instruction limit reached!
% 134.43/25.17 % (3841555)------------------------------
% 134.43/25.17 % (3841555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.17 % (3841555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.17 % (3841555)CaDiCaL version: 2.1.3
% 134.43/25.17 % (3841555)Termination reason: Instruction limit
% 134.43/25.17 % (3841555)Termination phase: Saturation
% 134.43/25.17 % (3841555)Time elapsed: 1.871 s
% 134.43/25.17 % (3841555)Peak memory usage: 47 MB
% 134.43/25.17 % (3841555)Instructions burned: 3513 (million)
% 134.43/25.17 % (3841712)ott+11_1_sil=16000:gs=on:random_seed=1693258276:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2904 on theBenchmark for (2904ds/2251Mi)
% 134.43/25.17 % (3841551)Instruction limit reached!
% 134.43/25.17 % (3841551)------------------------------
% 134.43/25.17 % (3841551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.17 % (3841551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.17 % (3841551)CaDiCaL version: 2.1.3
% 134.43/25.17 % (3841551)Termination reason: Instruction limit
% 134.43/25.17 % (3841551)Termination phase: Saturation
% 134.43/25.17 % (3841551)Time elapsed: 3.343 s
% 134.43/25.17 % (3841551)Peak memory usage: 84 MB
% 134.43/25.17 % (3841551)Instructions burned: 5115 (million)
% 134.43/25.17 % (3841714)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2327804525:fmbsr=1.6:i=67534_2902 on theBenchmark for (2902ds/67534Mi)
% 134.43/25.17 % TRYING [7]
% 134.43/25.17 % (3841710)Instruction limit reached!
% 134.43/25.17 % (3841710)------------------------------
% 134.43/25.17 % (3841710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.17 % (3841710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.17 % (3841710)CaDiCaL version: 2.1.3
% 134.43/25.17 % (3841710)Termination reason: Instruction limit
% 134.43/25.17 % (3841710)Termination phase: Saturation
% 134.43/25.17 % (3841710)Time elapsed: 1.107 s
% 134.43/25.17 % (3841710)Peak memory usage: 52 MB
% 134.43/25.17 % (3841710)Instructions burned: 3773 (million)
% 134.43/25.17 % (3841716)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3702455663:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2897 on theBenchmark for (2897ds/4591Mi)
% 134.43/25.17 % (3841712)Instruction limit reached!
% 134.43/25.17 % (3841712)------------------------------
% 134.43/25.17 % (3841712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.17 % (3841712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.17 % (3841712)CaDiCaL version: 2.1.3
% 134.43/25.17 % (3841712)Termination reason: Instruction limit
% 134.43/25.17 % (3841712)Termination phase: Saturation
% 134.43/25.17 % (3841712)Time elapsed: 0.916 s
% 134.43/25.17 % (3841712)Peak memory usage: 30 MB
% 134.43/25.17 % (3841712)Instructions burned: 2253 (million)
% 134.43/25.17 % (3841718)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3953921417:i=29340_2894 on theBenchmark for (2894ds/29340Mi)
% 134.43/25.17 % (3841716)Instruction limit reached!
% 134.43/25.17 % (3841716)------------------------------
% 134.43/25.17 % (3841716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.17 % (3841716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.17 % (3841716)CaDiCaL version: 2.1.3
% 134.43/25.17 % (3841716)Termination reason: Instruction limit
% 134.43/25.17 % (3841716)Termination phase: Saturation
% 134.43/25.17 % (3841716)Time elapsed: 1.285 s
% 134.43/25.17 % (3841716)Peak memory usage: 60 MB
% 134.43/25.17 % (3841716)Instructions burned: 4592 (million)
% 134.43/25.17 % (3841720)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4022260519:i=5211_2884 on theBenchmark for (2884ds/5211Mi)
% 134.43/25.17 % (3841720)Instruction limit reached!
% 134.43/25.17 % (3841720)------------------------------
% 134.43/25.17 % (3841720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.17 % (3841720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.17 % (3841720)CaDiCaL version: 2.1.3
% 134.43/25.17 % (3841720)Termination reason: Instruction limit
% 134.43/25.17 % (3841720)Termination phase: Saturation
% 134.43/25.17 % (3841720)Time elapsed: 1.534 s
% 134.43/25.17 % (3841720)Peak memory usage: 64 MB
% 134.43/25.17 % (3841720)Instructions burned: 5213 (million)
% 134.43/25.17 % (3841722)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1119604549:i=5497:nm=2_2869 on theBenchmark for (2869ds/5497Mi)
% 134.43/25.17 % TRYING [17]
% 134.43/25.17 % TRYING [5]
% 134.43/25.17 % (3841722)Instruction limit reached!
% 134.43/25.17 % (3841722)------------------------------
% 134.43/25.17 % (3841722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.17 % (3841722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.17 % (3841722)CaDiCaL version: 2.1.3
% 134.43/25.17 % (3841722)Termination reason: Instruction limit
% 134.43/25.17 % (3841722)Termination phase: Finite model building constraint generation
% 134.43/25.17 % (3841722)Time elapsed: 1.019 s
% 134.43/25.17 % (3841722)Peak memory usage: 285 MB
% 134.43/25.17 % (3841722)Instructions burned: 5502 (million)
% 134.43/25.17 % (3841838)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=254601086:fmbsr=2:i=46332_2858 on theBenchmark for (2858ds/46332Mi)
% 134.43/25.17 % TRYING [15]
% 134.43/25.17 % (3841838)Instruction limit reached!
% 134.43/25.17 % (3841838)------------------------------
% 134.43/25.17 % (3841838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.17 % (3841838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.17 % (3841838)CaDiCaL version: 2.1.3
% 134.43/25.17 % (3841838)Termination reason: Instruction limit
% 134.43/25.17 % (3841838)Termination phase: Finite model building constraint generation
% 134.43/25.17 % (3841838)Time elapsed: 9.251 s
% 134.43/25.17 % (3841838)Peak memory usage: 2822 MB
% 134.43/25.17 % (3841838)Instructions burned: 46334 (million)
% 134.43/25.17 % (3841979)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1467288546:i=14071_2763 on theBenchmark for (2763ds/14071Mi)
% 134.43/25.17 % TRYING [12]
% 134.43/25.17 % (3841718) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3841496-3841718"...
% 134.43/25.17 % (3841718)...printing done.
% 134.43/25.17 % (3841718)Refutation found. Thanks to Tanya!
% 134.43/25.17 % SZS status Unsatisfiable for theBenchmark
% 134.43/25.17 % SZS output start Proof for theBenchmark
% See solution above
% 134.43/25.17 % (3841718)------------------------------
% 134.43/25.17 % (3841718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.43/25.17 % (3841718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.43/25.17 % (3841718)CaDiCaL version: 2.1.3
% 134.43/25.17 % (3841718)Termination reason: Refutation
% 134.43/25.17 % (3841718)Time elapsed: 13.954 s
% 134.43/25.17 % (3841718)Peak memory usage: 305 MB
% 134.43/25.17 % (3841718)Instructions burned: 24285 (million)
% 134.43/25.17 % (3841496)Success in time 24.814 s
% 134.43/25.17 % Vampire exiting
%------------------------------------------------------------------------------