%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n008.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:42:10 AM UTC 2026
% Result : Unsatisfiable 22.06s 7.63s
% Output : Refutation 47.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 33
% Syntax : Number of formulae : 176 ( 176 unt; 0 def)
% Number of atoms : 176 ( 175 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 : 68 ( 68 !; 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(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(f2228,axiom,
! [X2,X0,X1] : ifeq4(genls(X0,X1),true,ifeq4(disjointwith(X1,X2),true,disjointwith(X0,X2),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_1122) ).
fof(f2229,plain,
! [X2,X0,X1] : true = ifeq4(genls(X0,X1),true,ifeq4(disjointwith(X1,X2),true,disjointwith(X0,X2),true),true),
inference(reorient_equations,[],[f2228]) ).
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(f3360,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_6_92162,X0),true,disjointwith(c_tptpcol_7_93186,X0),true),true),
inference(superposition,[],[f2229,f29]) ).
fof(f3361,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_5_90114,X0),true,disjointwith(c_tptpcol_6_92162,X0),true),true),
inference(superposition,[],[f2229,f827]) ).
fof(f3364,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_4_16387,X0),true,disjointwith(c_tptpcol_5_16388,X0),true),true),
inference(superposition,[],[f2229,f47]) ).
fof(f3365,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_3_16386,X0),true,disjointwith(c_tptpcol_4_16387,X0),true),true),
inference(superposition,[],[f2229,f567]) ).
fof(f3376,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_2_65537,X0),true,disjointwith(c_tptpcol_3_81921,X0),true),true),
inference(superposition,[],[f2229,f83]) ).
fof(f3377,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_1_65536,X0),true,disjointwith(c_tptpcol_2_65537,X0),true),true),
inference(superposition,[],[f2229,f691]) ).
fof(f3378,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_9_18439,X0),true,disjointwith(c_tptpcol_10_18567,X0),true),true),
inference(superposition,[],[f2229,f87]) ).
fof(f3379,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_8_18438,X0),true,disjointwith(c_tptpcol_9_18439,X0),true),true),
inference(superposition,[],[f2229,f507]) ).
fof(f3389,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_11_93764,X0),true,disjointwith(c_tptpcol_12_93765,X0),true),true),
inference(superposition,[],[f2229,f145]) ).
fof(f3390,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_10_93700,X0),true,disjointwith(c_tptpcol_11_93764,X0),true),true),
inference(superposition,[],[f2229,f737]) ).
fof(f3393,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_12_93765,X0),true,disjointwith(c_tptpcol_13_93766,X0),true),true),
inference(superposition,[],[f2229,f157]) ).
fof(f3400,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_11_18631,X0),true,disjointwith(c_tptpcol_12_18663,X0),true),true),
inference(superposition,[],[f2229,f219]) ).
fof(f3401,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_10_18567,X0),true,disjointwith(c_tptpcol_11_18631,X0),true),true),
inference(superposition,[],[f2229,f347]) ).
fof(f3415,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_1_1,X0),true,disjointwith(c_tptpcol_2_2,X0),true),true),
inference(superposition,[],[f2229,f291]) ).
fof(f3425,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_14_93774,X0),true,disjointwith(c_tptpcol_15_93775,X0),true),true),
inference(superposition,[],[f2229,f361]) ).
fof(f3426,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_13_93766,X0),true,disjointwith(c_tptpcol_14_93774,X0),true),true),
inference(superposition,[],[f2229,f379]) ).
fof(f3433,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_12_18663,X0),true,disjointwith(c_tptpcol_13_18664,X0),true),true),
inference(superposition,[],[f2229,f413]) ).
fof(f3438,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_2_2,X0),true,disjointwith(c_tptpcol_3_16386,X0),true),true),
inference(superposition,[],[f2229,f763]) ).
fof(f3445,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_7_18437,X0),true,disjointwith(c_tptpcol_8_18438,X0),true),true),
inference(superposition,[],[f2229,f701]) ).
fof(f3464,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_7_93186,X0),true,disjointwith(c_tptpcol_8_93698,X0),true),true),
inference(superposition,[],[f2229,f685]) ).
fof(f3465,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_5_16388,X0),true,disjointwith(c_tptpcol_6_18436,X0),true),true),
inference(superposition,[],[f2229,f697]) ).
fof(f3466,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_6_18436,X0),true,disjointwith(c_tptpcol_7_18437,X0),true),true),
inference(superposition,[],[f2229,f959]) ).
fof(f3469,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_8_93698,X0),true,disjointwith(c_tptpcol_9_93699,X0),true),true),
inference(superposition,[],[f2229,f733]) ).
fof(f3470,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_9_93699,X0),true,disjointwith(c_tptpcol_10_93700,X0),true),true),
inference(superposition,[],[f2229,f751]) ).
fof(f3471,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_3_81921,X0),true,disjointwith(c_tptpcol_4_90113,X0),true),true),
inference(superposition,[],[f2229,f745]) ).
fof(f3478,plain,
! [X0] : true = ifeq4(true,true,ifeq4(disjointwith(c_tptpcol_4_90113,X0),true,disjointwith(c_tptpcol_5_90114,X0),true),true),
inference(superposition,[],[f2229,f945]) ).
fof(f3511,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_4_90113,X0),true,disjointwith(c_tptpcol_5_90114,X0),true),
inference(forward_demodulation,[],[f3478,f1]) ).
fof(f3518,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_3_81921,X0),true,disjointwith(c_tptpcol_4_90113,X0),true),
inference(forward_demodulation,[],[f3471,f1]) ).
fof(f3519,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_9_93699,X0),true,disjointwith(c_tptpcol_10_93700,X0),true),
inference(forward_demodulation,[],[f3470,f1]) ).
fof(f3520,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_8_93698,X0),true,disjointwith(c_tptpcol_9_93699,X0),true),
inference(forward_demodulation,[],[f3469,f1]) ).
fof(f3523,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_6_18436,X0),true,disjointwith(c_tptpcol_7_18437,X0),true),
inference(forward_demodulation,[],[f3466,f1]) ).
fof(f3524,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_5_16388,X0),true,disjointwith(c_tptpcol_6_18436,X0),true),
inference(forward_demodulation,[],[f3465,f1]) ).
fof(f3525,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_7_93186,X0),true,disjointwith(c_tptpcol_8_93698,X0),true),
inference(forward_demodulation,[],[f3464,f1]) ).
fof(f3544,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_7_18437,X0),true,disjointwith(c_tptpcol_8_18438,X0),true),
inference(forward_demodulation,[],[f3445,f1]) ).
fof(f3551,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_2_2,X0),true,disjointwith(c_tptpcol_3_16386,X0),true),
inference(forward_demodulation,[],[f3438,f1]) ).
fof(f3556,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_12_18663,X0),true,disjointwith(c_tptpcol_13_18664,X0),true),
inference(forward_demodulation,[],[f3433,f1]) ).
fof(f3563,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_13_93766,X0),true,disjointwith(c_tptpcol_14_93774,X0),true),
inference(forward_demodulation,[],[f3426,f1]) ).
fof(f3564,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_14_93774,X0),true,disjointwith(c_tptpcol_15_93775,X0),true),
inference(forward_demodulation,[],[f3425,f1]) ).
fof(f3574,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_1_1,X0),true,disjointwith(c_tptpcol_2_2,X0),true),
inference(forward_demodulation,[],[f3415,f1]) ).
fof(f3588,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_10_18567,X0),true,disjointwith(c_tptpcol_11_18631,X0),true),
inference(forward_demodulation,[],[f3401,f1]) ).
fof(f3589,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_11_18631,X0),true,disjointwith(c_tptpcol_12_18663,X0),true),
inference(forward_demodulation,[],[f3400,f1]) ).
fof(f3596,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_12_93765,X0),true,disjointwith(c_tptpcol_13_93766,X0),true),
inference(forward_demodulation,[],[f3393,f1]) ).
fof(f3599,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_10_93700,X0),true,disjointwith(c_tptpcol_11_93764,X0),true),
inference(forward_demodulation,[],[f3390,f1]) ).
fof(f3600,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_11_93764,X0),true,disjointwith(c_tptpcol_12_93765,X0),true),
inference(forward_demodulation,[],[f3389,f1]) ).
fof(f3610,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_8_18438,X0),true,disjointwith(c_tptpcol_9_18439,X0),true),
inference(forward_demodulation,[],[f3379,f1]) ).
fof(f3611,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_9_18439,X0),true,disjointwith(c_tptpcol_10_18567,X0),true),
inference(forward_demodulation,[],[f3378,f1]) ).
fof(f3612,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_1_65536,X0),true,disjointwith(c_tptpcol_2_65537,X0),true),
inference(forward_demodulation,[],[f3377,f1]) ).
fof(f3613,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_2_65537,X0),true,disjointwith(c_tptpcol_3_81921,X0),true),
inference(forward_demodulation,[],[f3376,f1]) ).
fof(f3624,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_3_16386,X0),true,disjointwith(c_tptpcol_4_16387,X0),true),
inference(forward_demodulation,[],[f3365,f1]) ).
fof(f3625,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_4_16387,X0),true,disjointwith(c_tptpcol_5_16388,X0),true),
inference(forward_demodulation,[],[f3364,f1]) ).
fof(f3628,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_5_90114,X0),true,disjointwith(c_tptpcol_6_92162,X0),true),
inference(forward_demodulation,[],[f3361,f1]) ).
fof(f3629,plain,
! [X0] : true = ifeq4(disjointwith(c_tptpcol_6_92162,X0),true,disjointwith(c_tptpcol_7_93186,X0),true),
inference(forward_demodulation,[],[f3360,f1]) ).
fof(f7537,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536),true),
inference(superposition,[],[f3574,f305]) ).
fof(f7540,plain,
true = disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f7537,f1]) ).
fof(f7542,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_3_16386,c_tptpcol_1_65536),true),
inference(superposition,[],[f3551,f7540]) ).
fof(f7559,plain,
true = disjointwith(c_tptpcol_3_16386,c_tptpcol_1_65536),
inference(forward_demodulation,[],[f7542,f1]) ).
fof(f7591,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_1_65536,c_tptpcol_3_16386),true),
inference(superposition,[],[f2225,f7559]) ).
fof(f7600,plain,
true = disjointwith(c_tptpcol_1_65536,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f7591,f1]) ).
fof(f14448,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_2_65537,c_tptpcol_3_16386),true),
inference(superposition,[],[f3612,f7600]) ).
fof(f14451,plain,
true = disjointwith(c_tptpcol_2_65537,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f14448,f1]) ).
fof(f15194,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_3_81921,c_tptpcol_3_16386),true),
inference(superposition,[],[f3613,f14451]) ).
fof(f15211,plain,
true = disjointwith(c_tptpcol_3_81921,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f15194,f1]) ).
fof(f15213,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_4_90113,c_tptpcol_3_16386),true),
inference(superposition,[],[f3518,f15211]) ).
fof(f15232,plain,
true = disjointwith(c_tptpcol_4_90113,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f15213,f1]) ).
fof(f15234,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_5_90114,c_tptpcol_3_16386),true),
inference(superposition,[],[f3511,f15232]) ).
fof(f15251,plain,
true = disjointwith(c_tptpcol_5_90114,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f15234,f1]) ).
fof(f15254,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_6_92162,c_tptpcol_3_16386),true),
inference(superposition,[],[f3628,f15251]) ).
fof(f15271,plain,
true = disjointwith(c_tptpcol_6_92162,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f15254,f1]) ).
fof(f15273,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_7_93186,c_tptpcol_3_16386),true),
inference(superposition,[],[f3629,f15271]) ).
fof(f15294,plain,
true = disjointwith(c_tptpcol_7_93186,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f15273,f1]) ).
fof(f15296,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_8_93698,c_tptpcol_3_16386),true),
inference(superposition,[],[f3525,f15294]) ).
fof(f15313,plain,
true = disjointwith(c_tptpcol_8_93698,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f15296,f1]) ).
fof(f15335,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_9_93699,c_tptpcol_3_16386),true),
inference(superposition,[],[f3520,f15313]) ).
fof(f15354,plain,
true = disjointwith(c_tptpcol_9_93699,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f15335,f1]) ).
fof(f15356,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_10_93700,c_tptpcol_3_16386),true),
inference(superposition,[],[f3519,f15354]) ).
fof(f15373,plain,
true = disjointwith(c_tptpcol_10_93700,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f15356,f1]) ).
fof(f15533,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_11_93764,c_tptpcol_3_16386),true),
inference(superposition,[],[f3599,f15373]) ).
fof(f15552,plain,
true = disjointwith(c_tptpcol_11_93764,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f15533,f1]) ).
fof(f15554,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_12_93765,c_tptpcol_3_16386),true),
inference(superposition,[],[f3600,f15552]) ).
fof(f15571,plain,
true = disjointwith(c_tptpcol_12_93765,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f15554,f1]) ).
fof(f15573,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_13_93766,c_tptpcol_3_16386),true),
inference(superposition,[],[f3596,f15571]) ).
fof(f15592,plain,
true = disjointwith(c_tptpcol_13_93766,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f15573,f1]) ).
fof(f15594,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_14_93774,c_tptpcol_3_16386),true),
inference(superposition,[],[f3563,f15592]) ).
fof(f15611,plain,
true = disjointwith(c_tptpcol_14_93774,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f15594,f1]) ).
fof(f15613,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_3_16386),true),
inference(superposition,[],[f3564,f15611]) ).
fof(f15632,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_3_16386),
inference(forward_demodulation,[],[f15613,f1]) ).
fof(f15637,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_3_16386,c_tptpcol_15_93775),true),
inference(superposition,[],[f2225,f15632]) ).
fof(f15646,plain,
true = disjointwith(c_tptpcol_3_16386,c_tptpcol_15_93775),
inference(forward_demodulation,[],[f15637,f1]) ).
fof(f19119,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_4_16387,c_tptpcol_15_93775),true),
inference(superposition,[],[f3624,f15646]) ).
fof(f19138,plain,
true = disjointwith(c_tptpcol_4_16387,c_tptpcol_15_93775),
inference(forward_demodulation,[],[f19119,f1]) ).
fof(f19503,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_5_16388,c_tptpcol_15_93775),true),
inference(superposition,[],[f3625,f19138]) ).
fof(f19523,plain,
true = disjointwith(c_tptpcol_5_16388,c_tptpcol_15_93775),
inference(forward_demodulation,[],[f19503,f1]) ).
fof(f19525,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_6_18436,c_tptpcol_15_93775),true),
inference(superposition,[],[f3524,f19523]) ).
fof(f19542,plain,
true = disjointwith(c_tptpcol_6_18436,c_tptpcol_15_93775),
inference(forward_demodulation,[],[f19525,f1]) ).
fof(f19544,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_7_18437,c_tptpcol_15_93775),true),
inference(superposition,[],[f3523,f19542]) ).
fof(f19563,plain,
true = disjointwith(c_tptpcol_7_18437,c_tptpcol_15_93775),
inference(forward_demodulation,[],[f19544,f1]) ).
fof(f19565,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_8_18438,c_tptpcol_15_93775),true),
inference(superposition,[],[f3544,f19563]) ).
fof(f19582,plain,
true = disjointwith(c_tptpcol_8_18438,c_tptpcol_15_93775),
inference(forward_demodulation,[],[f19565,f1]) ).
fof(f19584,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_9_18439,c_tptpcol_15_93775),true),
inference(superposition,[],[f3610,f19582]) ).
fof(f19603,plain,
true = disjointwith(c_tptpcol_9_18439,c_tptpcol_15_93775),
inference(forward_demodulation,[],[f19584,f1]) ).
fof(f19605,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_10_18567,c_tptpcol_15_93775),true),
inference(superposition,[],[f3611,f19603]) ).
fof(f19622,plain,
true = disjointwith(c_tptpcol_10_18567,c_tptpcol_15_93775),
inference(forward_demodulation,[],[f19605,f1]) ).
fof(f19624,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_11_18631,c_tptpcol_15_93775),true),
inference(superposition,[],[f3588,f19622]) ).
fof(f19643,plain,
true = disjointwith(c_tptpcol_11_18631,c_tptpcol_15_93775),
inference(forward_demodulation,[],[f19624,f1]) ).
fof(f19645,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_12_18663,c_tptpcol_15_93775),true),
inference(superposition,[],[f3589,f19643]) ).
fof(f19662,plain,
true = disjointwith(c_tptpcol_12_18663,c_tptpcol_15_93775),
inference(forward_demodulation,[],[f19645,f1]) ).
fof(f19664,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_13_18664,c_tptpcol_15_93775),true),
inference(superposition,[],[f3556,f19662]) ).
fof(f19683,plain,
true = disjointwith(c_tptpcol_13_18664,c_tptpcol_15_93775),
inference(forward_demodulation,[],[f19664,f1]) ).
fof(f19688,plain,
true = ifeq4(true,true,disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),true),
inference(superposition,[],[f2225,f19683]) ).
fof(f19697,plain,
true = disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),
inference(forward_demodulation,[],[f19688,f1]) ).
fof(f19992,plain,
b = ifeq3(true,true,a,b),
inference(superposition,[],[f2269,f19697]) ).
fof(f20011,plain,
a = b,
inference(forward_demodulation,[],[f19992,f2]) ).
fof(f20012,plain,
$false,
inference(forward_subsumption_resolution,[],[f20011,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 THM
% 0.12/0.30 % Computer : n008.cluster.edu
% 0.12/0.30 % Model : x86_64 x86_64
% 0.12/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.30 % Memory : 8046.5625MB
% 0.12/0.30 % OS : Linux 6.8.0-71-generic
% 0.12/0.30 % CPULimit : 300
% 0.12/0.30 % WCLimit : 300
% 0.12/0.30 % DateTime : Mon Sep 28 22:15:25 UTC 2026
% 0.12/0.30 % CPUTime :
% 0.12/0.30 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.30/0.36 Running first-order theorem proving
% 0.30/0.36 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
% 22.06/7.63 % (2716870)Detected a unit-equality problem, will run specialized UEQ schedule.
% 22.06/7.63 % (2716875)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=683420080:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 22.06/7.63 % (2716876)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=72034788:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 22.06/7.63 % (2716877)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=969959986:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 22.06/7.63 % (2716879)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=4116707786:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 22.06/7.63 % (2716878)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=624146558:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 22.06/7.63 % (2716880)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1433406275:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 22.06/7.63 % (2716881)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=4157892634:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 22.06/7.63 % (2716878)Instruction limit reached!
% 22.06/7.63 % (2716878)------------------------------
% 22.06/7.63 % (2716878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.06/7.63 % (2716878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.06/7.63 % (2716878)CaDiCaL version: 2.1.3
% 22.06/7.63 % (2716878)Termination reason: Instruction limit
% 22.06/7.63 % (2716878)Termination phase: Saturation
% 22.06/7.63 % (2716878)Time elapsed: 0.117 s
% 22.06/7.63 % (2716878)Peak memory usage: 89 MB
% 22.06/7.63 % (2716878)Instructions burned: 136 (million)
% 22.06/7.63 % (2716879)Instruction limit reached!
% 22.06/7.63 % (2716879)------------------------------
% 22.06/7.63 % (2716879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.06/7.63 % (2716879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.06/7.63 % (2716879)CaDiCaL version: 2.1.3
% 22.06/7.63 % (2716879)Termination reason: Instruction limit
% 22.06/7.63 % (2716879)Termination phase: Saturation
% 22.06/7.63 % (2716879)Time elapsed: 0.163 s
% 22.06/7.63 % (2716879)Peak memory usage: 92 MB
% 22.06/7.63 % (2716879)Instructions burned: 181 (million)
% 22.06/7.63 % (2716880)Instruction limit reached!
% 22.06/7.63 % (2716880)------------------------------
% 22.06/7.63 % (2716880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.06/7.63 % (2716880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.06/7.63 % (2716880)CaDiCaL version: 2.1.3
% 22.06/7.63 % (2716880)Termination reason: Instruction limit
% 22.06/7.63 % (2716880)Termination phase: Saturation
% 22.06/7.63 % (2716880)Time elapsed: 0.237 s
% 22.06/7.63 % (2716880)Peak memory usage: 92 MB
% 22.06/7.63 % (2716880)Instructions burned: 261 (million)
% 22.06/7.63 % (2716889)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=744372297:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2995 on theBenchmark for (2995ds/2051Mi)
% 22.06/7.63 % (2716890)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2395124628:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 22.06/7.63 % (2716891)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1658772116:i=215:ep=RSTC_2994 on theBenchmark for (2994ds/215Mi)
% 22.06/7.63 % (2716891)Instruction limit reached!
% 22.06/7.63 % (2716891)------------------------------
% 22.06/7.63 % (2716891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.06/7.63 % (2716891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.06/7.63 % (2716891)CaDiCaL version: 2.1.3
% 22.06/7.63 % (2716891)Termination reason: Instruction limit
% 22.06/7.63 % (2716891)Termination phase: Saturation
% 22.06/7.63 % (2716891)Time elapsed: 0.188 s
% 22.06/7.63 % (2716891)Peak memory usage: 95 MB
% 22.06/7.63 % (2716891)Instructions burned: 215 (million)
% 22.06/7.63 % (2716895)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=1793711188:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/317Mi)
% 22.06/7.63 % (2716881)Instruction limit reached!
% 22.06/7.63 % (2716881)------------------------------
% 22.06/7.63 % (2716881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.06/7.63 % (2716881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.06/7.63 % (2716881)CaDiCaL version: 2.1.3
% 22.06/7.63 % (2716881)Termination reason: Instruction limit
% 22.06/7.63 % (2716881)Termination phase: Saturation
% 22.06/7.63 % (2716881)Time elapsed: 1.092 s
% 22.06/7.63 % (2716881)Peak memory usage: 106 MB
% 22.06/7.63 % (2716881)Instructions burned: 1187 (million)
% 22.06/7.63 % (2716895)Instruction limit reached!
% 22.06/7.63 % (2716895)------------------------------
% 22.06/7.63 % (2716895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.06/7.63 % (2716895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.06/7.63 % (2716895)CaDiCaL version: 2.1.3
% 22.06/7.63 % (2716895)Termination reason: Instruction limit
% 22.06/7.63 % (2716895)Termination phase: Saturation
% 22.06/7.63 % (2716895)Time elapsed: 0.266 s
% 22.06/7.63 % (2716895)Peak memory usage: 97 MB
% 22.06/7.63 % (2716895)Instructions burned: 318 (million)
% 22.06/7.63 % (2716898)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3987765338:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2985 on theBenchmark for (2985ds/2836Mi)
% 22.06/7.63 % (2716897)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=3800660129:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/12125Mi)
% 22.06/7.63 % (2716889)Instruction limit reached!
% 22.06/7.63 % (2716889)------------------------------
% 22.06/7.63 % (2716889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.06/7.63 % (2716889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.06/7.63 % (2716889)CaDiCaL version: 2.1.3
% 22.06/7.63 % (2716889)Termination reason: Instruction limit
% 22.06/7.63 % (2716889)Termination phase: Saturation
% 22.06/7.63 % (2716889)Time elapsed: 2.160 s
% 22.06/7.63 % (2716889)Peak memory usage: 142 MB
% 22.06/7.63 % (2716889)Instructions burned: 2051 (million)
% 22.06/7.63 % (2716901)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1298512725:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2971 on theBenchmark for (2971ds/14534Mi)
% 22.06/7.63 % (2716898)Instruction limit reached!
% 22.06/7.63 % (2716898)------------------------------
% 22.06/7.63 % (2716898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.06/7.63 % (2716898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.06/7.63 % (2716898)CaDiCaL version: 2.1.3
% 22.06/7.63 % (2716898)Termination reason: Instruction limit
% 22.06/7.63 % (2716898)Termination phase: Saturation
% 22.06/7.63 % (2716898)Time elapsed: 2.773 s
% 22.06/7.63 % (2716898)Peak memory usage: 157 MB
% 22.06/7.63 % (2716898)Instructions burned: 2836 (million)
% 22.06/7.63 % (2716903)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=2206402339:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2955 on theBenchmark for (2955ds/11832Mi)
% 22.06/7.63 % (2716890)Instruction limit reached!
% 22.06/7.63 % (2716890)------------------------------
% 22.06/7.63 % (2716890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.06/7.63 % (2716890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.06/7.63 % (2716890)CaDiCaL version: 2.1.3
% 22.06/7.63 % (2716890)Termination reason: Instruction limit
% 22.06/7.63 % (2716890)Termination phase: Saturation
% 22.06/7.63 % (2716890)Time elapsed: 5.172 s
% 22.06/7.63 % (2716890)Peak memory usage: 169 MB
% 22.06/7.63 % (2716890)Instructions burned: 4948 (million)
% 22.06/7.63 % (2716876)First to succeed.
% 22.06/7.63 % (2716876)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2716870"
% 22.06/7.63 % (2716907)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=639933630:i=2279:fgj=on:bd=all_2941 on theBenchmark for (2941ds/2279Mi)
% 22.06/7.63 % (2716876)Refutation found. Thanks to Tanya!
% 22.06/7.63 % SZS status Unsatisfiable for theBenchmark
% 22.06/7.63 % SZS output start Proof for theBenchmark
% See solution above
% 47.50/8.01 % (2716876)------------------------------
% 47.50/8.01 % (2716876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.50/8.01 % (2716876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.50/8.01 % (2716876)CaDiCaL version: 2.1.3
% 47.50/8.01 % (2716876)Termination reason: Refutation
% 47.50/8.01 % (2716876)Time elapsed: 5.851 s
% 47.50/8.01 % (2716876)Peak memory usage: 176 MB
% 47.50/8.01 % (2716876)Instructions burned: 5476 (million)
% 47.50/8.01 % (2716876)------------------------------
% 47.50/8.01 % (2716876)------------------------------
% 47.50/8.01 % (2716870)Success in time 6.678 s
% 47.50/8.01 % Vampire exiting
%------------------------------------------------------------------------------