%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : COL076-2 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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:38:23 AM UTC 2026
% Result : Unsatisfiable 76.64s 26.64s
% Output : Refutation 76.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 7
% Syntax : Number of formulae : 18 ( 16 unt; 0 def)
% Number of atoms : 20 ( 19 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 9 ( 7 ~; 2 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 30 ( 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : apply(apply(k,X0),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',k_definition) ).
fof(f4,axiom,
! [X0] : pair(apply(projection1,X0),apply(projection2,X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pairing) ).
fof(f5,axiom,
! [X2,X0,X1] : apply(pair(X0,X1),X2) = pair(apply(X0,X2),apply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pairwise_application) ).
fof(f6,axiom,
! [X2,X0,X1] : apply(apply(apply(abstraction,X0),X1),X2) = apply(apply(X0,apply(k,X2)),apply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abstraction) ).
fof(f7,axiom,
! [X0,X1] :
( apply(X0,n(X0,X1)) != apply(X1,n(X0,X1))
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',extensionality2) ).
fof(f8,axiom,
! [X0,X1] : apply(apply(f,X0),X1) = apply(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diagonal_combinator) ).
fof(f9,negated_conjecture,
! [X0] : X0 != apply(eq,pair(apply(k,X0),apply(k,projection2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_self_referential) ).
fof(f10,plain,
! [X0] : apply(eq,pair(apply(k,X0),apply(k,projection2))) != X0,
inference(reorient_equations,[],[f9]) ).
fof(f17,plain,
! [X2,X0,X1] : apply(pair(X1,apply(k,X0)),X2) = pair(apply(X1,X2),X0),
inference(superposition,[],[f5,f1]) ).
fof(f21,plain,
! [X0] : apply(pair(projection1,projection2),X0) = X0,
inference(superposition,[],[f5,f4]) ).
fof(f80,plain,
! [X0,X1] : pair(X0,X1) = apply(pair(pair(projection1,projection2),apply(k,X1)),X0),
inference(superposition,[],[f17,f21]) ).
fof(f601,plain,
! [X0,X1] :
( apply(X1,n(apply(k,X0),X1)) != X0
| apply(k,X0) = X1 ),
inference(superposition,[],[f7,f1]) ).
fof(f1089,plain,
! [X2,X0,X1] : apply(X0,apply(X1,X2)) = apply(apply(apply(abstraction,apply(k,X0)),X1),X2),
inference(superposition,[],[f6,f1]) ).
fof(f4370,plain,
! [X0] : apply(f,X0) = apply(k,apply(X0,X0)),
inference(unit_resulting_resolution,[],[f601,f8]) ).
fof(f55968,plain,
! [X0] : apply(X0,X0) != apply(eq,pair(apply(f,X0),apply(k,projection2))),
inference(superposition,[],[f10,f4370]) ).
fof(f57560,plain,
! [X0] : apply(X0,X0) != apply(eq,apply(pair(f,apply(k,apply(k,projection2))),X0)),
inference(forward_demodulation,[],[f55968,f17]) ).
fof(f57602,plain,
! [X0] : apply(X0,X0) != apply(eq,apply(apply(pair(pair(projection1,projection2),apply(k,apply(k,apply(k,projection2)))),f),X0)),
inference(forward_demodulation,[],[f57560,f80]) ).
fof(f57690,plain,
$false,
inference(unit_resulting_resolution,[],[f57602,f1089]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : COL076-2 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.27 % Computer : n015.cluster.edu
% 0.11/0.27 % Model : x86_64 x86_64
% 0.11/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.27 % Memory : 8046.5625MB
% 0.11/0.27 % OS : Linux 6.8.0-71-generic
% 0.11/0.27 % CPULimit : 300
% 0.11/0.27 % WCLimit : 300
% 0.11/0.27 % DateTime : Mon Sep 28 21:37:17 UTC 2026
% 0.11/0.27 % CPUTime :
% 0.11/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.25/0.32 Running first-order model finding
% 0.25/0.32 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
% 28.86/4.41 % (3060247)Will run a generic schedule for satisfiability detection.
% 28.86/4.41 % (3060253)% WARNING: option uhcvi not known.
% 28.86/4.41 % (3060253)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=795582183:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 28.86/4.41 % (3060258)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1987143473:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 28.86/4.41 % (3060252)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=407816146_2999 on theBenchmark for (2999ds/0Mi)
% 28.86/4.41 % (3060257)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1709985258:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 28.86/4.41 % (3060254)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=193720801:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 28.86/4.41 % (3060256)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3166205083:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 28.86/4.41 % TRYING [1]
% 28.86/4.41 % TRYING [2]
% 28.86/4.41 % (3060255)dis+10_1_sil=32000:sp=arity:random_seed=2781237946:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 28.86/4.41 % TRYING [3]
% 28.86/4.41 % TRYING [4]
% 28.86/4.41 % TRYING [5]
% 28.86/4.41 % TRYING [6]
% 28.86/4.41 % (3060255)Instruction limit reached!
% 28.86/4.41 % (3060255)------------------------------
% 28.86/4.41 % (3060255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.86/4.41 % (3060255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.86/4.41 % (3060255)CaDiCaL version: 2.1.3
% 28.86/4.41 % (3060255)Termination reason: Instruction limit
% 28.86/4.41 % (3060255)Termination phase: Saturation
% 28.86/4.41 % (3060255)Time elapsed: 0.098 s
% 28.86/4.41 % (3060255)Peak memory usage: 12 MB
% 28.86/4.41 % (3060255)Instructions burned: 104 (million)
% 28.86/4.41 % (3060256)Instruction limit reached!
% 28.86/4.41 % (3060256)------------------------------
% 28.86/4.41 % (3060256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.86/4.41 % (3060256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.86/4.41 % (3060256)CaDiCaL version: 2.1.3
% 28.86/4.41 % (3060256)Termination reason: Instruction limit
% 28.86/4.41 % (3060256)Termination phase: Saturation
% 28.86/4.41 % (3060256)Time elapsed: 0.120 s
% 28.86/4.41 % (3060256)Peak memory usage: 13 MB
% 28.86/4.41 % (3060256)Instructions burned: 116 (million)
% 28.86/4.41 % (3060257)Instruction limit reached!
% 28.86/4.41 % (3060257)------------------------------
% 28.86/4.41 % (3060257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.86/4.41 % (3060257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.86/4.41 % (3060257)CaDiCaL version: 2.1.3
% 28.86/4.41 % (3060257)Termination reason: Instruction limit
% 28.86/4.41 % (3060257)Termination phase: Saturation
% 28.86/4.41 % (3060257)Time elapsed: 0.131 s
% 28.86/4.41 % (3060257)Peak memory usage: 13 MB
% 28.86/4.41 % (3060257)Instructions burned: 131 (million)
% 28.86/4.41 % (3060266)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1453832891:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 28.86/4.41 % TRYING [1]
% 28.86/4.41 % TRYING [2]
% 28.86/4.41 % TRYING [3]
% 28.86/4.41 % TRYING [4]
% 28.86/4.41 % (3060267)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3837477475:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 28.86/4.41 % (3060258)Instruction limit reached!
% 28.86/4.41 % (3060258)------------------------------
% 28.86/4.41 % (3060258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.86/4.41 % (3060258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.86/4.41 % (3060258)CaDiCaL version: 2.1.3
% 28.86/4.41 % (3060258)Termination reason: Instruction limit
% 28.86/4.41 % (3060258)Termination phase: Saturation
% 28.86/4.41 % (3060258)Time elapsed: 0.164 s
% 28.86/4.41 % (3060258)Peak memory usage: 13 MB
% 28.86/4.41 % (3060258)Instructions burned: 159 (million)
% 28.86/4.41 % (3060268)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=1644960570:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 28.86/4.41 % TRYING [5]
% 28.86/4.41 % (3060272)ott-21_1_sil=16000:fs=off:random_seed=1680362846:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 28.86/4.41 % TRYING [6]
% 28.86/4.41 % TRYING [7]
% 28.86/4.41 % (3060267)Instruction limit reached!
% 28.86/4.41 % (3060267)------------------------------
% 28.86/4.41 % (3060267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.06/12.40 % (3060267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.06/12.40 % (3060267)CaDiCaL version: 2.1.3
% 85.06/12.40 % (3060267)Termination reason: Instruction limit
% 85.06/12.40 % (3060267)Termination phase: Saturation
% 85.06/12.40 % (3060267)Time elapsed: 0.143 s
% 85.06/12.40 % (3060267)Peak memory usage: 13 MB
% 85.06/12.40 % (3060267)Instructions burned: 132 (million)
% 85.06/12.40 % (3060275)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2895715883:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 85.06/12.40 % (3060272)Instruction limit reached!
% 85.06/12.40 % (3060272)------------------------------
% 85.06/12.40 % (3060272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.06/12.40 % (3060272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.06/12.40 % (3060272)CaDiCaL version: 2.1.3
% 85.06/12.40 % (3060272)Termination reason: Instruction limit
% 85.06/12.40 % (3060272)Termination phase: Saturation
% 85.06/12.40 % (3060272)Time elapsed: 0.174 s
% 85.06/12.40 % (3060272)Peak memory usage: 13 MB
% 85.06/12.40 % (3060272)Instructions burned: 180 (million)
% 85.06/12.40 % TRYING [7]
% 85.06/12.40 % (3060277)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3733460303:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 85.06/12.40 % TRYING [1]
% 85.06/12.40 % TRYING [2]
% 85.06/12.40 % TRYING [3]
% 85.06/12.40 % TRYING [4]
% 85.06/12.40 % TRYING [5]
% 85.06/12.40 % TRYING [6]
% 85.06/12.40 % (3060268)Instruction limit reached!
% 85.06/12.40 % (3060268)------------------------------
% 85.06/12.40 % (3060268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.06/12.40 % (3060268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.06/12.40 % (3060268)CaDiCaL version: 2.1.3
% 85.06/12.40 % (3060268)Termination reason: Instruction limit
% 85.06/12.40 % (3060268)Termination phase: Saturation
% 85.06/12.40 % (3060268)Time elapsed: 0.468 s
% 85.06/12.40 % (3060268)Peak memory usage: 17 MB
% 85.06/12.40 % (3060268)Instructions burned: 685 (million)
% 85.06/12.40 % (3060281)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=105926485:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 85.06/12.40 % (3060266)Instruction limit reached!
% 85.06/12.40 % (3060266)------------------------------
% 85.06/12.40 % (3060266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.06/12.40 % (3060266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.06/12.40 % (3060266)CaDiCaL version: 2.1.3
% 85.06/12.40 % (3060266)Termination reason: Instruction limit
% 85.06/12.40 % (3060266)Termination phase: Finite model building SAT solving
% 85.06/12.40 % (3060266)Time elapsed: 0.539 s
% 85.06/12.40 % (3060266)Peak memory usage: 33 MB
% 85.06/12.40 % (3060266)Instructions burned: 714 (million)
% 85.06/12.40 % (3060283)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=709174099:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 85.06/12.40 % TRYING [8]
% 85.06/12.40 % (3060275)Instruction limit reached!
% 85.06/12.40 % (3060275)------------------------------
% 85.06/12.40 % (3060275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.06/12.40 % (3060275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.06/12.40 % (3060275)CaDiCaL version: 2.1.3
% 85.06/12.40 % (3060275)Termination reason: Instruction limit
% 85.06/12.40 % (3060275)Termination phase: Saturation
% 85.06/12.40 % (3060275)Time elapsed: 0.470 s
% 85.06/12.40 % (3060275)Peak memory usage: 15 MB
% 85.06/12.40 % (3060275)Instructions burned: 477 (million)
% 85.06/12.40 % TRYING [14]
% 85.06/12.40 % (3060286)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=2524138015: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)
% 85.06/12.40 % TRYING [7]
% 85.06/12.40 % (3060277)Instruction limit reached!
% 85.06/12.40 % (3060277)------------------------------
% 85.06/12.40 % (3060277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.06/12.40 % (3060277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.06/12.40 % (3060277)CaDiCaL version: 2.1.3
% 85.06/12.40 % (3060277)Termination reason: Instruction limit
% 85.06/12.40 % (3060277)Termination phase: Finite model building constraint generation
% 85.06/12.40 % (3060277)Time elapsed: 0.582 s
% 85.06/12.40 % (3060277)Peak memory usage: 24 MB
% 85.06/12.40 % (3060277)Instructions burned: 865 (million)
% 85.06/12.40 % (3060289)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4076225423:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 174.58/24.98 % (3060283)Instruction limit reached!
% 174.58/24.98 % (3060283)------------------------------
% 174.58/24.98 % (3060283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 174.58/24.98 % (3060283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.58/24.98 % (3060283)CaDiCaL version: 2.1.3
% 174.58/24.98 % (3060283)Termination reason: Instruction limit
% 174.58/24.98 % (3060283)Termination phase: Finite model building constraint generation
% 174.58/24.98 % (3060283)Time elapsed: 0.514 s
% 174.58/24.98 % (3060283)Peak memory usage: 78 MB
% 174.58/24.98 % (3060283)Instructions burned: 889 (million)
% 174.58/24.98 % (3060292)fmb+10_1_sil=64000:random_seed=863704123:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi)
% 174.58/24.98 % TRYING [1]
% 174.58/24.98 % TRYING [2]
% 174.58/24.98 % TRYING [3]
% 174.58/24.98 % TRYING [4]
% 174.58/24.98 % TRYING [5]
% 174.58/24.98 % TRYING [6]
% 174.58/24.98 % (3060286)Instruction limit reached!
% 174.58/24.98 % (3060286)------------------------------
% 174.58/24.98 % (3060286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 174.58/24.98 % (3060286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.58/24.98 % (3060286)CaDiCaL version: 2.1.3
% 174.58/24.98 % (3060286)Termination reason: Instruction limit
% 174.58/24.98 % (3060286)Termination phase: Saturation
% 174.58/24.98 % (3060286)Time elapsed: 0.670 s
% 174.58/24.98 % (3060286)Peak memory usage: 21 MB
% 174.58/24.98 % (3060286)Instructions burned: 692 (million)
% 174.58/24.98 % (3060295)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=286790312:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 174.58/24.98 % TRYING [20]
% 174.58/24.98 % TRYING [7]
% 174.58/24.98 % (3060281)Instruction limit reached!
% 174.58/24.98 % (3060281)------------------------------
% 174.58/24.98 % (3060281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 174.58/24.98 % (3060281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.58/24.98 % (3060281)CaDiCaL version: 2.1.3
% 174.58/24.98 % (3060281)Termination reason: Instruction limit
% 174.58/24.98 % (3060281)Termination phase: Saturation
% 174.58/24.98 % (3060281)Time elapsed: 1.184 s
% 174.58/24.98 % (3060281)Peak memory usage: 26 MB
% 174.58/24.98 % (3060281)Instructions burned: 1180 (million)
% 174.58/24.98 % (3060289)Instruction limit reached!
% 174.58/24.98 % (3060289)------------------------------
% 174.58/24.98 % (3060289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 174.58/24.98 % (3060289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.58/24.98 % (3060289)CaDiCaL version: 2.1.3
% 174.58/24.98 % (3060289)Termination reason: Instruction limit
% 174.58/24.98 % (3060289)Termination phase: Saturation
% 174.58/24.98 % (3060289)Time elapsed: 0.820 s
% 174.58/24.98 % (3060289)Peak memory usage: 18 MB
% 174.58/24.98 % (3060289)Instructions burned: 880 (million)
% 174.58/24.98 % (3060299)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1174926853:fmbsr=1.7:i=920_2981 on theBenchmark for (2981ds/920Mi)
% 174.58/24.98 % TRYING [8]
% 174.58/24.98 % (3060300)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4227718437:i=5131_2980 on theBenchmark for (2980ds/5131Mi)
% 174.58/24.98 % TRYING [9]
% 174.58/24.98 % TRYING [8]
% 174.58/24.98 % (3060299)Instruction limit reached!
% 174.58/24.98 % (3060299)------------------------------
% 174.58/24.98 % (3060299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 174.58/24.98 % (3060299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.58/24.98 % (3060299)CaDiCaL version: 2.1.3
% 174.58/24.98 % (3060299)Termination reason: Instruction limit
% 174.58/24.98 % (3060299)Termination phase: Finite model building SAT solving
% 174.58/24.98 % (3060299)Time elapsed: 0.786 s
% 174.58/24.98 % (3060299)Peak memory usage: 53 MB
% 174.58/24.98 % (3060299)Instructions burned: 921 (million)
% 174.58/24.98 % (3060304)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3391800955:i=1472:ins=7:fdi=8:gsp=on_2972 on theBenchmark for (2972ds/1472Mi)
% 174.58/24.98 % (3060304)Instruction limit reached!
% 174.58/24.98 % (3060304)------------------------------
% 174.58/24.98 % (3060304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 174.58/24.98 % (3060304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.58/24.98 % (3060304)CaDiCaL version: 2.1.3
% 174.58/24.98 % (3060304)Termination reason: Instruction limit
% 174.58/24.98 % (3060304)Termination phase: Saturation
% 174.58/24.98 % (3060304)Time elapsed: 1.270 s
% 174.58/24.98 % (3060304)Peak memory usage: 23 MB
% 174.58/24.98 % (3060304)Instructions burned: 1472 (million)
% 174.58/24.98 % (3060306)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3716318181:i=6324_2959 on theBenchmark for (2959ds/6324Mi)
% 76.64/26.64 % TRYING [77]
% 76.64/26.64 % TRYING [9]
% 76.64/26.64 % (3060300)Instruction limit reached!
% 76.64/26.64 % (3060300)------------------------------
% 76.64/26.64 % (3060300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.64/26.64 % (3060300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.64/26.64 % (3060300)CaDiCaL version: 2.1.3
% 76.64/26.64 % (3060300)Termination reason: Instruction limit
% 76.64/26.64 % (3060300)Termination phase: Saturation
% 76.64/26.64 % (3060300)Time elapsed: 4.464 s
% 76.64/26.64 % (3060300)Peak memory usage: 49 MB
% 76.64/26.64 % (3060300)Instructions burned: 5131 (million)
% 76.64/26.64 % (3060316)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3728890530:fmbsr=2.30978:i=2174_2935 on theBenchmark for (2935ds/2174Mi)
% 76.64/26.64 % TRYING [16]
% 76.64/26.64 % TRYING [10]
% 76.64/26.64 % (3060316)Instruction limit reached!
% 76.64/26.64 % (3060316)------------------------------
% 76.64/26.64 % (3060316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.64/26.64 % (3060316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.64/26.64 % (3060316)CaDiCaL version: 2.1.3
% 76.64/26.64 % (3060316)Termination reason: Instruction limit
% 76.64/26.64 % (3060316)Termination phase: Finite model building constraint generation
% 76.64/26.64 % (3060316)Time elapsed: 1.467 s
% 76.64/26.64 % (3060316)Peak memory usage: 135 MB
% 76.64/26.64 % (3060316)Instructions burned: 2174 (million)
% 76.64/26.64 % (3060324)ott-2_1_sil=16000:newcnf=on:random_seed=1919748964:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2920 on theBenchmark for (2920ds/869Mi)
% 76.64/26.64 % (3060324)Instruction limit reached!
% 76.64/26.64 % (3060324)------------------------------
% 76.64/26.64 % (3060324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.64/26.64 % (3060324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.64/26.64 % (3060324)CaDiCaL version: 2.1.3
% 76.64/26.64 % (3060324)Termination reason: Instruction limit
% 76.64/26.64 % (3060324)Termination phase: Saturation
% 76.64/26.64 % (3060324)Time elapsed: 0.535 s
% 76.64/26.64 % (3060324)Peak memory usage: 15 MB
% 76.64/26.64 % (3060324)Instructions burned: 870 (million)
% 76.64/26.64 % (3060328)ott+10_1_sil=32000:tgt=ground:random_seed=3628573940:i=5114:av=off_2914 on theBenchmark for (2914ds/5114Mi)
% 76.64/26.64 % (3060295)Instruction limit reached!
% 76.64/26.64 % (3060295)------------------------------
% 76.64/26.64 % (3060295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.64/26.64 % (3060295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.64/26.64 % (3060295)CaDiCaL version: 2.1.3
% 76.64/26.64 % (3060295)Termination reason: Instruction limit
% 76.64/26.64 % (3060295)Termination phase: Finite model building constraint generation
% 76.64/26.64 % (3060295)Time elapsed: 7.047 s
% 76.64/26.64 % (3060295)Peak memory usage: 668 MB
% 76.64/26.64 % (3060295)Instructions burned: 9516 (million)
% 76.64/26.64 % (3060306)Instruction limit reached!
% 76.64/26.64 % (3060306)------------------------------
% 76.64/26.64 % (3060306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.64/26.64 % (3060306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.64/26.64 % (3060306)CaDiCaL version: 2.1.3
% 76.64/26.64 % (3060306)Termination reason: Instruction limit
% 76.64/26.64 % (3060306)Termination phase: Finite model building constraint generation
% 76.64/26.64 % (3060306)Time elapsed: 4.616 s
% 76.64/26.64 % (3060306)Peak memory usage: 509 MB
% 76.64/26.64 % (3060306)Instructions burned: 6325 (million)
% 76.64/26.64 % (3060332)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1579094354:i=54282_2911 on theBenchmark for (2911ds/54282Mi)
% 76.64/26.64 % TRYING [1]
% 76.64/26.64 % TRYING [2]
% 76.64/26.64 % TRYING [3]
% 76.64/26.64 % TRYING [4]
% 76.64/26.64 % TRYING [5]
% 76.64/26.64 % (3060333)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2649174854:i=3512:aac=none_2911 on theBenchmark for (2911ds/3512Mi)
% 76.64/26.64 % TRYING [6]
% 76.64/26.64 % TRYING [7]
% 76.64/26.64 % TRYING [8]
% 76.64/26.64 % TRYING [9]
% 76.64/26.64 % TRYING [10]
% 76.64/26.64 % (3060333)Instruction limit reached!
% 76.64/26.64 % (3060333)------------------------------
% 76.64/26.64 % (3060333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.64/26.64 % (3060333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.64/26.64 % (3060333)CaDiCaL version: 2.1.3
% 76.64/26.64 % (3060333)Termination reason: Instruction limit
% 76.64/26.64 % (3060333)Termination phase: Saturation
% 76.64/26.64 % (3060333)Time elapsed: 3.201 s
% 76.64/26.64 % (3060333)Peak memory usage: 40 MB
% 76.64/26.64 % (3060333)Instructions burned: 3512 (million)
% 76.64/26.64 % (3060338)dis+21_1_sil=32000:sas=cadical:random_seed=3798455756:i=3773:amm=off_2879 on theBenchmark for (2879ds/3773Mi)
% 76.64/26.64 % (3060328)Instruction limit reached!
% 76.64/26.64 % (3060328)------------------------------
% 76.64/26.64 % (3060328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.64/26.64 % (3060328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.64/26.64 % (3060328)CaDiCaL version: 2.1.3
% 76.64/26.64 % (3060328)Termination reason: Instruction limit
% 76.64/26.64 % (3060328)Termination phase: Saturation
% 76.64/26.64 % (3060328)Time elapsed: 5.280 s
% 76.64/26.64 % (3060328)Peak memory usage: 68 MB
% 76.64/26.64 % (3060328)Instructions burned: 5114 (million)
% 76.64/26.64 % (3060344)ott+11_1_sil=16000:gs=on:random_seed=538491673:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2861 on theBenchmark for (2861ds/2251Mi)
% 76.64/26.64 % (3060338)Instruction limit reached!
% 76.64/26.64 % (3060338)------------------------------
% 76.64/26.64 % (3060338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.64/26.64 % (3060338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.64/26.64 % (3060338)CaDiCaL version: 2.1.3
% 76.64/26.64 % (3060338)Termination reason: Instruction limit
% 76.64/26.64 % (3060338)Termination phase: Saturation
% 76.64/26.64 % (3060338)Time elapsed: 3.450 s
% 76.64/26.64 % (3060338)Peak memory usage: 42 MB
% 76.64/26.64 % (3060338)Instructions burned: 3774 (million)
% 76.64/26.64 % (3060350)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2420430924:fmbsr=1.6:i=67534_2844 on theBenchmark for (2844ds/67534Mi)
% 76.64/26.64 % TRYING [7]
% 76.64/26.64 % (3060344)Instruction limit reached!
% 76.64/26.64 % (3060344)------------------------------
% 76.64/26.64 % (3060344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.64/26.64 % (3060344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.64/26.64 % (3060344)CaDiCaL version: 2.1.3
% 76.64/26.64 % (3060344)Termination reason: Instruction limit
% 76.64/26.64 % (3060344)Termination phase: Saturation
% 76.64/26.64 % (3060344)Time elapsed: 2.005 s
% 76.64/26.64 % (3060344)Peak memory usage: 36 MB
% 76.64/26.64 % (3060344)Instructions burned: 2252 (million)
% 76.64/26.64 % (3060352)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3054092701:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2840 on theBenchmark for (2840ds/4591Mi)
% 76.64/26.64 % TRYING [8]
% 76.64/26.64 % TRYING [9]
% 76.64/26.64 % (3060292)Instruction limit reached!
% 76.64/26.64 % (3060292)------------------------------
% 76.64/26.64 % (3060292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.64/26.64 % (3060292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.64/26.64 % (3060292)CaDiCaL version: 2.1.3
% 76.64/26.64 % (3060292)Termination reason: Instruction limit
% 76.64/26.64 % (3060292)Termination phase: Finite model building SAT solving
% 76.64/26.64 % (3060292)Time elapsed: 16.925 s
% 76.64/26.64 % (3060292)Peak memory usage: 120 MB
% 76.64/26.64 % (3060292)Instructions burned: 22062 (million)
% 76.64/26.64 % (3060354)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1572194400:i=29340_2817 on theBenchmark for (2817ds/29340Mi)
% 76.64/26.64 % (3060352)Instruction limit reached!
% 76.64/26.64 % (3060352)------------------------------
% 76.64/26.64 % (3060352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.64/26.64 % (3060352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.64/26.64 % (3060352)CaDiCaL version: 2.1.3
% 76.64/26.64 % (3060352)Termination reason: Instruction limit
% 76.64/26.64 % (3060352)Termination phase: Saturation
% 76.64/26.64 % (3060352)Time elapsed: 3.937 s
% 76.64/26.64 % (3060352)Peak memory usage: 50 MB
% 76.64/26.64 % (3060352)Instructions burned: 4592 (million)
% 76.64/26.64 % (3060358)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4261598723:i=5211_2801 on theBenchmark for (2801ds/5211Mi)
% 76.64/26.64 % TRYING [10]
% 76.64/26.64 % TRYING [10]
% 76.64/26.64 % (3060358)Instruction limit reached!
% 76.64/26.64 % (3060358)------------------------------
% 76.64/26.64 % (3060358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.64/26.64 % (3060358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.64/26.64 % (3060358)CaDiCaL version: 2.1.3
% 76.64/26.64 % (3060358)Termination reason: Instruction limit
% 76.64/26.64 % (3060358)Termination phase: Saturation
% 76.64/26.64 % (3060358)Time elapsed: 4.736 s
% 76.64/26.64 % (3060358)Peak memory usage: 53 MB
% 76.64/26.64 % (3060358)Instructions burned: 5211 (million)
% 76.64/26.64 % (3060368)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3284092130:i=5497:nm=2_2753 on theBenchmark for (2753ds/5497Mi)
% 76.64/26.64 % TRYING [17]
% 76.64/26.64 % (3060354) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3060247-3060354"...
% 76.64/26.64 % (3060354)...printing done.
% 76.64/26.64 % (3060354)Refutation found. Thanks to Tanya!
% 76.64/26.64 % SZS status Unsatisfiable for theBenchmark
% 76.64/26.64 % SZS output start Proof for theBenchmark
% See solution above
% 76.64/26.64 % (3060354)------------------------------
% 76.64/26.64 % (3060354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.64/26.64 % (3060354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.64/26.64 % (3060354)CaDiCaL version: 2.1.3
% 76.64/26.64 % (3060354)Termination reason: Refutation
% 76.64/26.64 % (3060354)Time elapsed: 7.894 s
% 76.64/26.64 % (3060354)Peak memory usage: 84 MB
% 76.64/26.64 % (3060354)Instructions burned: 8801 (million)
% 76.64/26.64 % (3060247)Success in time 26.309 s
% 76.64/26.64 % Vampire exiting
%------------------------------------------------------------------------------