%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP504-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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 10:17:59 AM UTC 2026
% Result : Unsatisfiable 13.15s 7.46s
% Output : Refutation 13.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 3
% Syntax : Number of formulae : 56 ( 56 unt; 0 def)
% Number of atoms : 56 ( 55 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 11 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 200 ( 200 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] : double_divide(double_divide(X0,inverse(double_divide(X1,X2))),double_divide(inverse(X1),inverse(double_divide(X3,double_divide(X0,X3))))) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,axiom,
! [X0,X1] : multiply(X0,X1) = inverse(double_divide(X1,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiply) ).
fof(f3,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_3) ).
fof(f4,plain,
inverse(double_divide(c3,inverse(double_divide(b3,a3)))) != inverse(double_divide(inverse(double_divide(c3,b3)),a3)),
inference(definition_unfolding,[],[f3,f2,f2,f2,f2]) ).
fof(f5,plain,
! [X2,X3,X0,X1,X4,X5] : double_divide(inverse(X3),inverse(double_divide(X4,double_divide(X2,X4)))) = double_divide(double_divide(X1,inverse(X0)),double_divide(inverse(double_divide(X2,inverse(double_divide(X3,X0)))),inverse(double_divide(X5,double_divide(X1,X5))))),
inference(superposition,[],[f1,f1]) ).
fof(f6,plain,
! [X2,X3,X0,X1,X4,X5] : double_divide(double_divide(double_divide(X1,inverse(double_divide(X2,X0))),inverse(double_divide(X3,X4))),double_divide(inverse(X3),inverse(double_divide(double_divide(inverse(X2),inverse(double_divide(X5,double_divide(X1,X5)))),X0)))) = X4,
inference(superposition,[],[f1,f1]) ).
fof(f20,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X0),inverse(double_divide(X1,double_divide(X2,X1)))) = double_divide(inverse(X0),inverse(double_divide(X3,double_divide(X2,X3)))),
inference(superposition,[],[f5,f5]) ).
fof(f60,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(double_divide(X4,double_divide(X2,X4))) = double_divide(double_divide(X3,inverse(double_divide(inverse(X0),inverse(double_divide(X1,double_divide(X2,X1)))))),double_divide(inverse(inverse(X0)),inverse(double_divide(X5,double_divide(X3,X5))))),
inference(superposition,[],[f1,f20]) ).
fof(f65,plain,
! [X2,X1,X4] : inverse(double_divide(X1,double_divide(X2,X1))) = inverse(double_divide(X4,double_divide(X2,X4))),
inference(forward_demodulation,[],[f60,f1]) ).
fof(f87,plain,
! [X2,X3,X0,X1,X4] : double_divide(X1,X3) = double_divide(double_divide(X2,inverse(double_divide(X0,double_divide(X1,X0)))),double_divide(inverse(X3),inverse(double_divide(X4,double_divide(X2,X4))))),
inference(superposition,[],[f1,f65]) ).
fof(f115,plain,
! [X2,X3,X0,X1,X6,X4,X5] : double_divide(X2,double_divide(X3,double_divide(X1,X3))) = double_divide(double_divide(X4,inverse(double_divide(X5,double_divide(X2,X5)))),double_divide(inverse(double_divide(X0,double_divide(X1,X0))),inverse(double_divide(X6,double_divide(X4,X6))))),
inference(superposition,[],[f87,f65]) ).
fof(f127,plain,
! [X2,X3,X0,X1,X4] : double_divide(inverse(X0),inverse(double_divide(X1,double_divide(X2,X1)))) = double_divide(X3,double_divide(X2,inverse(double_divide(X0,double_divide(X4,double_divide(X3,X4)))))),
inference(superposition,[],[f87,f5]) ).
fof(f138,plain,
! [X2,X3,X0,X1] : double_divide(X2,double_divide(X3,double_divide(X1,X3))) = double_divide(X2,double_divide(X0,double_divide(X1,X0))),
inference(forward_demodulation,[],[f115,f87]) ).
fof(f193,plain,
! [X2,X3,X0,X1,X4,X5] : double_divide(X4,double_divide(X2,X4)) = double_divide(double_divide(X3,inverse(double_divide(X0,double_divide(X1,double_divide(X2,X1))))),double_divide(inverse(X0),inverse(double_divide(X5,double_divide(X3,X5))))),
inference(superposition,[],[f1,f138]) ).
fof(f205,plain,
! [X2,X1,X4] : double_divide(X1,double_divide(X2,X1)) = double_divide(X4,double_divide(X2,X4)),
inference(forward_demodulation,[],[f193,f1]) ).
fof(f2673,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(double_divide(X1,inverse(double_divide(X2,X0))),X1)),inverse(double_divide(X3,double_divide(inverse(X2),X3)))) = X0,
inference(superposition,[],[f127,f1]) ).
fof(f2942,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(inverse(X1),inverse(double_divide(double_divide(double_divide(X2,inverse(double_divide(X1,X0))),X2),X3))),X0) = X3,
inference(superposition,[],[f1,f2673]) ).
fof(f3126,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X0),inverse(double_divide(X3,double_divide(inverse(double_divide(double_divide(X2,inverse(double_divide(X1,inverse(X1)))),X2)),X3)))) = X0,
inference(superposition,[],[f2673,f2942]) ).
fof(f3395,plain,
! [X2,X0,X1] : double_divide(inverse(X1),inverse(double_divide(inverse(double_divide(X2,double_divide(inverse(X0),X2))),inverse(X0)))) = X1,
inference(superposition,[],[f3126,f2673]) ).
fof(f3437,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X1,inverse(double_divide(double_divide(double_divide(X2,inverse(double_divide(X3,inverse(X3)))),X2),X0))),X1) = X0,
inference(superposition,[],[f3126,f2673]) ).
fof(f3551,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X2),inverse(double_divide(inverse(double_divide(double_divide(X1,inverse(X3)),double_divide(X0,double_divide(X1,X0)))),inverse(X3)))) = X2,
inference(superposition,[],[f3395,f205]) ).
fof(f3688,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X2,inverse(double_divide(inverse(double_divide(double_divide(X0,inverse(double_divide(X1,inverse(X1)))),X0)),X3))),X2) = X3,
inference(superposition,[],[f3437,f2942]) ).
fof(f3845,plain,
! [X3,X0,X1] : inverse(double_divide(X3,double_divide(inverse(X0),X3))) = double_divide(double_divide(X1,inverse(inverse(X0))),X1),
inference(superposition,[],[f3688,f2673]) ).
fof(f4037,plain,
! [X2,X3,X0,X1] : double_divide(inverse(double_divide(double_divide(X2,inverse(double_divide(X1,X3))),X2)),double_divide(double_divide(X0,inverse(inverse(X1))),X0)) = X3,
inference(superposition,[],[f2673,f3845]) ).
fof(f7564,plain,
! [X2,X3,X0,X1,X4,X5] : double_divide(inverse(X1),inverse(double_divide(inverse(double_divide(X0,double_divide(X5,double_divide(inverse(X0),X5)))),inverse(double_divide(inverse(double_divide(double_divide(X2,inverse(X3)),double_divide(X4,double_divide(X2,X4)))),inverse(X3)))))) = X1,
inference(superposition,[],[f3551,f3551]) ).
fof(f7780,plain,
! [X0,X1,X5] : double_divide(inverse(X1),inverse(double_divide(X0,double_divide(X5,double_divide(inverse(X0),X5))))) = X1,
inference(forward_demodulation,[],[f7564,f3551]) ).
fof(f7890,plain,
! [X2,X0,X1] : double_divide(inverse(X1),X0) = double_divide(inverse(X1),inverse(double_divide(X2,double_divide(inverse(X0),X2)))),
inference(superposition,[],[f127,f7780]) ).
fof(f8175,plain,
! [X2,X3,X0,X1,X4] : inverse(double_divide(X3,double_divide(inverse(X1),X3))) = double_divide(inverse(double_divide(double_divide(X2,inverse(double_divide(inverse(X0),X1))),X2)),double_divide(double_divide(X4,inverse(inverse(inverse(X0)))),X4)),
inference(superposition,[],[f4037,f7890]) ).
fof(f8178,plain,
! [X3,X1] : inverse(double_divide(X3,double_divide(inverse(X1),X3))) = X1,
inference(forward_demodulation,[],[f8175,f4037]) ).
fof(f8282,plain,
! [X0,X1] : double_divide(inverse(X1),inverse(double_divide(X0,inverse(X0)))) = X1,
inference(superposition,[],[f3395,f8178]) ).
fof(f8662,plain,
! [X2,X0,X1] : double_divide(inverse(X1),inverse(double_divide(X2,double_divide(inverse(double_divide(X0,inverse(X0))),X2)))) = X1,
inference(superposition,[],[f3126,f8282]) ).
fof(f8667,plain,
! [X2,X0,X1] : inverse(X1) = double_divide(inverse(double_divide(X0,inverse(X0))),inverse(double_divide(X2,double_divide(inverse(X1),X2)))),
inference(superposition,[],[f2673,f8282]) ).
fof(f8669,plain,
! [X2,X0,X1] : inverse(X1) = double_divide(X0,double_divide(inverse(X1),inverse(double_divide(X2,double_divide(inverse(X0),X2))))),
inference(superposition,[],[f1,f8282]) ).
fof(f8749,plain,
! [X0,X1] : inverse(X1) = double_divide(X0,double_divide(inverse(X1),X0)),
inference(forward_demodulation,[],[f8669,f7890]) ).
fof(f8751,plain,
! [X0,X1] : inverse(X1) = double_divide(inverse(double_divide(X0,inverse(X0))),X1),
inference(forward_demodulation,[],[f8667,f7890]) ).
fof(f8753,plain,
! [X0,X1] : double_divide(inverse(X1),double_divide(X0,inverse(X0))) = X1,
inference(forward_demodulation,[],[f8662,f7890]) ).
fof(f8785,plain,
! [X2,X0] : double_divide(X2,double_divide(X0,X2)) = X0,
inference(superposition,[],[f8749,f8178]) ).
fof(f8851,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(superposition,[],[f8178,f8749]) ).
fof(f10212,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(inverse(X0),X1)) = double_divide(X0,double_divide(X2,inverse(X2))),
inference(superposition,[],[f8753,f8178]) ).
fof(f10535,plain,
! [X2,X0] : inverse(X0) = double_divide(X0,double_divide(X2,inverse(X2))),
inference(forward_demodulation,[],[f10212,f8749]) ).
fof(f18870,plain,
! [X2,X3,X0,X1,X4] : double_divide(double_divide(double_divide(X1,inverse(double_divide(X2,X0))),inverse(double_divide(X3,X4))),double_divide(inverse(X3),inverse(double_divide(double_divide(inverse(X2),inverse(X1)),X0)))) = X4,
inference(forward_demodulation,[],[f6,f8785]) ).
fof(f19453,plain,
! [X2,X3,X0,X1,X4] : double_divide(inverse(X1),inverse(double_divide(X2,double_divide(X3,X2)))) = double_divide(inverse(double_divide(X4,inverse(X4))),double_divide(X3,inverse(double_divide(X1,double_divide(X0,inverse(X0)))))),
inference(superposition,[],[f127,f8751]) ).
fof(f19797,plain,
! [X2,X3,X0,X1] : double_divide(inverse(X1),inverse(double_divide(X2,double_divide(X3,X2)))) = inverse(double_divide(X3,inverse(double_divide(X1,double_divide(X0,inverse(X0)))))),
inference(forward_demodulation,[],[f19453,f8751]) ).
fof(f20032,plain,
! [X2,X3,X1] : double_divide(inverse(X1),inverse(double_divide(X2,double_divide(X3,X2)))) = inverse(double_divide(X3,inverse(inverse(X1)))),
inference(forward_demodulation,[],[f19797,f10535]) ).
fof(f20186,plain,
! [X2,X3,X1] : inverse(double_divide(X3,X1)) = double_divide(inverse(X1),inverse(double_divide(X2,double_divide(X3,X2)))),
inference(forward_demodulation,[],[f20032,f8851]) ).
fof(f20257,plain,
! [X3,X1] : inverse(double_divide(X3,X1)) = double_divide(inverse(X1),inverse(X3)),
inference(forward_demodulation,[],[f20186,f8785]) ).
fof(f31308,plain,
! [X2,X3,X0,X1,X4] : double_divide(double_divide(double_divide(X1,inverse(double_divide(X2,X0))),inverse(double_divide(X3,X4))),inverse(double_divide(double_divide(double_divide(inverse(X2),inverse(X1)),X0),X3))) = X4,
inference(forward_demodulation,[],[f18870,f20257]) ).
fof(f31309,plain,
! [X2,X3,X0,X1,X4] : double_divide(double_divide(double_divide(X1,inverse(double_divide(X2,X0))),inverse(double_divide(X3,X4))),inverse(double_divide(double_divide(inverse(double_divide(X1,X2)),X0),X3))) = X4,
inference(forward_demodulation,[],[f31308,f20257]) ).
fof(f32301,plain,
! [X2,X3,X0,X1,X4] : double_divide(X0,inverse(double_divide(double_divide(inverse(double_divide(double_divide(X1,inverse(double_divide(X2,X3))),X4)),X0),double_divide(inverse(double_divide(X1,X2)),X3)))) = X4,
inference(superposition,[],[f31309,f31309]) ).
fof(f35040,plain,
! [X2,X3,X0,X1,X4,X5] : double_divide(inverse(double_divide(X2,X3)),X4) = double_divide(X0,double_divide(inverse(double_divide(inverse(double_divide(double_divide(X2,inverse(double_divide(X3,X4))),X0)),X1)),inverse(double_divide(X5,double_divide(X1,X5))))),
inference(superposition,[],[f1,f32301]) ).
fof(f35264,plain,
! [X2,X3,X0,X1,X4,X5] : double_divide(inverse(double_divide(X2,X3)),X4) = double_divide(X0,inverse(double_divide(double_divide(X5,double_divide(X1,X5)),double_divide(inverse(double_divide(double_divide(X2,inverse(double_divide(X3,X4))),X0)),X1)))),
inference(forward_demodulation,[],[f35040,f20257]) ).
fof(f35810,plain,
! [X2,X3,X0,X1,X4] : double_divide(inverse(double_divide(X2,X3)),X4) = double_divide(X0,inverse(double_divide(X1,double_divide(inverse(double_divide(double_divide(X2,inverse(double_divide(X3,X4))),X0)),X1)))),
inference(forward_demodulation,[],[f35264,f8785]) ).
fof(f36245,plain,
! [X2,X3,X0,X4] : double_divide(inverse(double_divide(X2,X3)),X4) = double_divide(X0,double_divide(double_divide(X2,inverse(double_divide(X3,X4))),X0)),
inference(forward_demodulation,[],[f35810,f8178]) ).
fof(f36557,plain,
! [X2,X3,X4] : double_divide(X2,inverse(double_divide(X3,X4))) = double_divide(inverse(double_divide(X2,X3)),X4),
inference(forward_demodulation,[],[f36245,f8785]) ).
fof(f44423,plain,
inverse(double_divide(c3,inverse(double_divide(b3,a3)))) != inverse(double_divide(c3,inverse(double_divide(b3,a3)))),
inference(superposition,[],[f4,f36557]) ).
fof(f44643,plain,
$false,
inference(trivial_inequality_removal,[],[f44423]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP504-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/5.40 % Computer : n008.cluster.edu
% 0.14/5.40 % Model : x86_64 x86_64
% 0.14/5.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.40 % Memory : 8046.5625MB
% 0.14/5.40 % OS : Linux 6.8.0-71-generic
% 0.14/5.40 % CPULimit : 300
% 0.14/5.40 % WCLimit : 300
% 0.14/5.40 % DateTime : Sun Sep 27 10:07:00 UTC 2026
% 0.14/5.40 % CPUTime :
% 0.14/5.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/5.45 Running first-order model finding
% 0.14/5.45 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
% 13.15/7.46 % (999165)Will run a generic schedule for satisfiability detection.
% 13.15/7.46 % (999174)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1517678043:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 13.15/7.46 % (999171)% WARNING: option uhcvi not known.
% 13.15/7.46 % (999170)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3642590735_3000 on theBenchmark for (3000ds/0Mi)
% 13.15/7.46 % (999175)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1782123208:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 13.15/7.46 % (999171)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2990529705:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 13.15/7.46 % (999172)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2509596064:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 13.15/7.46 % (999173)dis+10_1_sil=32000:sp=arity:random_seed=1749195216:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 13.15/7.46 % (999176)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3692997672:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 13.15/7.46 % TRYING [1]
% 13.15/7.46 % TRYING [2]
% 13.15/7.46 % TRYING [3]
% 13.15/7.46 % (999174)Instruction limit reached!
% 13.15/7.46 % (999174)------------------------------
% 13.15/7.46 % (999174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999174)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999174)Termination reason: Instruction limit
% 13.15/7.46 % (999174)Termination phase: Saturation
% 13.15/7.46 % (999174)Time elapsed: 0.047 s
% 13.15/7.46 % (999174)Peak memory usage: 12 MB
% 13.15/7.46 % (999174)Instructions burned: 116 (million)
% 13.15/7.46 % TRYING [4]
% 13.15/7.46 % (999184)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=333926989:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.15/7.46 % TRYING [1]
% 13.15/7.46 % TRYING [2]
% 13.15/7.46 % TRYING [3]
% 13.15/7.46 % TRYING [4]
% 13.15/7.46 % (999173)Instruction limit reached!
% 13.15/7.46 % (999173)------------------------------
% 13.15/7.46 % (999173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999173)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999173)Termination reason: Instruction limit
% 13.15/7.46 % (999173)Termination phase: Saturation
% 13.15/7.46 % (999173)Time elapsed: 0.092 s
% 13.15/7.46 % (999173)Peak memory usage: 12 MB
% 13.15/7.46 % (999173)Instructions burned: 103 (million)
% 13.15/7.46 % (999186)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1327511557:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 13.15/7.46 % (999175)Instruction limit reached!
% 13.15/7.46 % (999175)------------------------------
% 13.15/7.46 % (999175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999175)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999175)Termination reason: Instruction limit
% 13.15/7.46 % (999175)Termination phase: Saturation
% 13.15/7.46 % (999175)Time elapsed: 0.125 s
% 13.15/7.46 % (999175)Peak memory usage: 13 MB
% 13.15/7.46 % (999175)Instructions burned: 132 (million)
% 13.15/7.46 % (999189)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=819672472:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.15/7.46 % (999176)Instruction limit reached!
% 13.15/7.46 % (999176)------------------------------
% 13.15/7.46 % (999176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999176)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999176)Termination reason: Instruction limit
% 13.15/7.46 % (999176)Termination phase: Saturation
% 13.15/7.46 % (999176)Time elapsed: 0.157 s
% 13.15/7.46 % (999176)Peak memory usage: 12 MB
% 13.15/7.46 % (999176)Instructions burned: 159 (million)
% 13.15/7.46 % (999191)ott-21_1_sil=16000:fs=off:random_seed=1828208905:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.15/7.46 % (999186)Instruction limit reached!
% 13.15/7.46 % (999186)------------------------------
% 13.15/7.46 % (999186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999186)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999186)Termination reason: Instruction limit
% 13.15/7.46 % (999186)Termination phase: Saturation
% 13.15/7.46 % (999186)Time elapsed: 0.129 s
% 13.15/7.46 % (999186)Peak memory usage: 13 MB
% 13.15/7.46 % (999186)Instructions burned: 131 (million)
% 13.15/7.46 % (999193)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1640702413:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 13.15/7.46 % (999191)Instruction limit reached!
% 13.15/7.46 % (999191)------------------------------
% 13.15/7.46 % (999191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999191)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999191)Termination reason: Instruction limit
% 13.15/7.46 % (999191)Termination phase: Saturation
% 13.15/7.46 % (999191)Time elapsed: 0.107 s
% 13.15/7.46 % (999191)Peak memory usage: 12 MB
% 13.15/7.46 % (999191)Instructions burned: 181 (million)
% 13.15/7.46 % (999195)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3762933908:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 13.15/7.46 % TRYING [1]
% 13.15/7.46 % TRYING [2]
% 13.15/7.46 % TRYING [3]
% 13.15/7.46 % TRYING [4]
% 13.15/7.46 % (999184)Instruction limit reached!
% 13.15/7.46 % (999184)------------------------------
% 13.15/7.46 % (999184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999184)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999184)Termination reason: Instruction limit
% 13.15/7.46 % (999184)Termination phase: Finite model building SAT solving
% 13.15/7.46 % (999184)Time elapsed: 0.365 s
% 13.15/7.46 % (999184)Peak memory usage: 13 MB
% 13.15/7.46 % (999184)Instructions burned: 716 (million)
% 13.15/7.46 % (999197)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1576835750:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 13.15/7.46 % (999193)Instruction limit reached!
% 13.15/7.46 % (999193)------------------------------
% 13.15/7.46 % (999193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999193)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999193)Termination reason: Instruction limit
% 13.15/7.46 % (999193)Termination phase: Saturation
% 13.15/7.46 % (999193)Time elapsed: 0.410 s
% 13.15/7.46 % (999193)Peak memory usage: 16 MB
% 13.15/7.46 % (999193)Instructions burned: 477 (million)
% 13.15/7.46 % (999199)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2660232223:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 13.15/7.46 % (999189)Instruction limit reached!
% 13.15/7.46 % (999189)------------------------------
% 13.15/7.46 % (999189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999189)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999189)Termination reason: Instruction limit
% 13.15/7.46 % (999189)Termination phase: Saturation
% 13.15/7.46 % (999189)Time elapsed: 0.585 s
% 13.15/7.46 % (999189)Peak memory usage: 17 MB
% 13.15/7.46 % (999189)Instructions burned: 684 (million)
% 13.15/7.46 % (999201)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=4195706509:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 13.15/7.46 % TRYING [14]
% 13.15/7.46 % (999195)Instruction limit reached!
% 13.15/7.46 % (999195)------------------------------
% 13.15/7.46 % (999195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999195)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999195)Termination reason: Instruction limit
% 13.15/7.46 % (999195)Termination phase: Finite model building SAT solving
% 13.15/7.46 % (999195)Time elapsed: 0.485 s
% 13.15/7.46 % (999195)Peak memory usage: 11 MB
% 13.15/7.46 % (999195)Instructions burned: 865 (million)
% 13.15/7.46 % (999203)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2796563531:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 13.15/7.46 % (999201)Instruction limit reached!
% 13.15/7.46 % (999201)------------------------------
% 13.15/7.46 % (999201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999201)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999201)Termination reason: Instruction limit
% 13.15/7.46 % (999201)Termination phase: Saturation
% 13.15/7.46 % (999201)Time elapsed: 0.495 s
% 13.15/7.46 % (999201)Peak memory usage: 18 MB
% 13.15/7.46 % (999201)Instructions burned: 692 (million)
% 13.15/7.46 % (999206)fmb+10_1_sil=64000:random_seed=800555346:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi)
% 13.15/7.46 % TRYING [1]
% 13.15/7.46 % TRYING [2]
% 13.15/7.46 % TRYING [3]
% 13.15/7.46 % TRYING [4]
% 13.15/7.46 % (999199)Instruction limit reached!
% 13.15/7.46 % (999199)------------------------------
% 13.15/7.46 % (999199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999199)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999199)Termination reason: Instruction limit
% 13.15/7.46 % (999199)Termination phase: Finite model building constraint generation
% 13.15/7.46 % (999199)Time elapsed: 0.679 s
% 13.15/7.46 % (999199)Peak memory usage: 79 MB
% 13.15/7.46 % (999199)Instructions burned: 890 (million)
% 13.15/7.46 % (999208)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1606101494:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi)
% 13.15/7.46 % TRYING [20]
% 13.15/7.46 % (999197)Instruction limit reached!
% 13.15/7.46 % (999197)------------------------------
% 13.15/7.46 % (999197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999197)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999197)Termination reason: Instruction limit
% 13.15/7.46 % (999197)Termination phase: Saturation
% 13.15/7.46 % (999197)Time elapsed: 1.069 s
% 13.15/7.46 % (999197)Peak memory usage: 22 MB
% 13.15/7.46 % (999197)Instructions burned: 1179 (million)
% 13.15/7.46 % (999210)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3659244162:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 13.15/7.46 % TRYING [8]
% 13.15/7.46 % TRYING [5]
% 13.15/7.46 % (999203)Instruction limit reached!
% 13.15/7.46 % (999203)------------------------------
% 13.15/7.46 % (999203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999203)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999203)Termination reason: Instruction limit
% 13.15/7.46 % (999203)Termination phase: Saturation
% 13.15/7.46 % (999203)Time elapsed: 0.801 s
% 13.15/7.46 % (999203)Peak memory usage: 18 MB
% 13.15/7.46 % (999203)Instructions burned: 879 (million)
% 13.15/7.46 % (999212)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2342666466:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 13.15/7.46 % (999172) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-999165-999172"...
% 13.15/7.46 % (999172)...printing done.
% 13.15/7.46 % (999172)Refutation found. Thanks to Tanya!
% 13.15/7.46 % SZS status Unsatisfiable for theBenchmark
% 13.15/7.46 % SZS output start Proof for theBenchmark
% See solution above
% 13.15/7.46 % (999172)------------------------------
% 13.15/7.46 % (999172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.15/7.46 % (999172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/7.46 % (999172)CaDiCaL version: 2.1.3
% 13.15/7.46 % (999172)Termination reason: Refutation
% 13.15/7.46 % (999172)Time elapsed: 1.947 s
% 13.15/7.46 % (999172)Peak memory usage: 29 MB
% 13.15/7.46 % (999172)Instructions burned: 2426 (million)
% 13.15/7.46 % (999165)Success in time 2.002 s
% 13.15/7.46 % Vampire exiting
%------------------------------------------------------------------------------