%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR061+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:42:28 AM UTC 2026
% Result : Theorem 1.89s 1.86s
% Output : Refutation 6.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 21
% Syntax : Number of formulae : 83 ( 47 unt; 0 def)
% Number of atoms : 136 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 132 ( 79 ~; 44 |; 4 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 53 ( 53 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1312,axiom,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_1312) ).
fof(f1453,axiom,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_1453) ).
fof(f1842,axiom,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_1842) ).
fof(f2292,axiom,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_2292) ).
fof(f2693,axiom,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_2693) ).
fof(f2924,axiom,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_2924) ).
fof(f3283,axiom,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3283) ).
fof(f3521,axiom,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3521) ).
fof(f3853,axiom,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3853) ).
fof(f4060,axiom,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_4060) ).
fof(f4203,axiom,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_4203) ).
fof(f4211,axiom,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_4211) ).
fof(f4231,axiom,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_4231) ).
fof(f4238,axiom,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_4238) ).
fof(f4338,axiom,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_4338) ).
fof(f4394,axiom,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_4394) ).
fof(f4483,axiom,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_4483) ).
fof(f7585,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X1) )
=> disjointwith(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_7585) ).
fof(f7586,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X0) )
=> disjointwith(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_7586) ).
fof(f7995,axiom,
! [X0,X1,X2] :
( ( genls(X0,X1)
& genls(X1,X2) )
=> genls(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_7995) ).
fof(f8006,conjecture,
( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query161) ).
fof(f8007,negated_conjecture,
~ ( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
inference(negated_conjecture,[status(cth)],[f8006]) ).
fof(f8008,plain,
( ~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118)
& mtvisible(c_timehasnoendmt) ),
inference(ennf_transformation,[],[f8007]) ).
fof(f8011,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(ennf_transformation,[],[f7586]) ).
fof(f8012,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(flattening,[],[f8011]) ).
fof(f8013,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(ennf_transformation,[],[f7585]) ).
fof(f8014,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(flattening,[],[f8013]) ).
fof(f8024,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ),
inference(ennf_transformation,[],[f7995]) ).
fof(f8025,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ),
inference(flattening,[],[f8024]) ).
fof(f8116,plain,
~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(cnf_transformation,[],[f8008]) ).
fof(f8118,plain,
! [X2,X0,X1] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(cnf_transformation,[],[f8012]) ).
fof(f8119,plain,
! [X2,X0,X1] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(cnf_transformation,[],[f8014]) ).
fof(f8134,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
inference(cnf_transformation,[],[f1312]) ).
fof(f8136,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
inference(cnf_transformation,[],[f4483]) ).
fof(f8139,plain,
! [X2,X0,X1] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ),
inference(cnf_transformation,[],[f8025]) ).
fof(f8169,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
inference(cnf_transformation,[],[f4060]) ).
fof(f8173,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
inference(cnf_transformation,[],[f4203]) ).
fof(f8186,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
inference(cnf_transformation,[],[f4394]) ).
fof(f8192,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
inference(cnf_transformation,[],[f1842]) ).
fof(f8204,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
inference(cnf_transformation,[],[f4338]) ).
fof(f8210,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
inference(cnf_transformation,[],[f4238]) ).
fof(f8217,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
inference(cnf_transformation,[],[f1453]) ).
fof(f8223,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(cnf_transformation,[],[f4231]) ).
fof(f8229,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
inference(cnf_transformation,[],[f2693]) ).
fof(f8239,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
inference(cnf_transformation,[],[f4211]) ).
fof(f8245,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
inference(cnf_transformation,[],[f2292]) ).
fof(f8251,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
inference(cnf_transformation,[],[f3283]) ).
fof(f8257,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
inference(cnf_transformation,[],[f2924]) ).
fof(f8263,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
inference(cnf_transformation,[],[f3521]) ).
fof(f8269,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(cnf_transformation,[],[f3853]) ).
fof(f8394,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_14_118118)
| ~ genls(c_tptpcol_8_114177,X0) ),
inference(resolution,[],[f8118,f8116]) ).
fof(f8403,plain,
! [X0,X1] :
( ~ disjointwith(X0,X1)
| ~ genls(c_tptpcol_14_118118,X1)
| ~ genls(c_tptpcol_8_114177,X0) ),
inference(resolution,[],[f8119,f8394]) ).
fof(f8431,plain,
( ~ genls(c_tptpcol_8_114177,c_tptpcol_3_98305)
| ~ genls(c_tptpcol_14_118118,c_tptpcol_3_114688) ),
inference(resolution,[],[f8403,f8269]) ).
fof(f8434,plain,
! [X0] :
( ~ genls(c_tptpcol_8_114177,X0)
| ~ genls(c_tptpcol_14_118118,c_tptpcol_3_114688)
| ~ genls(X0,c_tptpcol_3_98305) ),
inference(resolution,[],[f8431,f8139]) ).
fof(f8554,plain,
( ~ genls(c_tptpcol_7_113665,c_tptpcol_3_98305)
| ~ genls(c_tptpcol_14_118118,c_tptpcol_3_114688) ),
inference(resolution,[],[f8434,f8136]) ).
fof(f8579,plain,
! [X0] :
( ~ genls(c_tptpcol_7_113665,X0)
| ~ genls(c_tptpcol_14_118118,c_tptpcol_3_114688)
| ~ genls(X0,c_tptpcol_3_98305) ),
inference(resolution,[],[f8554,f8139]) ).
fof(f8741,plain,
( ~ genls(c_tptpcol_6_112641,c_tptpcol_3_98305)
| ~ genls(c_tptpcol_14_118118,c_tptpcol_3_114688) ),
inference(resolution,[],[f8579,f8173]) ).
fof(f8764,plain,
! [X0] :
( ~ genls(c_tptpcol_6_112641,X0)
| ~ genls(c_tptpcol_14_118118,c_tptpcol_3_114688)
| ~ genls(X0,c_tptpcol_3_98305) ),
inference(resolution,[],[f8741,f8139]) ).
fof(f8929,plain,
( ~ genls(c_tptpcol_5_110593,c_tptpcol_3_98305)
| ~ genls(c_tptpcol_14_118118,c_tptpcol_3_114688) ),
inference(resolution,[],[f8764,f8192]) ).
fof(f8947,plain,
! [X0] :
( ~ genls(c_tptpcol_5_110593,X0)
| ~ genls(c_tptpcol_14_118118,c_tptpcol_3_114688)
| ~ genls(X0,c_tptpcol_3_98305) ),
inference(resolution,[],[f8929,f8139]) ).
fof(f8988,plain,
( ~ genls(c_tptpcol_14_118118,c_tptpcol_3_114688)
| ~ genls(c_tptpcol_4_106497,c_tptpcol_3_98305) ),
inference(resolution,[],[f8947,f8210]) ).
fof(f8991,plain,
~ genls(c_tptpcol_14_118118,c_tptpcol_3_114688),
inference(forward_subsumption_resolution,[],[f8988,f8223]) ).
fof(f8993,plain,
! [X0] :
( ~ genls(c_tptpcol_14_118118,X0)
| ~ genls(X0,c_tptpcol_3_114688) ),
inference(resolution,[],[f8991,f8139]) ).
fof(f8994,plain,
~ genls(c_tptpcol_13_118117,c_tptpcol_3_114688),
inference(resolution,[],[f8993,f8134]) ).
fof(f8998,plain,
! [X0] :
( ~ genls(c_tptpcol_13_118117,X0)
| ~ genls(X0,c_tptpcol_3_114688) ),
inference(resolution,[],[f8994,f8139]) ).
fof(f9000,plain,
~ genls(c_tptpcol_12_118116,c_tptpcol_3_114688),
inference(resolution,[],[f8998,f8169]) ).
fof(f9003,plain,
! [X0] :
( ~ genls(c_tptpcol_12_118116,X0)
| ~ genls(X0,c_tptpcol_3_114688) ),
inference(resolution,[],[f9000,f8139]) ).
fof(f9005,plain,
~ genls(c_tptpcol_11_118084,c_tptpcol_3_114688),
inference(resolution,[],[f9003,f8186]) ).
fof(f9009,plain,
! [X0] :
( ~ genls(c_tptpcol_11_118084,X0)
| ~ genls(X0,c_tptpcol_3_114688) ),
inference(resolution,[],[f9005,f8139]) ).
fof(f9010,plain,
~ genls(c_tptpcol_10_118020,c_tptpcol_3_114688),
inference(resolution,[],[f9009,f8204]) ).
fof(f9014,plain,
! [X0] :
( ~ genls(c_tptpcol_10_118020,X0)
| ~ genls(X0,c_tptpcol_3_114688) ),
inference(resolution,[],[f9010,f8139]) ).
fof(f9016,plain,
~ genls(c_tptpcol_9_118019,c_tptpcol_3_114688),
inference(resolution,[],[f9014,f8217]) ).
fof(f9019,plain,
! [X0] :
( ~ genls(c_tptpcol_9_118019,X0)
| ~ genls(X0,c_tptpcol_3_114688) ),
inference(resolution,[],[f9016,f8139]) ).
fof(f9021,plain,
~ genls(c_tptpcol_8_117763,c_tptpcol_3_114688),
inference(resolution,[],[f9019,f8229]) ).
fof(f9025,plain,
! [X0] :
( ~ genls(c_tptpcol_8_117763,X0)
| ~ genls(X0,c_tptpcol_3_114688) ),
inference(resolution,[],[f9021,f8139]) ).
fof(f9026,plain,
~ genls(c_tptpcol_7_117762,c_tptpcol_3_114688),
inference(resolution,[],[f9025,f8239]) ).
fof(f9030,plain,
! [X0] :
( ~ genls(c_tptpcol_7_117762,X0)
| ~ genls(X0,c_tptpcol_3_114688) ),
inference(resolution,[],[f9026,f8139]) ).
fof(f9032,plain,
~ genls(c_tptpcol_6_116738,c_tptpcol_3_114688),
inference(resolution,[],[f9030,f8245]) ).
fof(f9035,plain,
! [X0] :
( ~ genls(c_tptpcol_6_116738,X0)
| ~ genls(X0,c_tptpcol_3_114688) ),
inference(resolution,[],[f9032,f8139]) ).
fof(f9037,plain,
~ genls(c_tptpcol_5_114690,c_tptpcol_3_114688),
inference(resolution,[],[f9035,f8251]) ).
fof(f9041,plain,
! [X0] :
( ~ genls(c_tptpcol_5_114690,X0)
| ~ genls(X0,c_tptpcol_3_114688) ),
inference(resolution,[],[f9037,f8139]) ).
fof(f9042,plain,
~ genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
inference(resolution,[],[f9041,f8257]) ).
fof(f9045,plain,
$false,
inference(forward_subsumption_resolution,[],[f9042,f8263]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR061+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.29 % Computer : n008.cluster.edu
% 0.13/0.29 % Model : x86_64 x86_64
% 0.13/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.29 % Memory : 8046.5625MB
% 0.13/0.29 % OS : Linux 6.8.0-71-generic
% 0.13/0.29 % CPULimit : 300
% 0.13/0.29 % WCLimit : 300
% 0.13/0.29 % DateTime : Mon Sep 28 22:22:39 UTC 2026
% 0.13/0.30 % CPUTime :
% 0.13/0.30 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.32/0.34 Running first-order theorem proving
% 0.32/0.34 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.89/1.86 % (2726679)Detected formulas, will run a generic FOF schedule.
% 1.89/1.86 % (2726686)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2993677871:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 1.89/1.86 % (2726684)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=305534039:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 1.89/1.86 % (2726685)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=474789631:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 1.89/1.86 % (2726689)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3510361437:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 1.89/1.86 % (2726688)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3102859180:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 1.89/1.86 % (2726687)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=592689889:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 1.89/1.86 % (2726690)dis-21_1_sil=8000:lcm=predicate:random_seed=757304190:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 1.89/1.86 % (2726687)Refutation not found, incomplete strategy
% 1.89/1.86 % (2726687)------------------------------
% 1.89/1.86 % (2726687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.89/1.86 % (2726687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/1.86 % (2726687)CaDiCaL version: 2.1.3
% 1.89/1.86 % (2726687)Termination reason: Refutation not found, incomplete strategy
% 1.89/1.86 % (2726687)Time elapsed: 0.026 s
% 1.89/1.86 % (2726687)Peak memory usage: 93 MB
% 1.89/1.86 % (2726687)Instructions burned: 24 (million)
% 1.89/1.86 % (2726688)First to succeed.
% 1.89/1.86 % (2726688)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2726679"
% 1.89/1.86 % (2726690)Instruction limit reached!
% 1.89/1.86 % (2726690)------------------------------
% 1.89/1.86 % (2726690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.89/1.86 % (2726690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/1.86 % (2726690)CaDiCaL version: 2.1.3
% 1.89/1.86 % (2726690)Termination reason: Instruction limit
% 1.89/1.86 % (2726690)Termination phase: Saturation
% 1.89/1.86 % (2726690)Time elapsed: 0.126 s
% 1.89/1.86 % (2726690)Peak memory usage: 95 MB
% 1.89/1.86 % (2726690)Instructions burned: 129 (million)
% 1.89/1.86 % (2726689)Instruction limit reached!
% 1.89/1.86 % (2726689)------------------------------
% 1.89/1.86 % (2726689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.89/1.86 % (2726689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/1.86 % (2726689)CaDiCaL version: 2.1.3
% 1.89/1.86 % (2726689)Termination reason: Instruction limit
% 1.89/1.86 % (2726689)Termination phase: Property scanning
% 1.89/1.86 % (2726689)Time elapsed: 0.141 s
% 1.89/1.86 % (2726689)Peak memory usage: 93 MB
% 1.89/1.86 % (2726689)Instructions burned: 140 (million)
% 1.89/1.86 % (2726698)lrs+10_1_sil=8000:sp=occurrence:random_seed=1718301181:i=285:sd=3:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/285Mi)
% 1.89/1.86 % (2726699)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1522225868:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/157Mi)
% 1.89/1.86 % (2726698)Refutation not found, incomplete strategy
% 1.89/1.86 % (2726698)------------------------------
% 1.89/1.86 % (2726698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.89/1.86 % (2726698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/1.86 % (2726698)CaDiCaL version: 2.1.3
% 1.89/1.86 % (2726698)Termination reason: Refutation not found, incomplete strategy
% 1.89/1.86 % (2726698)Time elapsed: 0.035 s
% 1.89/1.86 % (2726698)Peak memory usage: 94 MB
% 1.89/1.86 % (2726698)Instructions burned: 27 (million)
% 1.89/1.86 % (2726687)------------------------------
% 1.89/1.86 % (2726687)------------------------------
% 1.89/1.86 % (2726688)Refutation found. Thanks to Tanya!
% 1.89/1.86 % SZS status Theorem for theBenchmark
% 1.89/1.86 % SZS output start Proof for theBenchmark
% See solution above
% 6.28/2.25 % (2726688)------------------------------
% 6.28/2.25 % (2726688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/2.25 % (2726688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/2.25 % (2726688)CaDiCaL version: 2.1.3
% 6.28/2.25 % (2726688)Termination reason: Refutation
% 6.28/2.25 % (2726688)Time elapsed: 0.046 s
% 6.28/2.25 % (2726688)Peak memory usage: 94 MB
% 6.28/2.25 % (2726688)Instructions burned: 44 (million)
% 6.28/2.25 % (2726688)------------------------------
% 6.28/2.25 % (2726688)------------------------------
% 6.28/2.25 % (2726679)Success in time 0.856 s
% 6.28/2.25 % Vampire exiting
%------------------------------------------------------------------------------