%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : COL011-1 : TPTP v9.3.1. Released v1.0.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 09:38:10 AM UTC 2026
% Result : Unsatisfiable 42.35s 13.81s
% Output : Refutation 42.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 3
% Syntax : Number of formulae : 9 ( 9 unt; 0 def)
% Number of atoms : 9 ( 8 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 19 ( 19 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : apply(apply(o,X0),X1) = apply(X1,apply(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o_definition) ).
fof(f2,axiom,
! [X2,X0,X1] : apply(apply(apply(q1,X0),X1),X2) = apply(X0,apply(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',q1_definition) ).
fof(f3,negated_conjecture,
! [X0] : X0 != apply(combinator,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_fixed_point) ).
fof(f4,plain,
! [X0] : apply(combinator,X0) != X0,
inference(reorient_equations,[],[f3]) ).
fof(f10,plain,
! [X2,X3,X0,X1] : apply(apply(X1,X0),apply(X3,X2)) = apply(apply(apply(apply(apply(q1,q1),X0),X1),X2),X3),
inference(superposition,[],[f2,f2]) ).
fof(f22,plain,
! [X0,X1] : apply(X1,X0) != apply(apply(apply(q1,combinator),X0),X1),
inference(superposition,[],[f4,f2]) ).
fof(f31,plain,
! [X2,X0,X1] : apply(X2,apply(X1,X0)) != apply(apply(apply(apply(q1,apply(q1,combinator)),X0),X1),X2),
inference(superposition,[],[f22,f2]) ).
fof(f211,plain,
! [X2,X0,X1] : apply(X2,apply(X0,apply(X1,X0))) != apply(apply(apply(apply(q1,apply(q1,combinator)),X0),apply(o,X1)),X2),
inference(superposition,[],[f31,f1]) ).
fof(f15656,plain,
$false,
inference(unit_resulting_resolution,[],[f10,f211]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COL011-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.19 % Computer : n011.cluster.edu
% 0.11/0.19 % Model : x86_64 x86_64
% 0.11/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.19 % Memory : 8046.5625MB
% 0.11/0.19 % OS : Linux 6.8.0-71-generic
% 0.11/0.19 % CPULimit : 300
% 0.11/0.20 % WCLimit : 300
% 0.11/0.20 % DateTime : Mon Sep 28 21:29:46 UTC 2026
% 0.11/0.20 % CPUTime :
% 0.11/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.23 Running first-order model finding
% 0.11/0.23 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
% 16.76/2.72 % (3802195)Will run a generic schedule for satisfiability detection.
% 16.76/2.72 % (3802212)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=780570846:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.76/2.72 % (3802211)% WARNING: option uhcvi not known.
% 16.76/2.72 % (3802210)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2525585008_2999 on theBenchmark for (2999ds/0Mi)
% 16.76/2.72 % (3802211)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3867404505:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.76/2.72 % (3802214)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2756860234:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.76/2.72 % (3802213)dis+10_1_sil=32000:sp=arity:random_seed=938051775:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.76/2.72 % (3802215)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3504441747:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.76/2.72 % TRYING [1]
% 16.76/2.72 % (3802216)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3154666782:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.76/2.72 % TRYING [2]
% 16.76/2.72 % TRYING [3]
% 16.76/2.72 % TRYING [4]
% 16.76/2.72 % TRYING [5]
% 16.76/2.72 % (3802213)Instruction limit reached!
% 16.76/2.72 % (3802213)------------------------------
% 16.76/2.72 % (3802213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.76/2.72 % (3802213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.76/2.72 % (3802213)CaDiCaL version: 2.1.3
% 16.76/2.72 % (3802213)Termination reason: Instruction limit
% 16.76/2.72 % (3802213)Termination phase: Saturation
% 16.76/2.72 % (3802213)Time elapsed: 0.058 s
% 16.76/2.72 % (3802213)Peak memory usage: 12 MB
% 16.76/2.72 % (3802213)Instructions burned: 104 (million)
% 16.76/2.72 % (3802214)Instruction limit reached!
% 16.76/2.72 % (3802214)------------------------------
% 16.76/2.72 % (3802214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.76/2.72 % (3802214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.76/2.72 % (3802214)CaDiCaL version: 2.1.3
% 16.76/2.72 % (3802214)Termination reason: Instruction limit
% 16.76/2.72 % (3802214)Termination phase: Saturation
% 16.76/2.72 % (3802214)Time elapsed: 0.073 s
% 16.76/2.72 % (3802214)Peak memory usage: 12 MB
% 16.76/2.72 % (3802214)Instructions burned: 117 (million)
% 16.76/2.72 % (3802244)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=373512178:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.76/2.72 % TRYING [1]
% 16.76/2.72 % TRYING [2]
% 16.76/2.72 % TRYING [3]
% 16.76/2.72 % TRYING [4]
% 16.76/2.72 % (3802215)Instruction limit reached!
% 16.76/2.72 % (3802215)------------------------------
% 16.76/2.72 % (3802215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.76/2.72 % (3802215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.76/2.72 % (3802215)CaDiCaL version: 2.1.3
% 16.76/2.72 % (3802215)Termination reason: Instruction limit
% 16.76/2.72 % (3802215)Termination phase: Saturation
% 16.76/2.72 % (3802215)Time elapsed: 0.084 s
% 16.76/2.72 % (3802215)Peak memory usage: 13 MB
% 16.76/2.72 % (3802215)Instructions burned: 131 (million)
% 16.76/2.72 % (3802250)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=14239162:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.76/2.72 % (3802216)Instruction limit reached!
% 16.76/2.72 % (3802216)------------------------------
% 16.76/2.72 % (3802216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.76/2.72 % (3802216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.76/2.72 % (3802216)CaDiCaL version: 2.1.3
% 16.76/2.72 % (3802216)Termination reason: Instruction limit
% 16.76/2.72 % (3802216)Termination phase: Saturation
% 16.76/2.72 % (3802216)Time elapsed: 0.100 s
% 16.76/2.72 % (3802216)Peak memory usage: 13 MB
% 16.76/2.72 % (3802216)Instructions burned: 160 (million)
% 16.76/2.72 % (3802255)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=2557368038:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.76/2.72 % (3802263)ott-21_1_sil=16000:fs=off:random_seed=3943234935:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.76/2.72 % TRYING [5]
% 16.76/2.72 % (3802250)Instruction limit reached!
% 16.76/2.72 % (3802250)------------------------------
% 16.76/2.72 % (3802250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.47/7.57 % (3802250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.47/7.57 % (3802250)CaDiCaL version: 2.1.3
% 51.47/7.57 % (3802250)Termination reason: Instruction limit
% 51.47/7.57 % (3802250)Termination phase: Saturation
% 51.47/7.57 % (3802250)Time elapsed: 0.085 s
% 51.47/7.57 % (3802250)Peak memory usage: 13 MB
% 51.47/7.57 % (3802250)Instructions burned: 131 (million)
% 51.47/7.57 % (3802299)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3265420521:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 51.47/7.57 % (3802263)Instruction limit reached!
% 51.47/7.57 % (3802263)------------------------------
% 51.47/7.57 % (3802263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.47/7.57 % (3802263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.47/7.57 % (3802263)CaDiCaL version: 2.1.3
% 51.47/7.57 % (3802263)Termination reason: Instruction limit
% 51.47/7.57 % (3802263)Termination phase: Saturation
% 51.47/7.57 % (3802263)Time elapsed: 0.097 s
% 51.47/7.57 % (3802263)Peak memory usage: 12 MB
% 51.47/7.57 % (3802263)Instructions burned: 181 (million)
% 51.47/7.57 % (3802301)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=329675672:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 51.47/7.57 % TRYING [1]
% 51.47/7.57 % TRYING [2]
% 51.47/7.57 % TRYING [3]
% 51.47/7.57 % TRYING [6]
% 51.47/7.57 % TRYING [4]
% 51.47/7.57 % TRYING [5]
% 51.47/7.57 % TRYING [6]
% 51.47/7.57 % TRYING [6]
% 51.47/7.57 % (3802299)Instruction limit reached!
% 51.47/7.57 % (3802299)------------------------------
% 51.47/7.57 % (3802299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.47/7.57 % (3802299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.47/7.57 % (3802299)CaDiCaL version: 2.1.3
% 51.47/7.57 % (3802299)Termination reason: Instruction limit
% 51.47/7.57 % (3802299)Termination phase: Saturation
% 51.47/7.57 % (3802299)Time elapsed: 0.261 s
% 51.47/7.57 % (3802299)Peak memory usage: 16 MB
% 51.47/7.57 % (3802299)Instructions burned: 478 (million)
% 51.47/7.57 % (3802303)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1281433702:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 51.47/7.57 % (3802255)Instruction limit reached!
% 51.47/7.57 % (3802255)------------------------------
% 51.47/7.57 % (3802255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.47/7.57 % (3802255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.47/7.57 % (3802255)CaDiCaL version: 2.1.3
% 51.47/7.57 % (3802255)Termination reason: Instruction limit
% 51.47/7.57 % (3802255)Termination phase: Saturation
% 51.47/7.57 % (3802255)Time elapsed: 0.376 s
% 51.47/7.57 % (3802255)Peak memory usage: 18 MB
% 51.47/7.57 % (3802255)Instructions burned: 684 (million)
% 51.47/7.57 % (3802244)Instruction limit reached!
% 51.47/7.57 % (3802244)------------------------------
% 51.47/7.57 % (3802244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.47/7.57 % (3802244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.47/7.57 % (3802244)CaDiCaL version: 2.1.3
% 51.47/7.57 % (3802244)Termination reason: Instruction limit
% 51.47/7.57 % (3802244)Termination phase: Finite model building SAT solving
% 51.47/7.57 % (3802244)Time elapsed: 0.413 s
% 51.47/7.57 % (3802244)Peak memory usage: 16 MB
% 51.47/7.57 % (3802244)Instructions burned: 714 (million)
% 51.47/7.57 % (3802305)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4232585559:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 51.47/7.57 % (3802306)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=1089149272:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 51.47/7.57 % TRYING [14]
% 51.47/7.57 % (3802301)Instruction limit reached!
% 51.47/7.57 % (3802301)------------------------------
% 51.47/7.57 % (3802301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.47/7.57 % (3802301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.47/7.57 % (3802301)CaDiCaL version: 2.1.3
% 51.47/7.57 % (3802301)Termination reason: Instruction limit
% 51.47/7.57 % (3802301)Termination phase: Finite model building SAT solving
% 51.47/7.57 % (3802301)Time elapsed: 0.460 s
% 51.47/7.57 % (3802301)Peak memory usage: 14 MB
% 51.47/7.57 % (3802301)Instructions burned: 866 (million)
% 51.47/7.57 % (3802309)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1821082611:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 51.47/7.57 % (3802305)Instruction limit reached!
% 42.35/13.80 % (3802305)------------------------------
% 42.35/13.80 % (3802305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.80 % (3802305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.80 % (3802305)CaDiCaL version: 2.1.3
% 42.35/13.80 % (3802305)Termination reason: Instruction limit
% 42.35/13.80 % (3802305)Termination phase: Finite model building constraint generation
% 42.35/13.80 % (3802305)Time elapsed: 0.319 s
% 42.35/13.80 % (3802305)Peak memory usage: 79 MB
% 42.35/13.80 % (3802305)Instructions burned: 890 (million)
% 42.35/13.80 % (3802311)fmb+10_1_sil=64000:random_seed=1269521032:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 42.35/13.80 % TRYING [1]
% 42.35/13.80 % TRYING [2]
% 42.35/13.80 % TRYING [3]
% 42.35/13.80 % TRYING [4]
% 42.35/13.80 % TRYING [5]
% 42.35/13.80 % (3802306)Instruction limit reached!
% 42.35/13.80 % (3802306)------------------------------
% 42.35/13.80 % (3802306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.80 % (3802306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.80 % (3802306)CaDiCaL version: 2.1.3
% 42.35/13.80 % (3802306)Termination reason: Instruction limit
% 42.35/13.80 % (3802306)Termination phase: Saturation
% 42.35/13.80 % (3802306)Time elapsed: 0.424 s
% 42.35/13.80 % (3802306)Peak memory usage: 18 MB
% 42.35/13.80 % (3802306)Instructions burned: 692 (million)
% 42.35/13.80 % (3802313)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1657522086:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 42.35/13.80 % TRYING [20]
% 42.35/13.80 % TRYING [6]
% 42.35/13.80 % TRYING [7]
% 42.35/13.80 % (3802309)Instruction limit reached!
% 42.35/13.80 % (3802309)------------------------------
% 42.35/13.80 % (3802309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.80 % (3802309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.80 % (3802309)CaDiCaL version: 2.1.3
% 42.35/13.80 % (3802309)Termination reason: Instruction limit
% 42.35/13.80 % (3802309)Termination phase: Saturation
% 42.35/13.80 % (3802309)Time elapsed: 0.478 s
% 42.35/13.80 % (3802309)Peak memory usage: 19 MB
% 42.35/13.80 % (3802309)Instructions burned: 879 (million)
% 42.35/13.80 % (3802315)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=680703482:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 42.35/13.80 % TRYING [8]
% 42.35/13.80 % (3802303)Instruction limit reached!
% 42.35/13.80 % (3802303)------------------------------
% 42.35/13.80 % (3802303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.80 % (3802303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.80 % (3802303)CaDiCaL version: 2.1.3
% 42.35/13.80 % (3802303)Termination reason: Instruction limit
% 42.35/13.80 % (3802303)Termination phase: Saturation
% 42.35/13.80 % (3802303)Time elapsed: 0.787 s
% 42.35/13.80 % (3802303)Peak memory usage: 25 MB
% 42.35/13.80 % (3802303)Instructions burned: 1180 (million)
% 42.35/13.80 % (3802317)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2290205311:i=5131_2986 on theBenchmark for (2986ds/5131Mi)
% 42.35/13.80 % TRYING [7]
% 42.35/13.80 % (3802315)Instruction limit reached!
% 42.35/13.80 % (3802315)------------------------------
% 42.35/13.80 % (3802315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.80 % (3802315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.80 % (3802315)CaDiCaL version: 2.1.3
% 42.35/13.80 % (3802315)Termination reason: Instruction limit
% 42.35/13.80 % (3802315)Termination phase: Finite model building SAT solving
% 42.35/13.80 % (3802315)Time elapsed: 0.510 s
% 42.35/13.80 % (3802315)Peak memory usage: 33 MB
% 42.35/13.80 % (3802315)Instructions burned: 926 (million)
% 42.35/13.80 % (3802319)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1935745755:i=1472:ins=7:fdi=8:gsp=on_2982 on theBenchmark for (2982ds/1472Mi)
% 42.35/13.80 % (3802319)Instruction limit reached!
% 42.35/13.80 % (3802319)------------------------------
% 42.35/13.80 % (3802319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.80 % (3802319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.80 % (3802319)CaDiCaL version: 2.1.3
% 42.35/13.80 % (3802319)Termination reason: Instruction limit
% 42.35/13.80 % (3802319)Termination phase: Saturation
% 42.35/13.80 % (3802319)Time elapsed: 0.671 s
% 42.35/13.80 % (3802319)Peak memory usage: 24 MB
% 42.35/13.80 % (3802319)Instructions burned: 1473 (million)
% 42.35/13.80 % (3802321)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=11338395:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 42.35/13.80 % TRYING [77]
% 42.35/13.80 % TRYING [8]
% 42.35/13.80 % TRYING [8]
% 42.35/13.80 % (3802317)Instruction limit reached!
% 42.35/13.80 % (3802317)------------------------------
% 42.35/13.80 % (3802317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.80 % (3802317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.80 % (3802317)CaDiCaL version: 2.1.3
% 42.35/13.80 % (3802317)Termination reason: Instruction limit
% 42.35/13.80 % (3802317)Termination phase: Saturation
% 42.35/13.80 % (3802317)Time elapsed: 2.879 s
% 42.35/13.80 % (3802317)Peak memory usage: 55 MB
% 42.35/13.80 % (3802317)Instructions burned: 5131 (million)
% 42.35/13.80 % (3802323)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2641247579:fmbsr=2.30978:i=2174_2957 on theBenchmark for (2957ds/2174Mi)
% 42.35/13.80 % TRYING [16]
% 42.35/13.80 % (3802313)Instruction limit reached!
% 42.35/13.80 % (3802313)------------------------------
% 42.35/13.80 % (3802313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.80 % (3802313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.80 % (3802313)CaDiCaL version: 2.1.3
% 42.35/13.80 % (3802313)Termination reason: Instruction limit
% 42.35/13.80 % (3802313)Termination phase: Finite model building constraint generation
% 42.35/13.80 % (3802313)Time elapsed: 3.643 s
% 42.35/13.80 % (3802313)Peak memory usage: 641 MB
% 42.35/13.80 % (3802313)Instructions burned: 9516 (million)
% 42.35/13.80 % (3802325)ott-2_1_sil=16000:newcnf=on:random_seed=4152662673:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2952 on theBenchmark for (2952ds/869Mi)
% 42.35/13.80 % (3802321)Instruction limit reached!
% 42.35/13.80 % (3802321)------------------------------
% 42.35/13.80 % (3802321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.80 % (3802321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.80 % (3802321)CaDiCaL version: 2.1.3
% 42.35/13.80 % (3802321)Termination reason: Instruction limit
% 42.35/13.80 % (3802321)Termination phase: Finite model building constraint generation
% 42.35/13.80 % (3802321)Time elapsed: 2.313 s
% 42.35/13.80 % (3802321)Peak memory usage: 420 MB
% 42.35/13.80 % (3802321)Instructions burned: 6325 (million)
% 42.35/13.80 % (3802327)ott+10_1_sil=32000:tgt=ground:random_seed=893409024:i=5114:av=off_2951 on theBenchmark for (2951ds/5114Mi)
% 42.35/13.81 % (3802323)Instruction limit reached!
% 42.35/13.81 % (3802323)------------------------------
% 42.35/13.81 % (3802323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.81 % (3802323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.81 % (3802323)CaDiCaL version: 2.1.3
% 42.35/13.81 % (3802323)Termination reason: Instruction limit
% 42.35/13.81 % (3802323)Termination phase: Finite model building constraint generation
% 42.35/13.81 % (3802323)Time elapsed: 0.803 s
% 42.35/13.81 % (3802323)Peak memory usage: 153 MB
% 42.35/13.81 % (3802323)Instructions burned: 2174 (million)
% 42.35/13.81 % (3802329)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2011056071:i=54282_2949 on theBenchmark for (2949ds/54282Mi)
% 42.35/13.81 % TRYING [1]
% 42.35/13.81 % TRYING [2]
% 42.35/13.81 % TRYING [3]
% 42.35/13.81 % TRYING [4]
% 42.35/13.81 % TRYING [5]
% 42.35/13.81 % (3802325)Instruction limit reached!
% 42.35/13.81 % (3802325)------------------------------
% 42.35/13.81 % (3802325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.81 % (3802325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.81 % (3802325)CaDiCaL version: 2.1.3
% 42.35/13.81 % (3802325)Termination reason: Instruction limit
% 42.35/13.81 % (3802325)Termination phase: Saturation
% 42.35/13.81 % (3802325)Time elapsed: 0.578 s
% 42.35/13.81 % (3802325)Peak memory usage: 22 MB
% 42.35/13.81 % (3802325)Instructions burned: 869 (million)
% 42.35/13.81 % TRYING [6]
% 42.35/13.81 % (3802331)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2069905029:i=3512:aac=none_2946 on theBenchmark for (2946ds/3512Mi)
% 42.35/13.81 % TRYING [7]
% 42.35/13.81 % (3802331)Instruction limit reached!
% 42.35/13.81 % (3802331)------------------------------
% 42.35/13.81 % (3802331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.81 % (3802331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.81 % (3802331)CaDiCaL version: 2.1.3
% 42.35/13.81 % (3802331)Termination reason: Instruction limit
% 42.35/13.81 % (3802331)Termination phase: Saturation
% 42.35/13.81 % (3802331)Time elapsed: 1.972 s
% 42.35/13.81 % (3802331)Peak memory usage: 46 MB
% 42.35/13.81 % (3802331)Instructions burned: 3512 (million)
% 42.35/13.81 % (3802333)dis+21_1_sil=32000:sas=cadical:random_seed=3491168864:i=3773:amm=off_2926 on theBenchmark for (2926ds/3773Mi)
% 42.35/13.81 % (3802327)Instruction limit reached!
% 42.35/13.81 % (3802327)------------------------------
% 42.35/13.81 % (3802327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.81 % (3802327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.81 % (3802327)CaDiCaL version: 2.1.3
% 42.35/13.81 % (3802327)Termination reason: Instruction limit
% 42.35/13.81 % (3802327)Termination phase: Saturation
% 42.35/13.81 % (3802327)Time elapsed: 3.760 s
% 42.35/13.81 % (3802327)Peak memory usage: 67 MB
% 42.35/13.81 % (3802327)Instructions burned: 5115 (million)
% 42.35/13.81 % (3802335)ott+11_1_sil=16000:gs=on:random_seed=2124556434:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2913 on theBenchmark for (2913ds/2251Mi)
% 42.35/13.81 % TRYING [8]
% 42.35/13.81 % (3802333)Instruction limit reached!
% 42.35/13.81 % (3802333)------------------------------
% 42.35/13.81 % (3802333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.81 % (3802333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.81 % (3802333)CaDiCaL version: 2.1.3
% 42.35/13.81 % (3802333)Termination reason: Instruction limit
% 42.35/13.81 % (3802333)Termination phase: Saturation
% 42.35/13.81 % (3802333)Time elapsed: 2.140 s
% 42.35/13.81 % (3802333)Peak memory usage: 50 MB
% 42.35/13.81 % (3802333)Instructions burned: 3773 (million)
% 42.35/13.81 % (3802337)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2360622065:fmbsr=1.6:i=67534_2905 on theBenchmark for (2905ds/67534Mi)
% 42.35/13.81 % TRYING [7]
% 42.35/13.81 % (3802335)Instruction limit reached!
% 42.35/13.81 % (3802335)------------------------------
% 42.35/13.81 % (3802335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.81 % (3802335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.81 % (3802335)CaDiCaL version: 2.1.3
% 42.35/13.81 % (3802335)Termination reason: Instruction limit
% 42.35/13.81 % (3802335)Termination phase: Saturation
% 42.35/13.81 % (3802335)Time elapsed: 1.355 s
% 42.35/13.81 % (3802335)Peak memory usage: 35 MB
% 42.35/13.81 % (3802335)Instructions burned: 2252 (million)
% 42.35/13.81 % (3802339)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1877904964:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2899 on theBenchmark for (2899ds/4591Mi)
% 42.35/13.81 % TRYING [9]
% 42.35/13.81 % TRYING [8]
% 42.35/13.81 % (3802339)Instruction limit reached!
% 42.35/13.81 % (3802339)------------------------------
% 42.35/13.81 % (3802339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.81 % (3802339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.81 % (3802339)CaDiCaL version: 2.1.3
% 42.35/13.81 % (3802339)Termination reason: Instruction limit
% 42.35/13.81 % (3802339)Termination phase: Saturation
% 42.35/13.81 % (3802339)Time elapsed: 2.664 s
% 42.35/13.81 % (3802339)Peak memory usage: 88 MB
% 42.35/13.81 % (3802339)Instructions burned: 4591 (million)
% 42.35/13.81 % (3802341)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1040071397:i=29340_2872 on theBenchmark for (2872ds/29340Mi)
% 42.35/13.81 % (3802341) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3802195-3802341"...
% 42.35/13.81 % (3802341)...printing done.
% 42.35/13.81 % (3802341)Refutation found. Thanks to Tanya!
% 42.35/13.81 % SZS status Unsatisfiable for theBenchmark
% 42.35/13.81 % SZS output start Proof for theBenchmark
% See solution above
% 42.35/13.81 % (3802341)------------------------------
% 42.35/13.81 % (3802341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.35/13.81 % (3802341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.35/13.81 % (3802341)CaDiCaL version: 2.1.3
% 42.35/13.81 % (3802341)Termination reason: Refutation
% 42.35/13.81 % (3802341)Time elapsed: 0.807 s
% 42.35/13.81 % (3802341)Peak memory usage: 21 MB
% 42.35/13.81 % (3802341)Instructions burned: 1455 (million)
% 42.35/13.81 % (3802195)Success in time 13.566 s
% 42.35/13.81 % Vampire exiting
%------------------------------------------------------------------------------