%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN598-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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 02:17:41 PM UTC 2026
% Result : Unsatisfiable 19.83s 3.80s
% Output : Refutation 19.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 31
% Syntax : Number of formulae : 97 ( 97 unt; 21 def)
% Number of atoms : 97 ( 96 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 40 ( 40 usr; 25 con; 0-4 aty)
% Number of variables : 59 ( 59 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f3,negated_conjecture,
p18(c21) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c21_is_p18_2) ).
fof(f4,plain,
true = p18(c21),
inference(reorient_equations,[],[f3]) ).
fof(f5,negated_conjecture,
! [X0] : p7(X0,X0) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p7_3) ).
fof(f6,plain,
! [X0] : true = p7(X0,X0),
inference(reorient_equations,[],[f5]) ).
fof(f13,negated_conjecture,
p3(f4(f6(c21)),c22) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3_7) ).
fof(f14,plain,
true = p3(f4(f6(c21)),c22),
inference(reorient_equations,[],[f13]) ).
fof(f39,negated_conjecture,
! [X2,X0,X1] : ifeq(p7(X0,X1),true,ifeq(p7(X0,X2),true,p7(X2,X1),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p7_20) ).
fof(f40,plain,
! [X2,X0,X1] : true = ifeq(p7(X0,X1),true,ifeq(p7(X0,X2),true,p7(X2,X1),true),true),
inference(reorient_equations,[],[f39]) ).
fof(f45,negated_conjecture,
! [X2,X3,X0,X1] : ifeq(p19(X0,X1),true,ifeq(p7(X1,X2),true,ifeq(p7(X0,X3),true,p19(X3,X2),true),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p19_23) ).
fof(f46,plain,
! [X2,X3,X0,X1] : true = ifeq(p19(X0,X1),true,ifeq(p7(X1,X2),true,ifeq(p7(X0,X3),true,p19(X3,X2),true),true),true),
inference(reorient_equations,[],[f45]) ).
fof(f49,negated_conjecture,
! [X2,X3,X0,X1] : ifeq(p3(X0,X1),true,ifeq(p7(X2,X3),true,p7(f11(X2,X0),f11(X3,X1)),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p7_25) ).
fof(f50,plain,
! [X2,X3,X0,X1] : true = ifeq(p3(X0,X1),true,ifeq(p7(X2,X3),true,p7(f11(X2,X0),f11(X3,X1)),true),true),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
! [X2,X3,X0,X1] : ifeq(p7(X0,X1),true,ifeq(p7(X2,X3),true,p7(f10(X2,X0),f10(X3,X1)),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p7_26) ).
fof(f52,plain,
! [X2,X3,X0,X1] : true = ifeq(p7(X0,X1),true,ifeq(p7(X2,X3),true,p7(f10(X2,X0),f10(X3,X1)),true),true),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
p19(f10(f11(f14(f12(f15(f13(c23)))),c22),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(c21))) != true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_p19_27) ).
fof(f54,plain,
true != p19(f10(f11(f14(f12(f15(f13(c23)))),c22),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(c21))),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(X0))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X0))),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p19_28) ).
fof(f56,plain,
! [X0] : true = ifeq(p18(X0),true,p19(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(X0))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X0))),true),
inference(reorient_equations,[],[f55]) ).
fof(f62,definition,
sF1 = p18(c21),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f63,plain,
p18(c21) = sF1,
inference(reorient_equations,[],[f62]) ).
fof(f64,plain,
true = sF1,
inference(definition_folding,[],[f4,f63]) ).
fof(f65,definition,
sF2 = f6(c21),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f66,plain,
f6(c21) = sF2,
inference(reorient_equations,[],[f65]) ).
fof(f67,definition,
sF3 = f4(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f68,plain,
f4(sF2) = sF3,
inference(reorient_equations,[],[f67]) ).
fof(f69,definition,
sF4 = p3(sF3,c22),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f70,plain,
p3(sF3,c22) = sF4,
inference(reorient_equations,[],[f69]) ).
fof(f71,plain,
true = sF4,
inference(definition_folding,[],[f14,f70,f68,f66]) ).
fof(f72,definition,
sF5 = f13(c23),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f73,plain,
f13(c23) = sF5,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF6 = f15(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f75,plain,
f15(sF5) = sF6,
inference(reorient_equations,[],[f74]) ).
fof(f76,definition,
sF7 = f12(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f77,plain,
f12(sF6) = sF7,
inference(reorient_equations,[],[f76]) ).
fof(f78,definition,
sF8 = f14(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f79,plain,
f14(sF7) = sF8,
inference(reorient_equations,[],[f78]) ).
fof(f80,definition,
sF9 = f11(sF8,c22),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f81,plain,
f11(sF8,c22) = sF9,
inference(reorient_equations,[],[f80]) ).
fof(f82,definition,
sF10 = f13(sF5),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f83,plain,
f13(sF5) = sF10,
inference(reorient_equations,[],[f82]) ).
fof(f84,definition,
sF11 = f13(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f85,plain,
f13(sF10) = sF11,
inference(reorient_equations,[],[f84]) ).
fof(f86,definition,
sF12 = f13(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f87,plain,
f13(sF11) = sF12,
inference(reorient_equations,[],[f86]) ).
fof(f88,definition,
sF13 = f13(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f89,plain,
f13(sF12) = sF13,
inference(reorient_equations,[],[f88]) ).
fof(f90,definition,
sF14 = f13(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f91,plain,
f13(sF13) = sF14,
inference(reorient_equations,[],[f90]) ).
fof(f92,definition,
sF15 = f13(sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f93,plain,
f13(sF14) = sF15,
inference(reorient_equations,[],[f92]) ).
fof(f94,definition,
sF16 = f12(sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f95,plain,
f12(sF15) = sF16,
inference(reorient_equations,[],[f94]) ).
fof(f96,definition,
sF17 = f11(sF8,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f97,plain,
f11(sF8,sF16) = sF17,
inference(reorient_equations,[],[f96]) ).
fof(f98,definition,
sF18 = f10(sF9,sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f99,plain,
f10(sF9,sF17) = sF18,
inference(reorient_equations,[],[f98]) ).
fof(f100,definition,
sF19 = f9(c21),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f101,plain,
f9(c21) = sF19,
inference(reorient_equations,[],[f100]) ).
fof(f102,definition,
sF20 = f8(sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f103,plain,
f8(sF19) = sF20,
inference(reorient_equations,[],[f102]) ).
fof(f104,definition,
sF21 = p19(sF18,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f105,plain,
p19(sF18,sF20) = sF21,
inference(reorient_equations,[],[f104]) ).
fof(f106,plain,
true != sF21,
inference(definition_folding,[],[f54,f105,f103,f101,f99,f97,f95,f93,f91,f89,f87,f85,f83,f73,f79,f77,f75,f73,f81,f79,f77,f75,f73]) ).
fof(f107,plain,
! [X0] : true = ifeq(p18(X0),true,p19(f10(f11(sF8,f4(f6(X0))),sF17),f8(f9(X0))),true),
inference(definition_folding,[],[f56,f97,f95,f93,f91,f89,f87,f85,f83,f73,f79,f77,f75,f73,f79,f77,f75,f73]) ).
fof(f110,plain,
true = p18(c21),
inference(forward_demodulation,[],[f63,f64]) ).
fof(f111,plain,
true = p3(sF3,c22),
inference(forward_demodulation,[],[f70,f71]) ).
fof(f263,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(p7(X0,X1),true,p7(X1,X0),true),true),
inference(superposition,[],[f40,f6]) ).
fof(f273,plain,
! [X0,X1] : true = ifeq(p7(X0,X1),true,p7(X1,X0),true),
inference(forward_demodulation,[],[f263,f1]) ).
fof(f379,plain,
true = ifeq(true,true,p19(f10(f11(sF8,f4(f6(c21))),sF17),f8(f9(c21))),true),
inference(superposition,[],[f107,f110]) ).
fof(f380,plain,
true = p19(f10(f11(sF8,f4(f6(c21))),sF17),f8(f9(c21))),
inference(forward_demodulation,[],[f379,f1]) ).
fof(f381,plain,
true = p19(f10(f11(sF8,f4(f6(c21))),sF17),f8(sF19)),
inference(forward_demodulation,[],[f380,f101]) ).
fof(f382,plain,
true = p19(f10(f11(sF8,f4(f6(c21))),sF17),sF20),
inference(forward_demodulation,[],[f381,f103]) ).
fof(f383,plain,
true = p19(f10(f11(sF8,f4(sF2)),sF17),sF20),
inference(forward_demodulation,[],[f382,f66]) ).
fof(f384,plain,
true = p19(f10(f11(sF8,sF3),sF17),sF20),
inference(forward_demodulation,[],[f383,f68]) ).
fof(f421,plain,
! [X2,X0,X1] : true = ifeq(p3(X0,X1),true,ifeq(true,true,p7(f11(X2,X0),f11(X2,X1)),true),true),
inference(superposition,[],[f50,f6]) ).
fof(f426,plain,
! [X2,X0,X1] : true = ifeq(p3(X0,X1),true,p7(f11(X2,X0),f11(X2,X1)),true),
inference(forward_demodulation,[],[f421,f1]) ).
fof(f461,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(p7(X1,X2),true,p7(f10(X1,X0),f10(X2,X0)),true),true),
inference(superposition,[],[f52,f6]) ).
fof(f470,plain,
! [X2,X0,X1] : true = ifeq(p7(X1,X2),true,p7(f10(X1,X0),f10(X2,X0)),true),
inference(forward_demodulation,[],[f461,f1]) ).
fof(f851,plain,
! [X0,X1] : true = ifeq(p19(X0,X1),true,ifeq(p7(X1,sF20),true,ifeq(p7(X0,sF18),true,sF21,true),true),true),
inference(superposition,[],[f46,f105]) ).
fof(f2162,plain,
! [X0] : true = ifeq(true,true,p7(f11(X0,sF3),f11(X0,c22)),true),
inference(superposition,[],[f426,f111]) ).
fof(f2169,plain,
! [X0] : true = p7(f11(X0,sF3),f11(X0,c22)),
inference(forward_demodulation,[],[f2162,f1]) ).
fof(f2212,plain,
true = p7(f11(sF8,sF3),sF9),
inference(superposition,[],[f2169,f81]) ).
fof(f2294,plain,
true = ifeq(true,true,p7(sF9,f11(sF8,sF3)),true),
inference(superposition,[],[f273,f2212]) ).
fof(f2298,plain,
true = p7(sF9,f11(sF8,sF3)),
inference(forward_demodulation,[],[f2294,f1]) ).
fof(f2476,plain,
! [X0] : true = ifeq(p7(sF9,X0),true,p7(sF18,f10(X0,sF17)),true),
inference(superposition,[],[f470,f99]) ).
fof(f2824,plain,
true = ifeq(true,true,ifeq(p7(sF20,sF20),true,ifeq(p7(f10(f11(sF8,sF3),sF17),sF18),true,sF21,true),true),true),
inference(superposition,[],[f851,f384]) ).
fof(f2831,plain,
true = ifeq(p7(sF20,sF20),true,ifeq(p7(f10(f11(sF8,sF3),sF17),sF18),true,sF21,true),true),
inference(forward_demodulation,[],[f2824,f1]) ).
fof(f2833,plain,
true = ifeq(true,true,ifeq(p7(f10(f11(sF8,sF3),sF17),sF18),true,sF21,true),true),
inference(forward_demodulation,[],[f2831,f6]) ).
fof(f2835,plain,
true = ifeq(p7(f10(f11(sF8,sF3),sF17),sF18),true,sF21,true),
inference(forward_demodulation,[],[f2833,f1]) ).
fof(f4240,plain,
true = ifeq(true,true,p7(sF18,f10(f11(sF8,sF3),sF17)),true),
inference(superposition,[],[f2476,f2298]) ).
fof(f4248,plain,
true = p7(sF18,f10(f11(sF8,sF3),sF17)),
inference(forward_demodulation,[],[f4240,f1]) ).
fof(f4267,plain,
true = ifeq(true,true,p7(f10(f11(sF8,sF3),sF17),sF18),true),
inference(superposition,[],[f273,f4248]) ).
fof(f4285,plain,
true = p7(f10(f11(sF8,sF3),sF17),sF18),
inference(forward_demodulation,[],[f4267,f1]) ).
fof(f4495,plain,
true = ifeq(true,true,sF21,true),
inference(superposition,[],[f2835,f4285]) ).
fof(f4497,plain,
true = sF21,
inference(forward_demodulation,[],[f4495,f1]) ).
fof(f4498,plain,
$false,
inference(forward_subsumption_resolution,[],[f4497,f106]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN598-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.18 % Computer : n011.cluster.edu
% 0.06/0.18 % Model : x86_64 x86_64
% 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.18 % Memory : 8046.5625MB
% 0.06/0.18 % OS : Linux 6.8.0-71-generic
% 0.06/0.18 % CPULimit : 300
% 0.06/0.18 % WCLimit : 300
% 0.06/0.18 % DateTime : Mon Sep 28 16:34:12 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.21 Running first-order model finding
% 0.06/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.73/2.32 % (3518422)Will run a generic schedule for satisfiability detection.
% 14.73/2.32 % (3518430)dis+10_1_sil=32000:sp=arity:random_seed=3976849293:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.73/2.32 % (3518428)% WARNING: option uhcvi not known.
% 14.73/2.32 % (3518427)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1127639350_2999 on theBenchmark for (2999ds/0Mi)
% 14.73/2.32 % (3518429)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1383723995:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.73/2.32 % (3518428)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3932292299:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.73/2.32 % (3518431)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1884659136:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.73/2.32 % (3518432)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3722513746:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.73/2.32 % (3518433)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1093044110:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.73/2.32 % TRYING [1]
% 14.73/2.32 % TRYING [2]
% 14.73/2.32 % (3518430)Instruction limit reached!
% 14.73/2.32 % (3518430)------------------------------
% 14.73/2.32 % (3518430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.73/2.32 % (3518430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.73/2.32 % (3518430)CaDiCaL version: 2.1.3
% 14.73/2.32 % (3518430)Termination reason: Instruction limit
% 14.73/2.32 % (3518430)Termination phase: Saturation
% 14.73/2.32 % (3518430)Time elapsed: 0.030 s
% 14.73/2.32 % (3518430)Peak memory usage: 12 MB
% 14.73/2.32 % (3518430)Instructions burned: 106 (million)
% 14.73/2.32 % TRYING [3]
% 14.73/2.32 % (3518441)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3813479467:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.73/2.32 % TRYING [1]
% 14.73/2.32 % TRYING [2]
% 14.73/2.32 % (3518431)Instruction limit reached!
% 14.73/2.32 % (3518431)------------------------------
% 14.73/2.32 % (3518431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.73/2.32 % (3518431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.73/2.32 % (3518431)CaDiCaL version: 2.1.3
% 14.73/2.32 % (3518431)Termination reason: Instruction limit
% 14.73/2.32 % (3518431)Termination phase: Saturation
% 14.73/2.32 % (3518431)Time elapsed: 0.062 s
% 14.73/2.32 % (3518431)Peak memory usage: 13 MB
% 14.73/2.32 % (3518431)Instructions burned: 116 (million)
% 14.73/2.32 % TRYING [3]
% 14.73/2.32 % (3518432)Instruction limit reached!
% 14.73/2.32 % (3518432)------------------------------
% 14.73/2.32 % (3518432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.73/2.32 % (3518432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.73/2.32 % (3518432)CaDiCaL version: 2.1.3
% 14.73/2.32 % (3518432)Termination reason: Instruction limit
% 14.73/2.32 % (3518432)Termination phase: Saturation
% 14.73/2.32 % (3518432)Time elapsed: 0.069 s
% 14.73/2.32 % (3518432)Peak memory usage: 13 MB
% 14.73/2.32 % (3518432)Instructions burned: 131 (million)
% 14.73/2.32 % (3518443)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3812551492:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.73/2.32 % (3518444)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=865382700:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.73/2.32 % (3518433)Instruction limit reached!
% 14.73/2.32 % (3518433)------------------------------
% 14.73/2.32 % (3518433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.73/2.32 % (3518433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.73/2.32 % (3518433)CaDiCaL version: 2.1.3
% 14.73/2.32 % (3518433)Termination reason: Instruction limit
% 14.73/2.32 % (3518433)Termination phase: Saturation
% 14.73/2.32 % (3518433)Time elapsed: 0.093 s
% 14.73/2.32 % (3518433)Peak memory usage: 13 MB
% 14.73/2.32 % (3518433)Instructions burned: 159 (million)
% 14.73/2.32 % (3518447)ott-21_1_sil=16000:fs=off:random_seed=248428504:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.73/2.32 % TRYING [4]
% 14.73/2.32 % (3518443)Instruction limit reached!
% 14.73/2.32 % (3518443)------------------------------
% 14.73/2.32 % (3518443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.73/2.32 % (3518443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518443)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518443)Termination reason: Instruction limit
% 19.83/3.80 % (3518443)Termination phase: Saturation
% 19.83/3.80 % (3518443)Time elapsed: 0.077 s
% 19.83/3.80 % (3518443)Peak memory usage: 13 MB
% 19.83/3.80 % (3518443)Instructions burned: 131 (million)
% 19.83/3.80 % (3518449)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4207118502:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 19.83/3.80 % (3518447)Instruction limit reached!
% 19.83/3.80 % (3518447)------------------------------
% 19.83/3.80 % (3518447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.80 % (3518447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518447)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518447)Termination reason: Instruction limit
% 19.83/3.80 % (3518447)Termination phase: Saturation
% 19.83/3.80 % (3518447)Time elapsed: 0.089 s
% 19.83/3.80 % (3518447)Peak memory usage: 12 MB
% 19.83/3.80 % (3518447)Instructions burned: 180 (million)
% 19.83/3.80 % (3518451)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2905940918:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 19.83/3.80 % (3518441)Instruction limit reached!
% 19.83/3.80 % (3518441)------------------------------
% 19.83/3.80 % (3518441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.80 % (3518441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518441)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518441)Termination reason: Instruction limit
% 19.83/3.80 % (3518441)Termination phase: Finite model building SAT solving
% 19.83/3.80 % (3518441)Time elapsed: 0.194 s
% 19.83/3.80 % (3518441)Peak memory usage: 19 MB
% 19.83/3.80 % (3518441)Instructions burned: 718 (million)
% 19.83/3.80 % TRYING [1]
% 19.83/3.80 % TRYING [2]
% 19.83/3.80 % (3518453)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3053894227:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 19.83/3.80 % TRYING [3]
% 19.83/3.80 % TRYING [4]
% 19.83/3.80 % (3518449)Instruction limit reached!
% 19.83/3.80 % (3518449)------------------------------
% 19.83/3.80 % (3518449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.80 % (3518449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518449)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518449)Termination reason: Instruction limit
% 19.83/3.80 % (3518449)Termination phase: Saturation
% 19.83/3.80 % (3518449)Time elapsed: 0.243 s
% 19.83/3.80 % (3518449)Peak memory usage: 17 MB
% 19.83/3.80 % (3518449)Instructions burned: 478 (million)
% 19.83/3.80 % (3518444)Instruction limit reached!
% 19.83/3.80 % (3518444)------------------------------
% 19.83/3.80 % (3518444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.80 % (3518444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518444)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518444)Termination reason: Instruction limit
% 19.83/3.80 % (3518444)Termination phase: Saturation
% 19.83/3.80 % (3518444)Time elapsed: 0.336 s
% 19.83/3.80 % (3518444)Peak memory usage: 20 MB
% 19.83/3.80 % (3518444)Instructions burned: 686 (million)
% 19.83/3.80 % (3518455)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2412091300:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 19.83/3.80 % (3518456)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=795864015:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 19.83/3.80 % (3518451)Instruction limit reached!
% 19.83/3.80 % (3518451)------------------------------
% 19.83/3.80 % (3518451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.80 % (3518451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518451)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518451)Termination reason: Instruction limit
% 19.83/3.80 % (3518451)Termination phase: Finite model building SAT solving
% 19.83/3.80 % (3518451)Time elapsed: 0.357 s
% 19.83/3.80 % (3518451)Peak memory usage: 25 MB
% 19.83/3.80 % (3518451)Instructions burned: 865 (million)
% 19.83/3.80 % (3518453)Instruction limit reached!
% 19.83/3.80 % (3518453)------------------------------
% 19.83/3.80 % (3518453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.80 % (3518453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518453)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518453)Termination reason: Instruction limit
% 19.83/3.80 % (3518453)Termination phase: Saturation
% 19.83/3.80 % (3518453)Time elapsed: 0.344 s
% 19.83/3.80 % (3518453)Peak memory usage: 26 MB
% 19.83/3.80 % (3518453)Instructions burned: 1182 (million)
% 19.83/3.80 % (3518460)fmb+10_1_sil=64000:random_seed=1750972228:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 19.83/3.80 % TRYING [1]
% 19.83/3.80 % (3518459)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2808428884:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 19.83/3.80 % TRYING [2]
% 19.83/3.80 % TRYING [3]
% 19.83/3.80 % TRYING [4]
% 19.83/3.80 % (3518456)Instruction limit reached!
% 19.83/3.80 % (3518456)------------------------------
% 19.83/3.80 % (3518456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.80 % (3518456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518456)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518456)Termination reason: Instruction limit
% 19.83/3.80 % (3518456)Termination phase: Saturation
% 19.83/3.80 % (3518456)Time elapsed: 0.371 s
% 19.83/3.80 % (3518456)Peak memory usage: 22 MB
% 19.83/3.80 % (3518456)Instructions burned: 693 (million)
% 19.83/3.80 % TRYING [5]
% 19.83/3.80 % (3518463)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=642347043:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 19.83/3.80 % TRYING [20]
% 19.83/3.80 % (3518455)Instruction limit reached!
% 19.83/3.80 % (3518455)------------------------------
% 19.83/3.80 % (3518455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.80 % (3518455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518455)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518455)Termination reason: Instruction limit
% 19.83/3.80 % (3518455)Termination phase: Finite model building constraint generation
% 19.83/3.80 % (3518455)Time elapsed: 0.404 s
% 19.83/3.80 % (3518455)Peak memory usage: 104 MB
% 19.83/3.80 % (3518455)Instructions burned: 891 (million)
% 19.83/3.80 % (3518465)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1654628513:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 19.83/3.80 % TRYING [8]
% 19.83/3.80 % TRYING [5]
% 19.83/3.80 % (3518459)Instruction limit reached!
% 19.83/3.80 % (3518459)------------------------------
% 19.83/3.80 % (3518459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.80 % (3518459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518459)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518459)Termination reason: Instruction limit
% 19.83/3.80 % (3518459)Termination phase: Saturation
% 19.83/3.80 % (3518459)Time elapsed: 0.429 s
% 19.83/3.80 % (3518459)Peak memory usage: 20 MB
% 19.83/3.80 % (3518459)Instructions burned: 879 (million)
% 19.83/3.80 % (3518467)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1733014051:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 19.83/3.80 % (3518465)Instruction limit reached!
% 19.83/3.80 % (3518465)------------------------------
% 19.83/3.80 % (3518465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.80 % (3518465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518465)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518465)Termination reason: Instruction limit
% 19.83/3.80 % (3518465)Termination phase: Finite model building constraint generation
% 19.83/3.80 % (3518465)Time elapsed: 0.334 s
% 19.83/3.80 % (3518465)Peak memory usage: 75 MB
% 19.83/3.80 % (3518465)Instructions burned: 921 (million)
% 19.83/3.80 % (3518469)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4117110948:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 19.83/3.80 % TRYING [6]
% 19.83/3.80 % (3518469)Instruction limit reached!
% 19.83/3.80 % (3518469)------------------------------
% 19.83/3.80 % (3518469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.80 % (3518469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518469)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518469)Termination reason: Instruction limit
% 19.83/3.80 % (3518469)Termination phase: Saturation
% 19.83/3.80 % (3518469)Time elapsed: 0.791 s
% 19.83/3.80 % (3518469)Peak memory usage: 35 MB
% 19.83/3.80 % (3518469)Instructions burned: 1473 (million)
% 19.83/3.80 % (3518471)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1602254760:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 19.83/3.80 % (3518471)Cannot represent all propositional literals internally
% 19.83/3.80 % (3518471)Refutation not found, incomplete strategy
% 19.83/3.80 % (3518471)------------------------------
% 19.83/3.80 % (3518471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.80 % (3518471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518471)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518471)Termination reason: Refutation not found, incomplete strategy
% 19.83/3.80 % (3518471)Time elapsed: 0.010 s
% 19.83/3.80 % (3518471)Peak memory usage: 10 MB
% 19.83/3.80 % (3518471)Instructions burned: 20 (million)
% 19.83/3.80 % (3518471)------------------------------
% 19.83/3.80 % (3518471)------------------------------
% 19.83/3.80 % (3518473)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=881669499:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 19.83/3.80 % TRYING [16]
% 19.83/3.80 % (3518473)Instruction limit reached!
% 19.83/3.80 % (3518473)------------------------------
% 19.83/3.80 % (3518473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.80 % (3518473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518473)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518473)Termination reason: Instruction limit
% 19.83/3.80 % (3518473)Termination phase: Finite model building constraint generation
% 19.83/3.80 % (3518473)Time elapsed: 0.757 s
% 19.83/3.80 % (3518473)Peak memory usage: 142 MB
% 19.83/3.80 % (3518473)Instructions burned: 2174 (million)
% 19.83/3.80 % (3518475)ott-2_1_sil=16000:newcnf=on:random_seed=2219989431:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2971 on theBenchmark for (2971ds/869Mi)
% 19.83/3.80 % TRYING [7]
% 19.83/3.80 % TRYING [6]
% 19.83/3.80 % (3518475)Instruction limit reached!
% 19.83/3.80 % (3518475)------------------------------
% 19.83/3.80 % (3518475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.80 % (3518475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.80 % (3518475)CaDiCaL version: 2.1.3
% 19.83/3.80 % (3518475)Termination reason: Instruction limit
% 19.83/3.80 % (3518475)Termination phase: Saturation
% 19.83/3.80 % (3518475)Time elapsed: 0.452 s
% 19.83/3.80 % (3518475)Peak memory usage: 27 MB
% 19.83/3.80 % (3518475)Instructions burned: 870 (million)
% 19.83/3.80 % (3518477)ott+10_1_sil=32000:tgt=ground:random_seed=3826417328:i=5114:av=off_2966 on theBenchmark for (2966ds/5114Mi)
% 19.83/3.80 % (3518477) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3518422-3518477"...
% 19.83/3.80 % (3518477)...printing done.
% 19.83/3.80 % (3518477)Refutation found. Thanks to Tanya!
% 19.83/3.80 % SZS status Unsatisfiable for theBenchmark
% 19.83/3.80 % SZS output start Proof for theBenchmark
% See solution above
% 19.83/3.81 % (3518477)------------------------------
% 19.83/3.81 % (3518477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.83/3.81 % (3518477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.81 % (3518477)CaDiCaL version: 2.1.3
% 19.83/3.81 % (3518477)Termination reason: Refutation
% 19.83/3.81 % (3518477)Time elapsed: 0.117 s
% 19.83/3.81 % (3518477)Peak memory usage: 15 MB
% 19.83/3.81 % (3518477)Instructions burned: 213 (million)
% 19.83/3.81 % (3518422)Success in time 3.583 s
% 19.83/3.81 % Vampire exiting
%------------------------------------------------------------------------------