%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR061+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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:44:48 AM UTC 2026
% Result : Theorem 1.65s 0.74s
% Output : Refutation 1.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 20
% Syntax : Number of formulae : 83 ( 54 unt; 0 def)
% Number of atoms : 122 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 75 ( 36 ~; 32 |; 3 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 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 : 46 ( 46 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f436,axiom,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_436) ).
fof(f467,axiom,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_467) ).
fof(f716,axiom,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_716) ).
fof(f817,axiom,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_817) ).
fof(f966,axiom,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_966) ).
fof(f976,axiom,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_976) ).
fof(f1323,axiom,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1323) ).
fof(f1417,axiom,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1417) ).
fof(f1422,axiom,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1422) ).
fof(f1914,axiom,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1914) ).
fof(f2341,axiom,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_2341) ).
fof(f2345,axiom,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_2345) ).
fof(f2474,axiom,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_2474) ).
fof(f2515,axiom,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_2515) ).
fof(f3407,axiom,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_3407) ).
fof(f3445,axiom,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_3445) ).
fof(f4158,axiom,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_4158) ).
fof(f7585,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X1) )
=> disjointwith(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_7585) ).
fof(f7586,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X0) )
=> disjointwith(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_7586) ).
fof(f8006,conjecture,
( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
file('/export/starexec/sandbox2/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(f13088,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(ennf_transformation,[],[f7585]) ).
fof(f13089,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(flattening,[],[f13088]) ).
fof(f13090,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(ennf_transformation,[],[f7586]) ).
fof(f13091,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(flattening,[],[f13090]) ).
fof(f13400,plain,
( ~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118)
& mtvisible(c_timehasnoendmt) ),
inference(ennf_transformation,[],[f8007]) ).
fof(f13828,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
inference(cnf_transformation,[],[f436]) ).
fof(f13859,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
inference(cnf_transformation,[],[f467]) ).
fof(f14104,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
inference(cnf_transformation,[],[f716]) ).
fof(f14201,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
inference(cnf_transformation,[],[f817]) ).
fof(f14348,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
inference(cnf_transformation,[],[f966]) ).
fof(f14358,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
inference(cnf_transformation,[],[f976]) ).
fof(f14696,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
inference(cnf_transformation,[],[f1323]) ).
fof(f14789,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
inference(cnf_transformation,[],[f1417]) ).
fof(f14794,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
inference(cnf_transformation,[],[f1422]) ).
fof(f15276,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
inference(cnf_transformation,[],[f1914]) ).
fof(f15698,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
inference(cnf_transformation,[],[f2341]) ).
fof(f15702,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(cnf_transformation,[],[f2345]) ).
fof(f15831,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(cnf_transformation,[],[f2474]) ).
fof(f15871,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
inference(cnf_transformation,[],[f2515]) ).
fof(f16749,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
inference(cnf_transformation,[],[f3407]) ).
fof(f16787,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
inference(cnf_transformation,[],[f3445]) ).
fof(f17487,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
inference(cnf_transformation,[],[f4158]) ).
fof(f20382,plain,
! [X2,X0,X1] :
( ~ genls(X2,X1)
| ~ disjointwith(X0,X1)
| disjointwith(X0,X2) ),
inference(cnf_transformation,[],[f13089]) ).
fof(f20383,plain,
! [X2,X0,X1] :
( ~ genls(X2,X0)
| ~ disjointwith(X0,X1)
| disjointwith(X2,X1) ),
inference(cnf_transformation,[],[f13091]) ).
fof(f20688,plain,
~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(cnf_transformation,[],[f13400]) ).
fof(f22272,plain,
~ disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(consistent_polarity_flipping,[],[f15702]) ).
fof(f25009,plain,
! [X2,X0,X1] :
( ~ disjointwith(X0,X2)
| disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(consistent_polarity_flipping,[],[f20382]) ).
fof(f25010,plain,
! [X2,X0,X1] :
( ~ disjointwith(X2,X1)
| disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(consistent_polarity_flipping,[],[f20383]) ).
fof(f25182,plain,
disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(consistent_polarity_flipping,[],[f20688]) ).
fof(f41380,plain,
! [X0] :
( ~ genls(c_tptpcol_8_114177,X0)
| disjointwith(X0,c_tptpcol_14_118118) ),
inference(resolution,[],[f25010,f25182]) ).
fof(f41394,plain,
disjointwith(c_tptpcol_7_113665,c_tptpcol_14_118118),
inference(resolution,[],[f41380,f13859]) ).
fof(f41396,plain,
! [X0] :
( ~ genls(c_tptpcol_7_113665,X0)
| disjointwith(X0,c_tptpcol_14_118118) ),
inference(resolution,[],[f41394,f25010]) ).
fof(f41421,plain,
disjointwith(c_tptpcol_6_112641,c_tptpcol_14_118118),
inference(resolution,[],[f41396,f16749]) ).
fof(f41423,plain,
! [X0] :
( ~ genls(c_tptpcol_6_112641,X0)
| disjointwith(X0,c_tptpcol_14_118118) ),
inference(resolution,[],[f41421,f25010]) ).
fof(f41481,plain,
disjointwith(c_tptpcol_5_110593,c_tptpcol_14_118118),
inference(resolution,[],[f41423,f14789]) ).
fof(f42100,plain,
! [X0] :
( ~ genls(c_tptpcol_5_110593,X0)
| disjointwith(X0,c_tptpcol_14_118118) ),
inference(resolution,[],[f41481,f25010]) ).
fof(f42150,plain,
disjointwith(c_tptpcol_4_106497,c_tptpcol_14_118118),
inference(resolution,[],[f42100,f17487]) ).
fof(f42152,plain,
! [X0] :
( ~ genls(c_tptpcol_4_106497,X0)
| disjointwith(X0,c_tptpcol_14_118118) ),
inference(resolution,[],[f42150,f25010]) ).
fof(f42212,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_14_118118),
inference(resolution,[],[f42152,f15831]) ).
fof(f42215,plain,
! [X0] :
( ~ genls(c_tptpcol_14_118118,X0)
| disjointwith(c_tptpcol_3_98305,X0) ),
inference(resolution,[],[f42212,f25009]) ).
fof(f42296,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_13_118117),
inference(resolution,[],[f42215,f13828]) ).
fof(f42299,plain,
! [X0] :
( ~ genls(c_tptpcol_13_118117,X0)
| disjointwith(c_tptpcol_3_98305,X0) ),
inference(resolution,[],[f42296,f25009]) ).
fof(f42396,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_12_118116),
inference(resolution,[],[f42299,f16787]) ).
fof(f42399,plain,
! [X0] :
( ~ genls(c_tptpcol_12_118116,X0)
| disjointwith(c_tptpcol_3_98305,X0) ),
inference(resolution,[],[f42396,f25009]) ).
fof(f42537,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_11_118084),
inference(resolution,[],[f42399,f15276]) ).
fof(f42540,plain,
! [X0] :
( ~ genls(c_tptpcol_11_118084,X0)
| disjointwith(c_tptpcol_3_98305,X0) ),
inference(resolution,[],[f42537,f25009]) ).
fof(f42760,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_10_118020),
inference(resolution,[],[f42540,f15871]) ).
fof(f42763,plain,
! [X0] :
( ~ genls(c_tptpcol_10_118020,X0)
| disjointwith(c_tptpcol_3_98305,X0) ),
inference(resolution,[],[f42760,f25009]) ).
fof(f43437,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_9_118019),
inference(resolution,[],[f42763,f14794]) ).
fof(f43440,plain,
! [X0] :
( ~ genls(c_tptpcol_9_118019,X0)
| disjointwith(c_tptpcol_3_98305,X0) ),
inference(resolution,[],[f43437,f25009]) ).
fof(f43579,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_8_117763),
inference(resolution,[],[f43440,f14358]) ).
fof(f43583,plain,
! [X0] :
( ~ genls(c_tptpcol_8_117763,X0)
| disjointwith(c_tptpcol_3_98305,X0) ),
inference(resolution,[],[f43579,f25009]) ).
fof(f43736,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_7_117762),
inference(resolution,[],[f43583,f14104]) ).
fof(f43739,plain,
! [X0] :
( ~ genls(c_tptpcol_7_117762,X0)
| disjointwith(c_tptpcol_3_98305,X0) ),
inference(resolution,[],[f43736,f25009]) ).
fof(f43878,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_6_116738),
inference(resolution,[],[f43739,f14348]) ).
fof(f43881,plain,
! [X0] :
( ~ genls(c_tptpcol_6_116738,X0)
| disjointwith(c_tptpcol_3_98305,X0) ),
inference(resolution,[],[f43878,f25009]) ).
fof(f44020,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_5_114690),
inference(resolution,[],[f43881,f15698]) ).
fof(f44023,plain,
! [X0] :
( ~ genls(c_tptpcol_5_114690,X0)
| disjointwith(c_tptpcol_3_98305,X0) ),
inference(resolution,[],[f44020,f25009]) ).
fof(f44194,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_4_114689),
inference(resolution,[],[f44023,f14201]) ).
fof(f44197,plain,
! [X0] :
( ~ genls(c_tptpcol_4_114689,X0)
| disjointwith(c_tptpcol_3_98305,X0) ),
inference(resolution,[],[f44194,f25009]) ).
fof(f44435,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(resolution,[],[f44197,f14696]) ).
fof(f44437,plain,
$false,
inference(forward_subsumption_resolution,[],[f44435,f22272]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR061+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.23 % Computer : n013.cluster.edu
% 0.11/0.23 % Model : x86_64 x86_64
% 0.11/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.23 % Memory : 8046.5625MB
% 0.11/0.23 % OS : Linux 6.8.0-71-generic
% 0.11/0.23 % CPULimit : 300
% 0.11/0.23 % WCLimit : 300
% 0.11/0.23 % DateTime : Mon Sep 28 22:21:22 UTC 2026
% 0.11/0.24 % CPUTime :
% 0.11/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.24/0.28 Running first-order model finding
% 0.24/0.28 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
% 1.65/0.74 % (1651886)Will run a generic schedule for satisfiability detection.
% 1.65/0.74 % (1651894)% WARNING: option uhcvi not known.
% 1.65/0.74 % (1651894)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3206885645:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 1.65/0.74 % (1651893)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3592286036_2998 on theBenchmark for (2998ds/0Mi)
% 1.65/0.74 % (1651895)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2785201676:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 1.65/0.74 % (1651896)dis+10_1_sil=32000:sp=arity:random_seed=3808512396:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 1.65/0.74 % (1651897)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2626058478:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 1.65/0.74 % (1651898)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2545690337:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 1.65/0.74 % (1651899)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3058427408:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 1.65/0.74 % (1651896)Instruction limit reached!
% 1.65/0.74 % (1651896)------------------------------
% 1.65/0.74 % (1651896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.74 % (1651896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.74 % (1651896)CaDiCaL version: 2.1.3
% 1.65/0.74 % (1651896)Termination reason: Instruction limit
% 1.65/0.74 % (1651896)Termination phase: Saturation
% 1.65/0.74 % (1651896)Time elapsed: 0.059 s
% 1.65/0.74 % (1651896)Peak memory usage: 22 MB
% 1.65/0.74 % (1651896)Instructions burned: 103 (million)
% 1.65/0.74 % (1651897)Instruction limit reached!
% 1.65/0.74 % (1651897)------------------------------
% 1.65/0.74 % (1651897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.74 % (1651897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.74 % (1651897)CaDiCaL version: 2.1.3
% 1.65/0.74 % (1651897)Termination reason: Instruction limit
% 1.65/0.74 % (1651897)Termination phase: Blocked clause elimination
% 1.65/0.74 % (1651897)Time elapsed: 0.078 s
% 1.65/0.74 % (1651897)Peak memory usage: 24 MB
% 1.65/0.74 % (1651897)Instructions burned: 116 (million)
% 1.65/0.74 % (1651907)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1161753812:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 1.65/0.74 % (1651898)Instruction limit reached!
% 1.65/0.74 % (1651898)------------------------------
% 1.65/0.74 % (1651898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.74 % (1651898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.74 % (1651898)CaDiCaL version: 2.1.3
% 1.65/0.74 % (1651898)Termination reason: Instruction limit
% 1.65/0.74 % (1651898)Termination phase: Saturation
% 1.65/0.74 % (1651898)Time elapsed: 0.100 s
% 1.65/0.74 % (1651898)Peak memory usage: 23 MB
% 1.65/0.74 % (1651898)Instructions burned: 132 (million)
% 1.65/0.74 % (1651899)Instruction limit reached!
% 1.65/0.74 % (1651899)------------------------------
% 1.65/0.74 % (1651899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.74 % (1651899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.74 % (1651899)CaDiCaL version: 2.1.3
% 1.65/0.74 % (1651899)Termination reason: Instruction limit
% 1.65/0.74 % (1651899)Termination phase: Saturation
% 1.65/0.74 % (1651899)Time elapsed: 0.105 s
% 1.65/0.74 % (1651899)Peak memory usage: 25 MB
% 1.65/0.74 % (1651899)Instructions burned: 159 (million)
% 1.65/0.74 % (1651908)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3227421776:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 1.65/0.74 % (1651910)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=2565721378:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 1.65/0.74 % (1651911)ott-21_1_sil=16000:fs=off:random_seed=2159464286:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 1.65/0.74 % (1651908)Instruction limit reached!
% 1.65/0.74 % (1651908)------------------------------
% 1.65/0.74 % (1651908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.74 % (1651908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.74 % (1651908)CaDiCaL version: 2.1.3
% 1.65/0.74 % (1651908)Termination reason: Instruction limit
% 1.65/0.74 % (1651908)Termination phase: Blocked clause elimination
% 1.65/0.74 % (1651908)Time elapsed: 0.081 s
% 1.65/0.74 % (1651908)Peak memory usage: 24 MB
% 1.65/0.74 % (1651908)Instructions burned: 132 (million)
% 1.65/0.74 % (1651916)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3790915225:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 1.65/0.74 % (1651911)Instruction limit reached!
% 1.65/0.74 % (1651911)------------------------------
% 1.65/0.74 % (1651911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.74 % (1651911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.74 % (1651911)CaDiCaL version: 2.1.3
% 1.65/0.74 % (1651911)Termination reason: Instruction limit
% 1.65/0.74 % (1651911)Termination phase: Saturation
% 1.65/0.74 % (1651911)Time elapsed: 0.098 s
% 1.65/0.74 % (1651911)Peak memory usage: 24 MB
% 1.65/0.74 % (1651911)Instructions burned: 181 (million)
% 1.65/0.74 % TRYING [1]
% 1.65/0.74 % (1651918)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4102785475:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 1.65/0.74 % (1651894) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1651886-1651894"...
% 1.65/0.74 % TRYING [2]
% 1.65/0.74 % (1651894)...printing done.
% 1.65/0.74 % (1651894)Refutation found. Thanks to Tanya!
% 1.65/0.74 % SZS status Theorem for theBenchmark
% 1.65/0.74 % SZS output start Proof for theBenchmark
% See solution above
% 1.65/0.76 % (1651894)------------------------------
% 1.65/0.76 % (1651894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.65/0.76 % (1651894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.65/0.76 % (1651894)CaDiCaL version: 2.1.3
% 1.65/0.76 % (1651894)Termination reason: Refutation
% 1.65/0.76 % (1651894)Time elapsed: 0.261 s
% 1.65/0.76 % (1651894)Peak memory usage: 36 MB
% 1.65/0.76 % (1651894)Instructions burned: 872 (million)
% 1.65/0.76 % (1651886)Success in time 0.455 s
% 1.65/0.76 % Vampire exiting
%------------------------------------------------------------------------------