%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT084-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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 11:47:49 AM UTC 2026
% Result : Unsatisfiable 79.12s 11.66s
% Output : Refutation 79.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 2
% Syntax : Number of formulae : 61 ( 61 unt; 0 def)
% Number of atoms : 61 ( 60 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 18 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 176 ( 176 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1,X6,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X3,X1),meet(X1,X4)),X1)),meet(join(meet(X1,meet(meet(join(X3,join(X1,X4)),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X3,join(X1,X4)),join(X5,X1)),X1)))),join(X0,join(join(meet(X3,X1),meet(X1,X4)),X1)))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
join(a,b) != join(b,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_normal_axioms_5) ).
fof(f5,plain,
! [X2,X3,X0,X1,X4,X5] : join(meet(X2,X0),meet(X0,join(X2,X0))) = join(meet(join(meet(X1,join(meet(X2,X0),meet(X0,join(X2,X0)))),meet(join(meet(X2,X0),meet(X0,join(X2,X0))),join(X1,join(meet(X2,X0),meet(X0,join(X2,X0)))))),X3),meet(join(meet(X1,join(join(meet(X4,join(meet(X2,X0),meet(X0,join(X2,X0)))),meet(join(meet(X2,X0),meet(X0,join(X2,X0))),X5)),join(meet(X2,X0),meet(X0,join(X2,X0))))),meet(X0,join(X1,join(join(meet(X4,join(meet(X2,X0),meet(X0,join(X2,X0)))),meet(join(meet(X2,X0),meet(X0,join(X2,X0))),X5)),join(meet(X2,X0),meet(X0,join(X2,X0))))))),join(join(meet(X1,join(meet(X2,X0),meet(X0,join(X2,X0)))),meet(join(meet(X2,X0),meet(X0,join(X2,X0))),join(X1,join(meet(X2,X0),meet(X0,join(X2,X0)))))),X3))),
inference(superposition,[],[f1,f1]) ).
fof(f13,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : join(meet(join(meet(X6,X0),meet(X0,join(X6,X0))),X7),meet(join(meet(X6,join(join(meet(X8,X0),meet(X0,X9)),X0)),meet(join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(join(meet(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)),meet(X5,join(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)))),join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))),join(X6,join(join(meet(X8,X0),meet(X0,X9)),X0)))),join(join(meet(X6,X0),meet(X0,join(X6,X0))),X7))) = X0,
inference(superposition,[],[f5,f1]) ).
fof(f36,plain,
! [X2,X0,X1] : join(meet(join(meet(join(meet(X1,X0),meet(X0,join(X1,X0))),X0),meet(X0,join(join(meet(X1,X0),meet(X0,join(X1,X0))),X0))),X2),meet(X0,join(join(meet(join(meet(X1,X0),meet(X0,join(X1,X0))),X0),meet(X0,join(join(meet(X1,X0),meet(X0,join(X1,X0))),X0))),X2))) = X0,
inference(superposition,[],[f13,f1]) ).
fof(f60,plain,
! [X2,X0] : join(meet(X0,X2),meet(X0,join(X0,X2))) = X0,
inference(superposition,[],[f36,f36]) ).
fof(f64,plain,
! [X2,X3,X0,X4,X5] : join(meet(join(meet(X2,X0),meet(X0,join(X2,X0))),X3),meet(join(meet(X2,join(join(meet(X4,X0),meet(X0,X5)),X0)),meet(X0,join(X2,join(join(meet(X4,X0),meet(X0,X5)),X0)))),join(join(meet(X2,X0),meet(X0,join(X2,X0))),X3))) = X0,
inference(superposition,[],[f5,f36]) ).
fof(f86,plain,
! [X0,X1] : meet(X0,X1) = join(meet(meet(X0,X1),meet(X0,join(X0,X1))),meet(meet(X0,X1),X0)),
inference(superposition,[],[f60,f60]) ).
fof(f164,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(join(meet(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)),meet(X5,join(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)))),join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))) = join(meet(X0,X6),meet(join(meet(join(meet(X1,X0),meet(X0,join(X1,X0))),join(join(meet(X7,join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(join(meet(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)),meet(X5,join(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)))),join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0))))),meet(join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(join(meet(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)),meet(X5,join(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)))),join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))),X8)),join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(join(meet(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)),meet(X5,join(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)))),join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))))),meet(join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(join(meet(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)),meet(X5,join(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)))),join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))),join(join(meet(X1,X0),meet(X0,join(X1,X0))),join(join(meet(X7,join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(join(meet(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)),meet(X5,join(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)))),join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0))))),meet(join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(join(meet(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)),meet(X5,join(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)))),join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))),X8)),join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(join(meet(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)),meet(X5,join(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)))),join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))))))),join(X0,X6))),
inference(superposition,[],[f64,f1]) ).
fof(f166,plain,
! [X2,X3,X0,X1,X6,X4,X5] : join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))) = join(meet(X0,X4),meet(join(meet(join(meet(X1,X0),meet(X0,join(X1,X0))),join(join(meet(X5,join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0))))),meet(join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))),X6)),join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))))),meet(join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))),join(join(meet(X1,X0),meet(X0,join(X1,X0))),join(join(meet(X5,join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0))))),meet(join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))),X6)),join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))))))),join(X0,X4))),
inference(superposition,[],[f64,f64]) ).
fof(f194,plain,
! [X2,X3,X0,X1,X4] : join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))) = join(meet(X0,X4),meet(X0,join(X0,X4))),
inference(forward_demodulation,[],[f166,f64]) ).
fof(f196,plain,
! [X2,X3,X0,X1,X6,X4,X5] : join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(join(meet(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)),meet(X5,join(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)))),join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))) = join(meet(X0,X6),meet(X0,join(X0,X6))),
inference(forward_demodulation,[],[f164,f1]) ).
fof(f203,plain,
! [X2,X3,X0,X1] : join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(X0,join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))) = X0,
inference(forward_demodulation,[],[f194,f60]) ).
fof(f205,plain,
! [X2,X3,X0,X1,X4,X5] : join(meet(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)),meet(join(meet(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)),meet(X5,join(X0,meet(meet(join(X2,join(X0,X3)),join(X4,X0)),X0)))),join(X1,join(join(meet(X2,X0),meet(X0,X3)),X0)))) = X0,
inference(forward_demodulation,[],[f196,f60]) ).
fof(f214,plain,
! [X0,X1] : join(meet(X1,join(X0,X0)),meet(X0,join(X1,join(X0,X0)))) = X0,
inference(superposition,[],[f203,f36]) ).
fof(f655,plain,
! [X2,X3,X0,X1,X4] : join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)))) = X0,
inference(superposition,[],[f205,f36]) ).
fof(f748,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,join(X1,X0))) = X0,
inference(superposition,[],[f655,f1]) ).
fof(f859,plain,
! [X2,X3,X0,X1] : meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0) = X0,
inference(superposition,[],[f748,f655]) ).
fof(f1041,plain,
! [X0,X4] : join(meet(X0,X0),meet(X4,join(X0,X0))) = X0,
inference(superposition,[],[f655,f859]) ).
fof(f1050,plain,
! [X2,X3,X0,X1] : join(meet(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0)),join(X0,meet(meet(join(X1,join(X0,X2)),join(X3,X0)),X0))) = X0,
inference(superposition,[],[f655,f859]) ).
fof(f1133,plain,
! [X0] : join(meet(X0,X0),join(X0,X0)) = X0,
inference(forward_demodulation,[],[f1050,f859]) ).
fof(f1200,plain,
! [X0,X1] : meet(meet(X0,join(X1,X0)),X0) = X0,
inference(superposition,[],[f859,f1133]) ).
fof(f1433,plain,
! [X2,X0,X1] : join(join(meet(X1,X0),meet(X0,X2)),X0) = X0,
inference(superposition,[],[f1041,f203]) ).
fof(f1434,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f1041,f214]) ).
fof(f1593,plain,
! [X0] : join(meet(X0,X0),meet(X0,X0)) = X0,
inference(superposition,[],[f748,f1434]) ).
fof(f1594,plain,
! [X2,X0,X1] : meet(meet(join(X1,X0),join(X2,X0)),X0) = X0,
inference(superposition,[],[f859,f1434]) ).
fof(f1595,plain,
! [X2,X0,X1] : meet(meet(join(X1,join(X0,X2)),X0),X0) = X0,
inference(superposition,[],[f859,f1434]) ).
fof(f1669,plain,
! [X0] : meet(X0,X0) = X0,
inference(forward_demodulation,[],[f1593,f1434]) ).
fof(f1745,plain,
! [X0,X1] : join(X0,meet(X1,join(X0,X0))) = X0,
inference(superposition,[],[f1041,f1669]) ).
fof(f1846,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(forward_demodulation,[],[f1745,f1434]) ).
fof(f2300,plain,
! [X0,X4] : join(join(X0,meet(X0,X4)),X0) = X0,
inference(superposition,[],[f1433,f859]) ).
fof(f2318,plain,
! [X0,X1] : join(meet(X0,X1),X1) = X1,
inference(superposition,[],[f1433,f1846]) ).
fof(f2606,plain,
! [X0,X1] : meet(X1,X0) = join(meet(meet(X1,X0),X0),meet(meet(X1,X0),X0)),
inference(superposition,[],[f60,f2318]) ).
fof(f2674,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(forward_demodulation,[],[f2606,f1434]) ).
fof(f2800,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = join(meet(join(X0,meet(X0,X1)),X0),meet(join(X0,meet(X0,X1)),X0)),
inference(superposition,[],[f60,f2300]) ).
fof(f2868,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = meet(join(X0,meet(X0,X1)),X0),
inference(forward_demodulation,[],[f2800,f1434]) ).
fof(f3280,plain,
! [X0,X1] : meet(join(X0,X1),X1) = X1,
inference(superposition,[],[f1594,f1669]) ).
fof(f3554,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(superposition,[],[f3280,f1846]) ).
fof(f4079,plain,
! [X2,X0,X1] : meet(join(X1,join(X0,X2)),X0) = X0,
inference(forward_demodulation,[],[f1595,f2674]) ).
fof(f4096,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(join(X1,X0),meet(X0,X2)),
inference(superposition,[],[f4079,f60]) ).
fof(f4110,plain,
! [X0,X1] : meet(join(X0,X1),X0) = X0,
inference(superposition,[],[f4079,f1434]) ).
fof(f4337,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(superposition,[],[f4110,f60]) ).
fof(f4397,plain,
! [X2,X0,X1] : join(X0,X2) = join(join(meet(X1,join(X0,X2)),X0),join(X0,X2)),
inference(superposition,[],[f1433,f4110]) ).
fof(f8904,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
inference(forward_demodulation,[],[f2868,f4110]) ).
fof(f8923,plain,
! [X2,X0,X1] : join(X2,X0) = join(join(X2,X0),meet(X0,X1)),
inference(superposition,[],[f8904,f4096]) ).
fof(f8943,plain,
! [X0,X1] : join(meet(X0,meet(X0,X1)),meet(X0,X0)) = X0,
inference(superposition,[],[f60,f8904]) ).
fof(f9025,plain,
! [X0,X1] : join(meet(X0,meet(X0,X1)),X0) = X0,
inference(forward_demodulation,[],[f8943,f1669]) ).
fof(f9064,plain,
! [X0,X1] : join(meet(X0,X1),X0) = X0,
inference(forward_demodulation,[],[f9025,f4337]) ).
fof(f9176,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = join(X0,meet(X0,join(X1,X0))),
inference(superposition,[],[f9064,f1200]) ).
fof(f9185,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(superposition,[],[f9064,f3280]) ).
fof(f9342,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = X0,
inference(forward_demodulation,[],[f9176,f8904]) ).
fof(f14611,plain,
! [X2,X0,X1] : join(X0,meet(meet(X0,X1),X2)) = X0,
inference(superposition,[],[f8923,f8904]) ).
fof(f15215,plain,
! [X2,X0,X1] : join(X1,meet(X0,meet(X1,X2))) = X1,
inference(superposition,[],[f14611,f3554]) ).
fof(f16222,plain,
! [X2,X0,X1] : join(meet(X1,meet(X0,X2)),X0) = X0,
inference(superposition,[],[f9185,f15215]) ).
fof(f272054,plain,
! [X0,X1] : join(X1,X0) = join(join(X0,X1),join(X1,X0)),
inference(superposition,[],[f4397,f9342]) ).
fof(f274007,plain,
! [X0,X1] : join(X1,X0) = meet(join(X0,X1),join(X1,X0)),
inference(superposition,[],[f4110,f272054]) ).
fof(f275466,plain,
! [X0,X1] : join(X0,X1) = join(meet(join(X0,X1),meet(join(X1,X0),join(join(X1,X0),join(X0,X1)))),meet(join(X0,X1),join(X1,X0))),
inference(superposition,[],[f86,f274007]) ).
fof(f275842,plain,
! [X0,X1] : join(X0,X1) = join(meet(join(X0,X1),meet(join(X1,X0),join(join(X1,X0),join(X0,X1)))),join(X1,X0)),
inference(forward_demodulation,[],[f275466,f274007]) ).
fof(f276133,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(forward_demodulation,[],[f275842,f16222]) ).
fof(f278131,plain,
join(a,b) != join(a,b),
inference(superposition,[],[f2,f276133]) ).
fof(f278132,plain,
$false,
inference(trivial_inequality_removal,[],[f278131]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT084-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n005.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 13:59:47 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 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.03/2.84 % (4009748)Will run a generic schedule for satisfiability detection.
% 16.03/2.84 % (4009758)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1974085478:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.03/2.84 % (4009755)% WARNING: option uhcvi not known.
% 16.03/2.84 % (4009755)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2179303397:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.03/2.84 % (4009756)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=753723710:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.03/2.84 % (4009754)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2663124235_2999 on theBenchmark for (2999ds/0Mi)
% 16.03/2.84 % (4009759)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2385452060:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.03/2.84 % (4009757)dis+10_1_sil=32000:sp=arity:random_seed=3150931833:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.03/2.84 % TRYING [1]
% 16.03/2.84 % TRYING [2]
% 16.03/2.84 % (4009760)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3614495107:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.03/2.84 % TRYING [3]
% 16.03/2.84 % (4009758)Instruction limit reached!
% 16.03/2.84 % (4009758)------------------------------
% 16.03/2.84 % (4009758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.03/2.84 % (4009758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.03/2.84 % (4009758)CaDiCaL version: 2.1.3
% 16.03/2.84 % (4009758)Termination reason: Instruction limit
% 16.03/2.84 % (4009758)Termination phase: Saturation
% 16.03/2.84 % (4009758)Time elapsed: 0.047 s
% 16.03/2.84 % (4009758)Peak memory usage: 15 MB
% 16.03/2.84 % (4009758)Instructions burned: 116 (million)
% 16.03/2.84 % (4009775)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3447792770:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.03/2.84 % TRYING [1]
% 16.03/2.84 % TRYING [2]
% 16.03/2.84 % TRYING [3]
% 16.03/2.84 % (4009759)Instruction limit reached!
% 16.03/2.84 % (4009759)------------------------------
% 16.03/2.84 % (4009759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.03/2.84 % (4009759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.03/2.84 % (4009759)CaDiCaL version: 2.1.3
% 16.03/2.84 % (4009759)Termination reason: Instruction limit
% 16.03/2.84 % (4009759)Termination phase: Saturation
% 16.03/2.84 % (4009759)Time elapsed: 0.071 s
% 16.03/2.84 % (4009759)Peak memory usage: 17 MB
% 16.03/2.84 % (4009759)Instructions burned: 131 (million)
% 16.03/2.84 % (4009757)Instruction limit reached!
% 16.03/2.84 % (4009757)------------------------------
% 16.03/2.84 % (4009757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.03/2.84 % (4009757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.03/2.84 % (4009757)CaDiCaL version: 2.1.3
% 16.03/2.84 % (4009757)Termination reason: Instruction limit
% 16.03/2.84 % (4009757)Termination phase: Saturation
% 16.03/2.84 % (4009757)Time elapsed: 0.080 s
% 16.03/2.84 % (4009757)Peak memory usage: 14 MB
% 16.03/2.84 % (4009757)Instructions burned: 104 (million)
% 16.03/2.84 % (4009777)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1662892440:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.03/2.84 % (4009778)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=476160452:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.03/2.84 % (4009777)Instruction limit reached!
% 16.03/2.84 % (4009777)------------------------------
% 16.03/2.84 % (4009777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.03/2.84 % (4009777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.03/2.84 % (4009777)CaDiCaL version: 2.1.3
% 16.03/2.84 % (4009777)Termination reason: Instruction limit
% 16.03/2.84 % (4009777)Termination phase: Saturation
% 16.03/2.84 % (4009777)Time elapsed: 0.063 s
% 16.03/2.84 % (4009777)Peak memory usage: 13 MB
% 16.03/2.84 % (4009777)Instructions burned: 133 (million)
% 16.03/2.84 % (4009760)Instruction limit reached!
% 16.03/2.84 % (4009760)------------------------------
% 16.03/2.84 % (4009760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.03/2.84 % (4009760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.03/2.84 % (4009760)CaDiCaL version: 2.1.3
% 16.03/2.84 % (4009760)Termination reason: Instruction limit
% 50.74/7.68 % (4009760)Termination phase: Saturation
% 50.74/7.68 % (4009760)Time elapsed: 0.154 s
% 50.74/7.68 % (4009760)Peak memory usage: 14 MB
% 50.74/7.68 % (4009760)Instructions burned: 160 (million)
% 50.74/7.68 % (4009781)ott-21_1_sil=16000:fs=off:random_seed=3585865430:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 50.74/7.68 % (4009783)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3490889357:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 50.74/7.68 % (4009781)Instruction limit reached!
% 50.74/7.68 % (4009781)------------------------------
% 50.74/7.68 % (4009781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.74/7.68 % (4009781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.74/7.68 % (4009781)CaDiCaL version: 2.1.3
% 50.74/7.68 % (4009781)Termination reason: Instruction limit
% 50.74/7.68 % (4009781)Termination phase: Saturation
% 50.74/7.68 % (4009781)Time elapsed: 0.124 s
% 50.74/7.68 % (4009781)Peak memory usage: 15 MB
% 50.74/7.68 % (4009781)Instructions burned: 181 (million)
% 50.74/7.68 % (4009792)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1451742685:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 50.74/7.68 % TRYING [1]
% 50.74/7.68 % TRYING [2]
% 50.74/7.68 % TRYING [3]
% 50.74/7.68 % (4009775)Instruction limit reached!
% 50.74/7.68 % (4009775)------------------------------
% 50.74/7.68 % (4009775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.74/7.68 % (4009775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.74/7.68 % (4009775)CaDiCaL version: 2.1.3
% 50.74/7.68 % (4009775)Termination reason: Instruction limit
% 50.74/7.68 % (4009775)Termination phase: Finite model building SAT solving
% 50.74/7.68 % (4009775)Time elapsed: 0.336 s
% 50.74/7.68 % (4009775)Peak memory usage: 15 MB
% 50.74/7.68 % (4009775)Instructions burned: 714 (million)
% 50.74/7.68 % (4009795)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1677011472:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 50.74/7.68 % (4009783)Instruction limit reached!
% 50.74/7.68 % (4009783)------------------------------
% 50.74/7.68 % (4009783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.74/7.68 % (4009783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.74/7.68 % (4009783)CaDiCaL version: 2.1.3
% 50.74/7.68 % (4009783)Termination reason: Instruction limit
% 50.74/7.68 % (4009783)Termination phase: Saturation
% 50.74/7.68 % (4009783)Time elapsed: 0.486 s
% 50.74/7.68 % (4009783)Peak memory usage: 26 MB
% 50.74/7.68 % (4009783)Instructions burned: 477 (million)
% 50.74/7.68 % (4009800)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=514309870:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 50.74/7.68 % (4009778)Instruction limit reached!
% 50.74/7.68 % (4009778)------------------------------
% 50.74/7.68 % (4009778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.74/7.68 % (4009778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.74/7.68 % (4009778)CaDiCaL version: 2.1.3
% 50.74/7.68 % (4009778)Termination reason: Instruction limit
% 50.74/7.68 % (4009778)Termination phase: Saturation
% 50.74/7.68 % (4009778)Time elapsed: 0.591 s
% 50.74/7.68 % (4009778)Peak memory usage: 18 MB
% 50.74/7.68 % (4009778)Instructions burned: 684 (million)
% 50.74/7.68 % (4009804)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=1625914397: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)
% 50.74/7.68 % (4009792)Instruction limit reached!
% 50.74/7.68 % (4009792)------------------------------
% 50.74/7.68 % (4009792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.74/7.68 % (4009792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.74/7.68 % (4009792)CaDiCaL version: 2.1.3
% 50.74/7.68 % (4009792)Termination reason: Instruction limit
% 50.74/7.68 % (4009792)Termination phase: Finite model building SAT solving
% 50.74/7.68 % (4009792)Time elapsed: 0.463 s
% 50.74/7.68 % (4009792)Peak memory usage: 14 MB
% 50.74/7.68 % (4009792)Instructions burned: 866 (million)
% 50.74/7.68 % (4009806)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4291020098:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 50.74/7.68 % (4009804)Instruction limit reached!
% 50.74/7.68 % (4009804)------------------------------
% 50.74/7.68 % (4009804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009804)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009804)Termination reason: Instruction limit
% 79.12/11.66 % (4009804)Termination phase: Saturation
% 79.12/11.66 % (4009804)Time elapsed: 0.459 s
% 79.12/11.66 % (4009804)Peak memory usage: 27 MB
% 79.12/11.66 % (4009804)Instructions burned: 693 (million)
% 79.12/11.66 % (4009806)Instruction limit reached!
% 79.12/11.66 % (4009806)------------------------------
% 79.12/11.66 % (4009806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009806)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009806)Termination reason: Instruction limit
% 79.12/11.66 % (4009806)Termination phase: Saturation
% 79.12/11.66 % (4009806)Time elapsed: 0.388 s
% 79.12/11.66 % (4009806)Peak memory usage: 31 MB
% 79.12/11.66 % (4009806)Instructions burned: 886 (million)
% 79.12/11.66 % (4009812)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1854331779:i=9515:nm=5_2987 on theBenchmark for (2987ds/9515Mi)
% 79.12/11.66 % (4009811)fmb+10_1_sil=64000:random_seed=4214119743:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi)
% 79.12/11.66 % TRYING [20]
% 79.12/11.66 % TRYING [1]
% 79.12/11.66 % (4009795)Instruction limit reached!
% 79.12/11.66 % (4009795)------------------------------
% 79.12/11.66 % (4009795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009795)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009795)Termination reason: Instruction limit
% 79.12/11.66 % (4009795)Termination phase: Saturation
% 79.12/11.66 % (4009795)Time elapsed: 0.840 s
% 79.12/11.66 % (4009795)Peak memory usage: 59 MB
% 79.12/11.66 % (4009795)Instructions burned: 1180 (million)
% 79.12/11.66 % TRYING [2]
% 79.12/11.66 % TRYING [3]
% 79.12/11.66 % (4009815)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=509773262:fmbsr=1.7:i=920_2986 on theBenchmark for (2986ds/920Mi)
% 79.12/11.66 % TRYING [8]
% 79.12/11.66 % (4009800)Instruction limit reached!
% 79.12/11.66 % (4009800)------------------------------
% 79.12/11.66 % (4009800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009800)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009800)Termination reason: Instruction limit
% 79.12/11.66 % (4009800)Termination phase: Finite model building constraint generation
% 79.12/11.66 % (4009800)Time elapsed: 0.739 s
% 79.12/11.66 % (4009800)Peak memory usage: 107 MB
% 79.12/11.66 % (4009800)Instructions burned: 890 (million)
% 79.12/11.66 % (4009818)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4292659903:i=5131_2984 on theBenchmark for (2984ds/5131Mi)
% 79.12/11.66 % (4009815)Instruction limit reached!
% 79.12/11.66 % (4009815)------------------------------
% 79.12/11.66 % (4009815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009815)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009815)Termination reason: Instruction limit
% 79.12/11.66 % (4009815)Termination phase: Finite model building constraint generation
% 79.12/11.66 % (4009815)Time elapsed: 0.319 s
% 79.12/11.66 % (4009815)Peak memory usage: 74 MB
% 79.12/11.66 % (4009815)Instructions burned: 925 (million)
% 79.12/11.66 % (4009821)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3984326889:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 79.12/11.66 % (4009821)Instruction limit reached!
% 79.12/11.66 % (4009821)------------------------------
% 79.12/11.66 % (4009821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009821)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009821)Termination reason: Instruction limit
% 79.12/11.66 % (4009821)Termination phase: Saturation
% 79.12/11.66 % (4009821)Time elapsed: 0.713 s
% 79.12/11.66 % (4009821)Peak memory usage: 25 MB
% 79.12/11.66 % (4009821)Instructions burned: 1473 (million)
% 79.12/11.66 % (4009933)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1746120074:i=6324_2976 on theBenchmark for (2976ds/6324Mi)
% 79.12/11.66 % (4009933)Cannot represent all propositional literals internally
% 79.12/11.66 % (4009933)Refutation not found, incomplete strategy
% 79.12/11.66 % (4009933)------------------------------
% 79.12/11.66 % (4009933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009933)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009933)Termination reason: Refutation not found, incomplete strategy
% 79.12/11.66 % (4009933)Time elapsed: 0.004 s
% 79.12/11.66 % (4009933)Peak memory usage: 10 MB
% 79.12/11.66 % (4009933)Instructions burned: 6 (million)
% 79.12/11.66 % (4009933)------------------------------
% 79.12/11.66 % (4009933)------------------------------
% 79.12/11.66 % (4009940)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1514705550:fmbsr=2.30978:i=2174_2975 on theBenchmark for (2975ds/2174Mi)
% 79.12/11.66 % TRYING [16]
% 79.12/11.66 % (4009940)Instruction limit reached!
% 79.12/11.66 % (4009940)------------------------------
% 79.12/11.66 % (4009940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009940)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009940)Termination reason: Instruction limit
% 79.12/11.66 % (4009940)Termination phase: Finite model building constraint generation
% 79.12/11.66 % (4009940)Time elapsed: 0.758 s
% 79.12/11.66 % (4009940)Peak memory usage: 137 MB
% 79.12/11.66 % (4009940)Instructions burned: 2177 (million)
% 79.12/11.66 % (4009981)ott-2_1_sil=16000:newcnf=on:random_seed=2105865575:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2967 on theBenchmark for (2967ds/869Mi)
% 79.12/11.66 % (4009981)Instruction limit reached!
% 79.12/11.66 % (4009981)------------------------------
% 79.12/11.66 % (4009981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009981)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009981)Termination reason: Instruction limit
% 79.12/11.66 % (4009981)Termination phase: Saturation
% 79.12/11.66 % (4009981)Time elapsed: 0.404 s
% 79.12/11.66 % (4009981)Peak memory usage: 38 MB
% 79.12/11.66 % (4009981)Instructions burned: 869 (million)
% 79.12/11.66 % (4009983)ott+10_1_sil=32000:tgt=ground:random_seed=2688260606:i=5114:av=off_2963 on theBenchmark for (2963ds/5114Mi)
% 79.12/11.66 % (4009818)Instruction limit reached!
% 79.12/11.66 % (4009818)------------------------------
% 79.12/11.66 % (4009818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009818)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009818)Termination reason: Instruction limit
% 79.12/11.66 % (4009818)Termination phase: Saturation
% 79.12/11.66 % (4009818)Time elapsed: 2.332 s
% 79.12/11.66 % (4009818)Peak memory usage: 38 MB
% 79.12/11.66 % (4009818)Instructions burned: 5132 (million)
% 79.12/11.66 % (4009985)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2100684004:i=54282_2961 on theBenchmark for (2961ds/54282Mi)
% 79.12/11.66 % TRYING [1]
% 79.12/11.66 % TRYING [2]
% 79.12/11.66 % TRYING [3]
% 79.12/11.66 % (4009812)Instruction limit reached!
% 79.12/11.66 % (4009812)------------------------------
% 79.12/11.66 % (4009812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009812)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009812)Termination reason: Instruction limit
% 79.12/11.66 % (4009812)Termination phase: Finite model building constraint generation
% 79.12/11.66 % (4009812)Time elapsed: 3.643 s
% 79.12/11.66 % (4009812)Peak memory usage: 671 MB
% 79.12/11.66 % (4009812)Instructions burned: 9518 (million)
% 79.12/11.66 % (4009987)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2878096025:i=3512:aac=none_2949 on theBenchmark for (2949ds/3512Mi)
% 79.12/11.66 % (4009983)Instruction limit reached!
% 79.12/11.66 % (4009983)------------------------------
% 79.12/11.66 % (4009983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009983)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009983)Termination reason: Instruction limit
% 79.12/11.66 % (4009983)Termination phase: Saturation
% 79.12/11.66 % (4009983)Time elapsed: 2.537 s
% 79.12/11.66 % (4009983)Peak memory usage: 234 MB
% 79.12/11.66 % (4009983)Instructions burned: 5114 (million)
% 79.12/11.66 % (4009989)dis+21_1_sil=32000:sas=cadical:random_seed=4196639313:i=3773:amm=off_2937 on theBenchmark for (2937ds/3773Mi)
% 79.12/11.66 % (4009987)Instruction limit reached!
% 79.12/11.66 % (4009987)------------------------------
% 79.12/11.66 % (4009987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009987)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009987)Termination reason: Instruction limit
% 79.12/11.66 % (4009987)Termination phase: Saturation
% 79.12/11.66 % (4009987)Time elapsed: 2.222 s
% 79.12/11.66 % (4009987)Peak memory usage: 37 MB
% 79.12/11.66 % (4009987)Instructions burned: 3513 (million)
% 79.12/11.66 % (4009991)ott+11_1_sil=16000:gs=on:random_seed=3471980257:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2927 on theBenchmark for (2927ds/2251Mi)
% 79.12/11.66 % (4009991)Instruction limit reached!
% 79.12/11.66 % (4009991)------------------------------
% 79.12/11.66 % (4009991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009991)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009991)Termination reason: Instruction limit
% 79.12/11.66 % (4009991)Termination phase: Saturation
% 79.12/11.66 % (4009991)Time elapsed: 0.947 s
% 79.12/11.66 % (4009991)Peak memory usage: 69 MB
% 79.12/11.66 % (4009991)Instructions burned: 2252 (million)
% 79.12/11.66 % (4009993)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2484655291:fmbsr=1.6:i=67534_2917 on theBenchmark for (2917ds/67534Mi)
% 79.12/11.66 % TRYING [7]
% 79.12/11.66 % (4009989)Instruction limit reached!
% 79.12/11.66 % (4009989)------------------------------
% 79.12/11.66 % (4009989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009989)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009989)Termination reason: Instruction limit
% 79.12/11.66 % (4009989)Termination phase: Saturation
% 79.12/11.66 % (4009989)Time elapsed: 2.499 s
% 79.12/11.66 % (4009989)Peak memory usage: 39 MB
% 79.12/11.66 % (4009989)Instructions burned: 3775 (million)
% 79.12/11.66 % (4009995)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4090951383:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2912 on theBenchmark for (2912ds/4591Mi)
% 79.12/11.66 % (4009995)Instruction limit reached!
% 79.12/11.66 % (4009995)------------------------------
% 79.12/11.66 % (4009995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009995)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009995)Termination reason: Instruction limit
% 79.12/11.66 % (4009995)Termination phase: Saturation
% 79.12/11.66 % (4009995)Time elapsed: 1.754 s
% 79.12/11.66 % (4009995)Peak memory usage: 25 MB
% 79.12/11.66 % (4009995)Instructions burned: 4592 (million)
% 79.12/11.66 % (4009997)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1772423612:i=29340_2894 on theBenchmark for (2894ds/29340Mi)
% 79.12/11.66 % (4009756) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4009748-4009756"...
% 79.12/11.66 % (4009756)...printing done.
% 79.12/11.66 % (4009756)Refutation found. Thanks to Tanya!
% 79.12/11.66 % SZS status Unsatisfiable for theBenchmark
% 79.12/11.66 % SZS output start Proof for theBenchmark
% See solution above
% 79.12/11.66 % (4009756)------------------------------
% 79.12/11.66 % (4009756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.12/11.66 % (4009756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.12/11.66 % (4009756)CaDiCaL version: 2.1.3
% 79.12/11.66 % (4009756)Termination reason: Refutation
% 79.12/11.66 % (4009756)Time elapsed: 11.148 s
% 79.12/11.66 % (4009756)Peak memory usage: 125 MB
% 79.12/11.66 % (4009756)Instructions burned: 24359 (million)
% 79.12/11.66 % (4009748)Success in time 11.233 s
% 79.12/11.66 % Vampire exiting
%------------------------------------------------------------------------------