%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ164-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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 12:32:38 PM UTC 2026
% Result : Unsatisfiable 136.53s 37.65s
% Output : Refutation 136.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 14
% Syntax : Number of formulae : 73 ( 73 unt; 0 def)
% Number of atoms : 73 ( 72 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-5 aty)
% Number of variables : 293 ( 293 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
eq(zero,zero) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule1) ).
fof(f2,axiom,
! [X0] : eq(zero,s(X0)) = false,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule2) ).
fof(f5,axiom,
! [X0,X1] : eq(s(X0),s(X1)) = eq(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule4) ).
fof(f8,axiom,
! [X0] : or(false,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule6) ).
fof(f9,axiom,
! [X0] : union(empty,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule7) ).
fof(f10,axiom,
! [X2,X3,X0,X1] : union(edge(X0,X1,X2),X3) = edge(X0,X1,union(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule8) ).
fof(f11,axiom,
! [X2,X0,X1] : reach(X0,X1,empty,X2) = false,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule9) ).
fof(f12,plain,
! [X2,X0,X1] : false = reach(X0,X1,empty,X2),
inference(reorient_equations,[],[f11]) ).
fof(f13,axiom,
! [X2,X3,X0,X1,X4,X5] : reach(X0,X1,edge(X2,X3,X4),X5) = if_reach_1(eq(X0,X2),X0,X1,edge(X2,X3,X4),X5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule10) ).
fof(f14,axiom,
! [X2,X3,X0,X1,X4,X5] : if_reach_1(true,X0,X1,edge(X2,X3,X4),X5) = if_reach_2(eq(X1,X3),X0,X1,edge(X2,X3,X4),X5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule11) ).
fof(f15,axiom,
! [X2,X3,X0,X1,X4,X5] : if_reach_2(true,X0,X1,edge(X2,X3,X4),X5) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule12) ).
fof(f16,plain,
! [X2,X3,X0,X1,X4,X5] : true = if_reach_2(true,X0,X1,edge(X2,X3,X4),X5),
inference(reorient_equations,[],[f15]) ).
fof(f17,axiom,
! [X2,X3,X0,X1,X4,X5] : if_reach_2(false,X0,X1,edge(X2,X3,X4),X5) = or(reach(X0,X1,X4,X5),reach(X3,X1,union(X4,X5),empty)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule13) ).
fof(f18,axiom,
! [X2,X3,X0,X1,X4,X5] : if_reach_1(false,X0,X1,edge(X2,X3,X4),X5) = reach(X0,X1,X4,edge(X2,X3,X5)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule14) ).
fof(f19,axiom,
g = edge(zero,s(zero),edge(s(zero),s(s(zero)),edge(s(s(zero)),s(s(s(zero))),edge(s(s(s(zero))),zero,empty)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',graph) ).
fof(f20,negated_conjecture,
reach(zero,zero,g,empty) != true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f21,plain,
true != reach(zero,zero,g,empty),
inference(reorient_equations,[],[f20]) ).
fof(f22,plain,
! [X2,X3,X0,X1] : reach(zero,X0,edge(zero,X1,X2),X3) = if_reach_1(true,zero,X0,edge(zero,X1,X2),X3),
inference(superposition,[],[f13,f1]) ).
fof(f23,plain,
! [X2,X3,X0,X1,X4] : reach(zero,X0,edge(s(X1),X2,X3),X4) = if_reach_1(false,zero,X0,edge(s(X1),X2,X3),X4),
inference(superposition,[],[f13,f2]) ).
fof(f25,plain,
! [X2,X3,X0,X1,X4,X5] : reach(s(X0),X2,edge(s(X1),X3,X4),X5) = if_reach_1(eq(X0,X1),s(X0),X2,edge(s(X1),X3,X4),X5),
inference(superposition,[],[f13,f5]) ).
fof(f27,plain,
! [X2,X3,X0,X1,X4] : reach(zero,X0,edge(s(X1),X2,X3),X4) = reach(zero,X0,X3,edge(s(X1),X2,X4)),
inference(forward_demodulation,[],[f23,f18]) ).
fof(f28,plain,
! [X2,X3,X0,X1] : if_reach_1(true,X0,zero,edge(X1,zero,X2),X3) = if_reach_2(true,X0,zero,edge(X1,zero,X2),X3),
inference(superposition,[],[f14,f1]) ).
fof(f29,plain,
! [X2,X3,X0,X1,X4] : if_reach_1(true,X0,zero,edge(X1,s(X2),X3),X4) = if_reach_2(false,X0,zero,edge(X1,s(X2),X3),X4),
inference(superposition,[],[f14,f2]) ).
fof(f32,plain,
! [X2,X3,X0,X1] : true = if_reach_1(true,X0,zero,edge(X1,zero,X2),X3),
inference(forward_demodulation,[],[f28,f16]) ).
fof(f35,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : if_reach_2(false,X4,X5,edge(X6,X7,edge(X0,X1,X2)),X3) = or(reach(X4,X5,edge(X0,X1,X2),X3),reach(X7,X5,edge(X0,X1,union(X2,X3)),empty)),
inference(superposition,[],[f17,f10]) ).
fof(f36,plain,
! [X2,X3,X0,X1,X6,X4,X5] : if_reach_2(false,X0,X1,edge(X2,X3,X4),X5) = if_reach_2(false,X0,X1,edge(X6,X3,X4),X5),
inference(superposition,[],[f17,f17]) ).
fof(f66,plain,
! [X2,X3,X0,X1,X6,X4,X5] : if_reach_2(false,zero,X0,edge(X5,X6,edge(s(X2),X3,X1)),X4) = or(reach(zero,X0,X1,edge(s(X2),X3,X4)),reach(X6,X0,union(edge(s(X2),X3,X1),X4),empty)),
inference(superposition,[],[f17,f27]) ).
fof(f67,plain,
! [X2,X3,X0,X1,X6,X4,X5] : if_reach_2(false,zero,X0,edge(X5,X6,edge(s(X2),X3,X1)),X4) = or(reach(zero,X0,X1,edge(s(X2),X3,X4)),reach(X6,X0,edge(s(X2),X3,union(X1,X4)),empty)),
inference(forward_demodulation,[],[f66,f10]) ).
fof(f68,plain,
! [X2,X3,X0,X1] : if_reach_2(false,X0,X1,edge(X3,s(zero),edge(s(zero),s(s(zero)),edge(s(s(zero)),s(s(s(zero))),edge(s(s(s(zero))),zero,empty)))),X2) = if_reach_2(false,X0,X1,g,X2),
inference(superposition,[],[f36,f19]) ).
fof(f83,plain,
! [X2,X3,X0,X1,X4,X5] : if_reach_2(false,X0,zero,edge(X1,s(X2),X3),X4) = if_reach_1(true,X0,zero,edge(X5,s(X2),X3),X4),
inference(superposition,[],[f29,f36]) ).
fof(f85,plain,
! [X2,X3,X0,X1,X4] : or(reach(X0,zero,X1,X2),reach(s(X3),zero,union(X1,X2),empty)) = if_reach_1(true,X0,zero,edge(X4,s(X3),X1),X2),
inference(superposition,[],[f29,f17]) ).
fof(f99,plain,
! [X2,X3,X0,X1] : reach(s(zero),X0,edge(s(zero),X1,X2),X3) = if_reach_1(true,s(zero),X0,edge(s(zero),X1,X2),X3),
inference(superposition,[],[f25,f1]) ).
fof(f100,plain,
! [X2,X3,X0,X1,X4] : reach(s(zero),X0,edge(s(s(X1)),X2,X3),X4) = if_reach_1(false,s(zero),X0,edge(s(s(X1)),X2,X3),X4),
inference(superposition,[],[f25,f2]) ).
fof(f102,plain,
! [X2,X3,X0,X1,X4,X5] : reach(s(s(X0)),X2,edge(s(s(X1)),X3,X4),X5) = if_reach_1(eq(X0,X1),s(s(X0)),X2,edge(s(s(X1)),X3,X4),X5),
inference(superposition,[],[f25,f5]) ).
fof(f104,plain,
! [X2,X3,X0,X1,X4] : reach(s(zero),X0,edge(s(s(X1)),X2,X3),X4) = reach(s(zero),X0,X3,edge(s(s(X1)),X2,X4)),
inference(forward_demodulation,[],[f100,f18]) ).
fof(f140,plain,
! [X2,X3,X0,X1,X6,X4,X5] : if_reach_2(false,X1,X2,edge(X3,X4,edge(X5,X6,empty)),X0) = or(reach(X1,X2,edge(X5,X6,empty),X0),reach(X4,X2,edge(X5,X6,X0),empty)),
inference(superposition,[],[f35,f9]) ).
fof(f208,plain,
! [X2,X3,X0,X1,X6,X4] : if_reach_1(true,X0,zero,edge(X1,s(X2),X3),X4) = if_reach_1(true,X0,zero,edge(X6,s(X2),X3),X4),
inference(superposition,[],[f83,f83]) ).
fof(f283,plain,
! [X2,X3,X0,X1,X4,X5] : if_reach_1(true,s(zero),zero,edge(X5,s(X4),edge(s(s(X1)),X2,X0)),X3) = or(reach(s(zero),zero,X0,edge(s(s(X1)),X2,X3)),reach(s(X4),zero,union(edge(s(s(X1)),X2,X0),X3),empty)),
inference(superposition,[],[f85,f104]) ).
fof(f306,plain,
! [X2,X3,X0,X1,X4,X5] : if_reach_1(true,s(zero),zero,edge(X5,s(X4),edge(s(s(X1)),X2,X0)),X3) = or(reach(s(zero),zero,X0,edge(s(s(X1)),X2,X3)),reach(s(X4),zero,edge(s(s(X1)),X2,union(X0,X3)),empty)),
inference(forward_demodulation,[],[f283,f10]) ).
fof(f392,plain,
! [X2,X3,X0,X1] : reach(s(s(zero)),X0,edge(s(s(zero)),X1,X2),X3) = if_reach_1(true,s(s(zero)),X0,edge(s(s(zero)),X1,X2),X3),
inference(superposition,[],[f102,f1]) ).
fof(f393,plain,
! [X2,X3,X0,X1,X4] : reach(s(s(zero)),X0,edge(s(s(s(X1))),X2,X3),X4) = if_reach_1(false,s(s(zero)),X0,edge(s(s(s(X1))),X2,X3),X4),
inference(superposition,[],[f102,f2]) ).
fof(f395,plain,
! [X2,X3,X0,X1,X4,X5] : reach(s(s(s(X0))),X2,edge(s(s(s(X1))),X3,X4),X5) = if_reach_1(eq(X0,X1),s(s(s(X0))),X2,edge(s(s(s(X1))),X3,X4),X5),
inference(superposition,[],[f102,f5]) ).
fof(f397,plain,
! [X2,X3,X0,X1,X4] : reach(s(s(zero)),X0,edge(s(s(s(X1))),X2,X3),X4) = reach(s(s(zero)),X0,X3,edge(s(s(s(X1))),X2,X4)),
inference(forward_demodulation,[],[f393,f18]) ).
fof(f961,plain,
! [X0,X1] : or(reach(zero,X0,edge(s(s(zero)),s(s(s(zero))),edge(s(s(s(zero))),zero,empty)),edge(s(zero),s(s(zero)),X1)),reach(s(zero),X0,edge(s(zero),s(s(zero)),union(edge(s(s(zero)),s(s(s(zero))),edge(s(s(s(zero))),zero,empty)),X1)),empty)) = if_reach_2(false,zero,X0,g,X1),
inference(superposition,[],[f67,f68]) ).
fof(f971,plain,
! [X0,X1] : if_reach_2(false,zero,X0,g,X1) = or(reach(zero,X0,edge(s(s(zero)),s(s(s(zero))),edge(s(s(s(zero))),zero,empty)),edge(s(zero),s(s(zero)),X1)),reach(s(zero),X0,edge(s(zero),s(s(zero)),edge(s(s(zero)),s(s(s(zero))),union(edge(s(s(s(zero))),zero,empty),X1))),empty)),
inference(forward_demodulation,[],[f961,f10]) ).
fof(f979,plain,
! [X0,X1] : if_reach_2(false,zero,X0,g,X1) = or(reach(zero,X0,edge(s(s(zero)),s(s(s(zero))),edge(s(s(s(zero))),zero,empty)),edge(s(zero),s(s(zero)),X1)),reach(s(zero),X0,edge(s(zero),s(s(zero)),edge(s(s(zero)),s(s(s(zero))),edge(s(s(s(zero))),zero,union(empty,X1)))),empty)),
inference(forward_demodulation,[],[f971,f10]) ).
fof(f985,plain,
! [X0,X1] : if_reach_2(false,zero,X0,g,X1) = or(reach(zero,X0,edge(s(s(zero)),s(s(s(zero))),edge(s(s(s(zero))),zero,empty)),edge(s(zero),s(s(zero)),X1)),reach(s(zero),X0,edge(s(zero),s(s(zero)),edge(s(s(zero)),s(s(s(zero))),edge(s(s(s(zero))),zero,X1))),empty)),
inference(forward_demodulation,[],[f979,f9]) ).
fof(f991,plain,
! [X0,X1] : if_reach_2(false,zero,X0,g,X1) = or(reach(zero,X0,edge(s(s(s(zero))),zero,empty),edge(s(s(zero)),s(s(s(zero))),edge(s(zero),s(s(zero)),X1))),reach(s(zero),X0,edge(s(zero),s(s(zero)),edge(s(s(zero)),s(s(s(zero))),edge(s(s(s(zero))),zero,X1))),empty)),
inference(forward_demodulation,[],[f985,f27]) ).
fof(f994,plain,
! [X0,X1] : if_reach_2(false,zero,X0,g,X1) = or(reach(zero,X0,empty,edge(s(s(s(zero))),zero,edge(s(s(zero)),s(s(s(zero))),edge(s(zero),s(s(zero)),X1)))),reach(s(zero),X0,edge(s(zero),s(s(zero)),edge(s(s(zero)),s(s(s(zero))),edge(s(s(s(zero))),zero,X1))),empty)),
inference(forward_demodulation,[],[f991,f27]) ).
fof(f996,plain,
! [X0,X1] : if_reach_2(false,zero,X0,g,X1) = or(false,reach(s(zero),X0,edge(s(zero),s(s(zero)),edge(s(s(zero)),s(s(s(zero))),edge(s(s(s(zero))),zero,X1))),empty)),
inference(forward_demodulation,[],[f994,f12]) ).
fof(f1708,plain,
! [X2,X3,X0,X1] : reach(zero,zero,edge(zero,s(X0),X1),X2) = if_reach_1(true,zero,zero,edge(X3,s(X0),X1),X2),
inference(superposition,[],[f208,f22]) ).
fof(f1709,plain,
! [X2,X3,X0,X1] : reach(s(zero),zero,edge(s(zero),s(X0),X1),X2) = if_reach_1(true,s(zero),zero,edge(X3,s(X0),X1),X2),
inference(superposition,[],[f208,f99]) ).
fof(f2472,plain,
! [X2,X3,X0,X1] : reach(s(s(zero)),zero,edge(s(s(zero)),s(X1),X2),X3) = if_reach_2(false,s(s(zero)),zero,edge(X0,s(X1),X2),X3),
inference(superposition,[],[f392,f83]) ).
fof(f2599,plain,
! [X2,X3,X0,X1,X4,X5] : if_reach_2(false,s(s(zero)),X0,edge(X4,X5,edge(s(s(s(X1))),X2,empty)),X3) = or(reach(s(s(zero)),X0,empty,edge(s(s(s(X1))),X2,X3)),reach(X5,X0,edge(s(s(s(X1))),X2,X3),empty)),
inference(superposition,[],[f140,f397]) ).
fof(f2614,plain,
! [X2,X3,X0,X1,X4,X5] : if_reach_2(false,s(s(zero)),X0,edge(X4,X5,edge(s(s(s(X1))),X2,empty)),X3) = or(false,reach(X5,X0,edge(s(s(s(X1))),X2,X3),empty)),
inference(forward_demodulation,[],[f2599,f12]) ).
fof(f2617,plain,
! [X2,X3,X0,X1,X4,X5] : if_reach_2(false,s(s(zero)),X0,edge(X4,X5,edge(s(s(s(X1))),X2,empty)),X3) = reach(X5,X0,edge(s(s(s(X1))),X2,X3),empty),
inference(forward_demodulation,[],[f2614,f8]) ).
fof(f3190,plain,
! [X2,X3,X0,X1] : reach(s(s(s(zero))),X0,edge(s(s(s(zero))),X1,X2),X3) = if_reach_1(true,s(s(s(zero))),X0,edge(s(s(s(zero))),X1,X2),X3),
inference(superposition,[],[f395,f1]) ).
fof(f8981,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : if_reach_1(true,s(zero),zero,edge(X6,s(X7),edge(s(s(X3)),X4,edge(s(s(X1)),X2,X0))),X5) = or(reach(s(zero),zero,X0,edge(s(s(X1)),X2,edge(s(s(X3)),X4,X5))),reach(s(X7),zero,edge(s(s(X3)),X4,union(edge(s(s(X1)),X2,X0),X5)),empty)),
inference(superposition,[],[f306,f104]) ).
fof(f9012,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : if_reach_1(true,s(zero),zero,edge(X6,s(X7),edge(s(s(X3)),X4,edge(s(s(X1)),X2,X0))),X5) = or(reach(s(zero),zero,X0,edge(s(s(X1)),X2,edge(s(s(X3)),X4,X5))),reach(s(X7),zero,edge(s(s(X3)),X4,edge(s(s(X1)),X2,union(X0,X5))),empty)),
inference(forward_demodulation,[],[f8981,f10]) ).
fof(f20184,plain,
! [X2,X3,X0,X1] : if_reach_2(false,zero,zero,edge(X0,s(X1),X2),X3) = reach(zero,zero,edge(zero,s(X1),X2),X3),
inference(superposition,[],[f1708,f83]) ).
fof(f31543,plain,
! [X2,X3,X0,X1] : reach(s(s(zero)),zero,edge(s(s(zero)),s(X0),edge(s(s(s(X1))),X2,empty)),X3) = reach(s(X0),zero,edge(s(s(s(X1))),X2,X3),empty),
inference(superposition,[],[f2617,f2472]) ).
fof(f34686,plain,
! [X0,X1] : true = reach(s(s(s(zero))),zero,edge(s(s(s(zero))),zero,X0),X1),
inference(superposition,[],[f3190,f32]) ).
fof(f172275,plain,
! [X2,X3,X0,X1,X7,X4,X5] : or(reach(s(zero),zero,X0,edge(s(s(X1)),X2,edge(s(s(X3)),X4,X5))),reach(s(X7),zero,edge(s(s(X3)),X4,edge(s(s(X1)),X2,union(X0,X5))),empty)) = reach(s(zero),zero,edge(s(zero),s(X7),edge(s(s(X3)),X4,edge(s(s(X1)),X2,X0))),X5),
inference(forward_demodulation,[],[f9012,f1709]) ).
fof(f178595,plain,
! [X2,X3,X0,X1,X4,X5] : reach(s(zero),zero,edge(s(zero),s(X5),edge(s(s(X3)),X4,edge(s(s(X1)),X2,empty))),X0) = or(reach(s(zero),zero,empty,edge(s(s(X1)),X2,edge(s(s(X3)),X4,X0))),reach(s(X5),zero,edge(s(s(X3)),X4,edge(s(s(X1)),X2,X0)),empty)),
inference(superposition,[],[f172275,f9]) ).
fof(f178612,plain,
! [X2,X3,X0,X1,X4,X5] : reach(s(zero),zero,edge(s(zero),s(X5),edge(s(s(X3)),X4,edge(s(s(X1)),X2,empty))),X0) = or(false,reach(s(X5),zero,edge(s(s(X3)),X4,edge(s(s(X1)),X2,X0)),empty)),
inference(forward_demodulation,[],[f178595,f12]) ).
fof(f178625,plain,
! [X2,X3,X0,X1,X4,X5] : reach(s(zero),zero,edge(s(zero),s(X5),edge(s(s(X3)),X4,edge(s(s(X1)),X2,empty))),X0) = reach(s(X5),zero,edge(s(s(X3)),X4,edge(s(s(X1)),X2,X0)),empty),
inference(forward_demodulation,[],[f178612,f8]) ).
fof(f263354,plain,
! [X0] : reach(zero,zero,g,X0) = if_reach_2(false,zero,zero,g,X0),
inference(superposition,[],[f20184,f19]) ).
fof(f613354,plain,
if_reach_2(false,zero,zero,g,empty) = or(false,reach(s(s(zero)),zero,edge(s(s(zero)),s(s(s(zero))),edge(s(s(s(zero))),zero,empty)),empty)),
inference(superposition,[],[f996,f178625]) ).
fof(f613597,plain,
if_reach_2(false,zero,zero,g,empty) = or(false,reach(s(s(s(zero))),zero,edge(s(s(s(zero))),zero,empty),empty)),
inference(forward_demodulation,[],[f613354,f31543]) ).
fof(f613706,plain,
or(false,true) = if_reach_2(false,zero,zero,g,empty),
inference(forward_demodulation,[],[f613597,f34686]) ).
fof(f613801,plain,
true = if_reach_2(false,zero,zero,g,empty),
inference(forward_demodulation,[],[f613706,f8]) ).
fof(f613914,plain,
true = reach(zero,zero,g,empty),
inference(superposition,[],[f263354,f613801]) ).
fof(f613920,plain,
$false,
inference(forward_subsumption_resolution,[],[f613914,f21]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ164-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n003.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 22:48:41 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 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
% 23.23/3.76 % (1000091)Will run a generic schedule for satisfiability detection.
% 23.23/3.76 % (1000098)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1128291168:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 23.23/3.76 % (1000097)% WARNING: option uhcvi not known.
% 23.23/3.76 % (1000097)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3380641626:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 23.23/3.76 % (1000096)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2606966688_2999 on theBenchmark for (2999ds/0Mi)
% 23.23/3.76 % (1000099)dis+10_1_sil=32000:sp=arity:random_seed=38286830:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 23.23/3.76 % (1000101)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2050640921:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 23.23/3.76 % (1000100)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=730930911:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 23.23/3.76 % TRYING [1]
% 23.23/3.76 % TRYING [2]
% 23.23/3.76 % TRYING [3]
% 23.23/3.76 % (1000102)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3454689725:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 23.23/3.76 % TRYING [4]
% 23.23/3.76 % (1000099)Instruction limit reached!
% 23.23/3.76 % (1000099)------------------------------
% 23.23/3.76 % (1000099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.23/3.76 % (1000099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.23/3.76 % (1000099)CaDiCaL version: 2.1.3
% 23.23/3.76 % (1000099)Termination reason: Instruction limit
% 23.23/3.76 % (1000099)Termination phase: Saturation
% 23.23/3.76 % (1000099)Time elapsed: 0.065 s
% 23.23/3.76 % (1000099)Peak memory usage: 12 MB
% 23.23/3.76 % (1000099)Instructions burned: 104 (million)
% 23.23/3.76 % (1000100)Instruction limit reached!
% 23.23/3.76 % (1000100)------------------------------
% 23.23/3.76 % (1000100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.23/3.76 % (1000100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.23/3.76 % (1000100)CaDiCaL version: 2.1.3
% 23.23/3.76 % (1000100)Termination reason: Instruction limit
% 23.23/3.76 % (1000100)Termination phase: Saturation
% 23.23/3.76 % (1000100)Time elapsed: 0.074 s
% 23.23/3.76 % (1000100)Peak memory usage: 12 MB
% 23.23/3.76 % (1000100)Instructions burned: 117 (million)
% 23.23/3.76 % (1000101)Instruction limit reached!
% 23.23/3.76 % (1000101)------------------------------
% 23.23/3.76 % (1000101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.23/3.76 % (1000101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.23/3.76 % (1000101)CaDiCaL version: 2.1.3
% 23.23/3.76 % (1000101)Termination reason: Instruction limit
% 23.23/3.76 % (1000101)Termination phase: Saturation
% 23.23/3.76 % (1000101)Time elapsed: 0.083 s
% 23.23/3.76 % (1000101)Peak memory usage: 13 MB
% 23.23/3.76 % (1000101)Instructions burned: 131 (million)
% 23.23/3.76 % (1000119)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1395830070:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 23.23/3.76 % TRYING [1]
% 23.23/3.76 % TRYING [2]
% 23.23/3.76 % TRYING [3]
% 23.23/3.76 % (1000123)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3259889837:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 23.23/3.76 % (1000126)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=3244824067:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 23.23/3.76 % (1000102)Instruction limit reached!
% 23.23/3.76 % (1000102)------------------------------
% 23.23/3.76 % (1000102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.23/3.76 % (1000102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.23/3.76 % (1000102)CaDiCaL version: 2.1.3
% 23.23/3.76 % (1000102)Termination reason: Instruction limit
% 23.23/3.76 % (1000102)Termination phase: Saturation
% 23.23/3.76 % (1000102)Time elapsed: 0.098 s
% 23.23/3.76 % (1000102)Peak memory usage: 12 MB
% 23.23/3.76 % (1000102)Instructions burned: 159 (million)
% 23.23/3.76 % TRYING [4]
% 23.23/3.76 % (1000141)ott-21_1_sil=16000:fs=off:random_seed=2097451291:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 23.23/3.76 % (1000123)Instruction limit reached!
% 23.23/3.76 % (1000123)------------------------------
% 23.23/3.76 % (1000123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.23/3.76 % (1000123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.53/10.57 % (1000123)CaDiCaL version: 2.1.3
% 71.53/10.57 % (1000123)Termination reason: Instruction limit
% 71.53/10.57 % (1000123)Termination phase: Saturation
% 71.53/10.57 % (1000123)Time elapsed: 0.089 s
% 71.53/10.57 % (1000123)Peak memory usage: 13 MB
% 71.53/10.57 % (1000123)Instructions burned: 131 (million)
% 71.53/10.57 % (1000166)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4069607493:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 71.53/10.57 % TRYING [5]
% 71.53/10.57 % (1000141)Instruction limit reached!
% 71.53/10.57 % (1000141)------------------------------
% 71.53/10.57 % (1000141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.53/10.57 % (1000141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.53/10.57 % (1000141)CaDiCaL version: 2.1.3
% 71.53/10.57 % (1000141)Termination reason: Instruction limit
% 71.53/10.57 % (1000141)Termination phase: Saturation
% 71.53/10.57 % (1000141)Time elapsed: 0.077 s
% 71.53/10.57 % (1000141)Peak memory usage: 11 MB
% 71.53/10.57 % (1000141)Instructions burned: 181 (million)
% 71.53/10.57 % (1000186)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1574924991:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 71.53/10.57 % TRYING [1]
% 71.53/10.57 % TRYING [2]
% 71.53/10.57 % TRYING [3]
% 71.53/10.57 % TRYING [4]
% 71.53/10.57 % TRYING [5]
% 71.53/10.57 % (1000119)Instruction limit reached!
% 71.53/10.57 % (1000119)------------------------------
% 71.53/10.57 % (1000119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.53/10.57 % (1000119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.53/10.57 % (1000119)CaDiCaL version: 2.1.3
% 71.53/10.57 % (1000119)Termination reason: Instruction limit
% 71.53/10.57 % (1000119)Termination phase: Finite model building constraint generation
% 71.53/10.57 % (1000119)Time elapsed: 0.280 s
% 71.53/10.57 % (1000119)Peak memory usage: 42 MB
% 71.53/10.57 % (1000119)Instructions burned: 716 (million)
% 71.53/10.57 % (1000213)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2368042978:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 71.53/10.57 % (1000166)Instruction limit reached!
% 71.53/10.57 % (1000166)------------------------------
% 71.53/10.57 % (1000166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.53/10.57 % (1000166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.53/10.57 % (1000166)CaDiCaL version: 2.1.3
% 71.53/10.57 % (1000166)Termination reason: Instruction limit
% 71.53/10.57 % (1000166)Termination phase: Saturation
% 71.53/10.57 % (1000166)Time elapsed: 0.283 s
% 71.53/10.57 % (1000166)Peak memory usage: 15 MB
% 71.53/10.57 % (1000166)Instructions burned: 478 (million)
% 71.53/10.57 % (1000126)Instruction limit reached!
% 71.53/10.57 % (1000126)------------------------------
% 71.53/10.57 % (1000126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.53/10.57 % (1000126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.53/10.57 % (1000126)CaDiCaL version: 2.1.3
% 71.53/10.57 % (1000126)Termination reason: Instruction limit
% 71.53/10.57 % (1000126)Termination phase: Saturation
% 71.53/10.57 % (1000126)Time elapsed: 0.394 s
% 71.53/10.57 % (1000126)Peak memory usage: 16 MB
% 71.53/10.57 % (1000126)Instructions burned: 685 (million)
% 71.53/10.57 % (1000225)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1852948923:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 71.53/10.57 % (1000226)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=2234420964:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 71.53/10.57 % (1000186)Instruction limit reached!
% 71.53/10.57 % (1000186)------------------------------
% 71.53/10.57 % (1000186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.53/10.57 % (1000186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.53/10.57 % (1000186)CaDiCaL version: 2.1.3
% 71.53/10.57 % (1000186)Termination reason: Instruction limit
% 71.53/10.57 % (1000186)Termination phase: Finite model building SAT solving
% 71.53/10.57 % (1000186)Time elapsed: 0.349 s
% 71.53/10.57 % (1000186)Peak memory usage: 33 MB
% 71.53/10.57 % (1000186)Instructions burned: 866 (million)
% 71.53/10.57 % (1000229)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3245590420:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 71.53/10.57 % (1000225)Instruction limit reached!
% 71.53/10.57 % (1000225)------------------------------
% 158.28/22.79 % (1000225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 158.28/22.79 % (1000225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.28/22.79 % (1000225)CaDiCaL version: 2.1.3
% 158.28/22.79 % (1000225)Termination reason: Instruction limit
% 158.28/22.79 % (1000225)Termination phase: Finite model building constraint generation
% 158.28/22.79 % (1000225)Time elapsed: 0.547 s
% 158.28/22.79 % (1000225)Peak memory usage: 107 MB
% 158.28/22.79 % (1000225)Instructions burned: 890 (million)
% 158.28/22.79 % (1000226)Instruction limit reached!
% 158.28/22.79 % (1000226)------------------------------
% 158.28/22.79 % (1000226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 158.28/22.79 % (1000226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.28/22.79 % (1000226)CaDiCaL version: 2.1.3
% 158.28/22.79 % (1000226)Termination reason: Instruction limit
% 158.28/22.79 % (1000226)Termination phase: Saturation
% 158.28/22.79 % (1000226)Time elapsed: 0.546 s
% 158.28/22.79 % (1000226)Peak memory usage: 19 MB
% 158.28/22.79 % (1000226)Instructions burned: 692 (million)
% 158.28/22.79 % (1000341)fmb+10_1_sil=64000:random_seed=4099969187:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 158.28/22.79 % TRYING [1]
% 158.28/22.79 % TRYING [2]
% 158.28/22.79 % (1000342)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3967815259:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi)
% 158.28/22.79 % TRYING [20]
% 158.28/22.79 % TRYING [3]
% 158.28/22.79 % TRYING [6]
% 158.28/22.79 % TRYING [4]
% 158.28/22.79 % (1000213)Instruction limit reached!
% 158.28/22.79 % (1000213)------------------------------
% 158.28/22.79 % (1000213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 158.28/22.79 % (1000213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.28/22.79 % (1000213)CaDiCaL version: 2.1.3
% 158.28/22.79 % (1000213)Termination reason: Instruction limit
% 158.28/22.79 % (1000213)Termination phase: Saturation
% 158.28/22.79 % (1000213)Time elapsed: 0.891 s
% 158.28/22.79 % (1000213)Peak memory usage: 22 MB
% 158.28/22.79 % (1000213)Instructions burned: 1180 (million)
% 158.28/22.79 % (1000381)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3212178103:fmbsr=1.7:i=920_2986 on theBenchmark for (2986ds/920Mi)
% 158.28/22.79 % (1000229)Instruction limit reached!
% 158.28/22.79 % (1000229)------------------------------
% 158.28/22.79 % (1000229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 158.28/22.79 % (1000229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.28/22.79 % (1000229)CaDiCaL version: 2.1.3
% 158.28/22.79 % (1000229)Termination reason: Instruction limit
% 158.28/22.79 % (1000229)Termination phase: Saturation
% 158.28/22.79 % (1000229)Time elapsed: 0.711 s
% 158.28/22.79 % (1000229)Peak memory usage: 18 MB
% 158.28/22.79 % (1000229)Instructions burned: 879 (million)
% 158.28/22.79 % TRYING [8]
% 158.28/22.79 % (1000392)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=394563419:i=5131_2986 on theBenchmark for (2986ds/5131Mi)
% 158.28/22.79 % (1000381)Instruction limit reached!
% 158.28/22.79 % (1000381)------------------------------
% 158.28/22.79 % (1000381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 158.28/22.79 % (1000381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.28/22.79 % (1000381)CaDiCaL version: 2.1.3
% 158.28/22.79 % (1000381)Termination reason: Instruction limit
% 158.28/22.79 % (1000381)Termination phase: Finite model building constraint generation
% 158.28/22.79 % (1000381)Time elapsed: 0.620 s
% 158.28/22.79 % (1000381)Peak memory usage: 70 MB
% 158.28/22.79 % (1000381)Instructions burned: 927 (million)
% 158.28/22.79 % (1000464)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=715160694:i=1472:ins=7:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/1472Mi)
% 158.28/22.79 % TRYING [5]
% 158.28/22.79 % (1000464)Instruction limit reached!
% 158.28/22.79 % (1000464)------------------------------
% 158.28/22.79 % (1000464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 158.28/22.79 % (1000464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.28/22.79 % (1000464)CaDiCaL version: 2.1.3
% 158.28/22.79 % (1000464)Termination reason: Instruction limit
% 158.28/22.79 % (1000464)Termination phase: Saturation
% 158.28/22.79 % (1000464)Time elapsed: 1.276 s
% 158.28/22.79 % (1000464)Peak memory usage: 28 MB
% 158.28/22.79 % (1000464)Instructions burned: 1472 (million)
% 158.28/22.79 % (1000572)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=231252950:i=6324_2967 on theBenchmark for (2967ds/6324Mi)
% 158.28/22.79 % (1000572)Cannot represent all propositional literals internally
% 136.53/37.65 % (1000572)Refutation not found, incomplete strategy
% 136.53/37.65 % (1000572)------------------------------
% 136.53/37.65 % (1000572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000572)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000572)Termination reason: Refutation not found, incomplete strategy
% 136.53/37.65 % (1000572)Time elapsed: 0.004 s
% 136.53/37.65 % (1000572)Peak memory usage: 10 MB
% 136.53/37.65 % (1000572)Instructions burned: 4 (million)
% 136.53/37.65 % (1000572)------------------------------
% 136.53/37.65 % (1000572)------------------------------
% 136.53/37.65 % (1000577)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4186979999:fmbsr=2.30978:i=2174_2966 on theBenchmark for (2966ds/2174Mi)
% 136.53/37.65 % TRYING [16]
% 136.53/37.65 % (1000577)Instruction limit reached!
% 136.53/37.65 % (1000577)------------------------------
% 136.53/37.65 % (1000577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000577)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000577)Termination reason: Instruction limit
% 136.53/37.65 % (1000577)Termination phase: Finite model building constraint generation
% 136.53/37.65 % (1000577)Time elapsed: 1.408 s
% 136.53/37.65 % (1000577)Peak memory usage: 131 MB
% 136.53/37.65 % (1000577)Instructions burned: 2175 (million)
% 136.53/37.65 % (1000643)ott-2_1_sil=16000:newcnf=on:random_seed=3631745697:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2951 on theBenchmark for (2951ds/869Mi)
% 136.53/37.65 % (1000643)Instruction limit reached!
% 136.53/37.65 % (1000643)------------------------------
% 136.53/37.65 % (1000643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000643)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000643)Termination reason: Instruction limit
% 136.53/37.65 % (1000643)Termination phase: Saturation
% 136.53/37.65 % (1000643)Time elapsed: 0.871 s
% 136.53/37.65 % (1000643)Peak memory usage: 19 MB
% 136.53/37.65 % (1000643)Instructions burned: 869 (million)
% 136.53/37.65 % (1000658)ott+10_1_sil=32000:tgt=ground:random_seed=3636546813:i=5114:av=off_2942 on theBenchmark for (2942ds/5114Mi)
% 136.53/37.65 % (1000392)Instruction limit reached!
% 136.53/37.65 % (1000392)------------------------------
% 136.53/37.65 % (1000392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000392)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000392)Termination reason: Instruction limit
% 136.53/37.65 % (1000392)Termination phase: Saturation
% 136.53/37.65 % (1000392)Time elapsed: 4.403 s
% 136.53/37.65 % (1000392)Peak memory usage: 44 MB
% 136.53/37.65 % (1000392)Instructions burned: 5132 (million)
% 136.53/37.65 % (1000666)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3758161546:i=54282_2941 on theBenchmark for (2941ds/54282Mi)
% 136.53/37.65 % TRYING [1]
% 136.53/37.65 % TRYING [2]
% 136.53/37.65 % TRYING [3]
% 136.53/37.65 % TRYING [4]
% 136.53/37.65 % TRYING [5]
% 136.53/37.65 % TRYING [7]
% 136.53/37.65 % TRYING [6]
% 136.53/37.65 % (1000342)Instruction limit reached!
% 136.53/37.65 % (1000342)------------------------------
% 136.53/37.65 % (1000342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000342)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000342)Termination reason: Instruction limit
% 136.53/37.65 % (1000342)Termination phase: Finite model building constraint generation
% 136.53/37.65 % (1000342)Time elapsed: 6.359 s
% 136.53/37.65 % (1000342)Peak memory usage: 575 MB
% 136.53/37.65 % (1000342)Instructions burned: 9516 (million)
% 136.53/37.65 % (1000742)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3217191248:i=3512:aac=none_2923 on theBenchmark for (2923ds/3512Mi)
% 136.53/37.65 % TRYING [6]
% 136.53/37.65 % (1000658)Instruction limit reached!
% 136.53/37.65 % (1000658)------------------------------
% 136.53/37.65 % (1000658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000658)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000658)Termination reason: Instruction limit
% 136.53/37.65 % (1000658)Termination phase: Saturation
% 136.53/37.65 % (1000658)Time elapsed: 4.362 s
% 136.53/37.65 % (1000658)Peak memory usage: 53 MB
% 136.53/37.65 % (1000658)Instructions burned: 5116 (million)
% 136.53/37.65 % (1000816)dis+21_1_sil=32000:sas=cadical:random_seed=2083040541:i=3773:amm=off_2898 on theBenchmark for (2898ds/3773Mi)
% 136.53/37.65 % (1000742)Instruction limit reached!
% 136.53/37.65 % (1000742)------------------------------
% 136.53/37.65 % (1000742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000742)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000742)Termination reason: Instruction limit
% 136.53/37.65 % (1000742)Termination phase: Saturation
% 136.53/37.65 % (1000742)Time elapsed: 3.040 s
% 136.53/37.65 % (1000742)Peak memory usage: 42 MB
% 136.53/37.65 % (1000742)Instructions burned: 3512 (million)
% 136.53/37.65 % (1000832)ott+11_1_sil=16000:gs=on:random_seed=1534331951:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2892 on theBenchmark for (2892ds/2251Mi)
% 136.53/37.65 % (1000832)Instruction limit reached!
% 136.53/37.65 % (1000832)------------------------------
% 136.53/37.65 % (1000832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000832)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000832)Termination reason: Instruction limit
% 136.53/37.65 % (1000832)Termination phase: Saturation
% 136.53/37.65 % (1000832)Time elapsed: 2.099 s
% 136.53/37.65 % (1000832)Peak memory usage: 28 MB
% 136.53/37.65 % (1000832)Instructions burned: 2251 (million)
% 136.53/37.65 % (1000843)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2283850023:fmbsr=1.6:i=67534_2871 on theBenchmark for (2871ds/67534Mi)
% 136.53/37.65 % TRYING [7]
% 136.53/37.65 % TRYING [7]
% 136.53/37.65 % (1000816)Instruction limit reached!
% 136.53/37.65 % (1000816)------------------------------
% 136.53/37.65 % (1000816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000816)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000816)Termination reason: Instruction limit
% 136.53/37.65 % (1000816)Termination phase: Saturation
% 136.53/37.65 % (1000816)Time elapsed: 3.473 s
% 136.53/37.65 % (1000816)Peak memory usage: 39 MB
% 136.53/37.65 % (1000816)Instructions burned: 3774 (million)
% 136.53/37.65 % (1000864)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2645944315:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2863 on theBenchmark for (2863ds/4591Mi)
% 136.53/37.65 % (1000864)Instruction limit reached!
% 136.53/37.65 % (1000864)------------------------------
% 136.53/37.65 % (1000864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000864)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000864)Termination reason: Instruction limit
% 136.53/37.65 % (1000864)Termination phase: Saturation
% 136.53/37.65 % (1000864)Time elapsed: 3.697 s
% 136.53/37.65 % (1000864)Peak memory usage: 40 MB
% 136.53/37.65 % (1000864)Instructions burned: 4592 (million)
% 136.53/37.65 % (1000341)Instruction limit reached!
% 136.53/37.65 % (1000341)------------------------------
% 136.53/37.65 % (1000341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000341)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000341)Termination reason: Instruction limit
% 136.53/37.65 % (1000341)Termination phase: Finite model building SAT solving
% 136.53/37.65 % (1000341)Time elapsed: 16.254 s
% 136.53/37.65 % (1000341)Peak memory usage: 373 MB
% 136.53/37.65 % (1000341)Instructions burned: 22062 (million)
% 136.53/37.65 % (1000882)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1551533564:i=29340_2826 on theBenchmark for (2826ds/29340Mi)
% 136.53/37.65 % (1000884)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3657000077:i=5211_2825 on theBenchmark for (2825ds/5211Mi)
% 136.53/37.65 % TRYING [8]
% 136.53/37.65 % (1000884)Instruction limit reached!
% 136.53/37.65 % (1000884)------------------------------
% 136.53/37.65 % (1000884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000884)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000884)Termination reason: Instruction limit
% 136.53/37.65 % (1000884)Termination phase: Saturation
% 136.53/37.65 % (1000884)Time elapsed: 4.828 s
% 136.53/37.65 % (1000884)Peak memory usage: 47 MB
% 136.53/37.65 % (1000884)Instructions burned: 5211 (million)
% 136.53/37.65 % (1000898)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1326077911:i=5497:nm=2_2776 on theBenchmark for (2776ds/5497Mi)
% 136.53/37.65 % TRYING [17]
% 136.53/37.65 % (1000898)Instruction limit reached!
% 136.53/37.65 % (1000898)------------------------------
% 136.53/37.65 % (1000898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000898)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000898)Termination reason: Instruction limit
% 136.53/37.65 % (1000898)Termination phase: Finite model building constraint generation
% 136.53/37.65 % (1000898)Time elapsed: 3.982 s
% 136.53/37.65 % (1000898)Peak memory usage: 343 MB
% 136.53/37.65 % (1000898)Instructions burned: 5498 (million)
% 136.53/37.65 % (1000900)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1448153242:fmbsr=2:i=46332_2735 on theBenchmark for (2735ds/46332Mi)
% 136.53/37.65 % TRYING [15]
% 136.53/37.65 % TRYING [8]
% 136.53/37.65 % (1000098)Instruction limit reached!
% 136.53/37.65 % (1000098)------------------------------
% 136.53/37.65 % (1000098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000098)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000098)Termination reason: Instruction limit
% 136.53/37.65 % (1000098)Termination phase: Saturation
% 136.53/37.65 % (1000098)Time elapsed: 29.036 s
% 136.53/37.65 % (1000098)Peak memory usage: 253 MB
% 136.53/37.65 % (1000098)Instructions burned: 88025 (million)
% 136.53/37.65 % (1000924)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=233131190:i=14071_2708 on theBenchmark for (2708ds/14071Mi)
% 136.53/37.65 % TRYING [12]
% 136.53/37.65 % (1000924)Instruction limit reached!
% 136.53/37.65 % (1000924)------------------------------
% 136.53/37.65 % (1000924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000924)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000924)Termination reason: Instruction limit
% 136.53/37.65 % (1000924)Termination phase: Finite model building constraint generation
% 136.53/37.65 % (1000924)Time elapsed: 5.622 s
% 136.53/37.65 % (1000924)Peak memory usage: 989 MB
% 136.53/37.65 % (1000924)Instructions burned: 14073 (million)
% 136.53/37.65 % (1000986)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2728448048:i=22565:add=on:rawr=on_2651 on theBenchmark for (2651ds/22565Mi)
% 136.53/37.65 % (1000097) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1000091-1000097"...
% 136.53/37.65 % (1000097)...printing done.
% 136.53/37.65 % (1000097)Refutation found. Thanks to Tanya!
% 136.53/37.65 % SZS status Unsatisfiable for theBenchmark
% 136.53/37.65 % SZS output start Proof for theBenchmark
% See solution above
% 136.53/37.65 % (1000097)------------------------------
% 136.53/37.65 % (1000097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.53/37.65 % (1000097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.53/37.65 % (1000097)CaDiCaL version: 2.1.3
% 136.53/37.65 % (1000097)Termination reason: Refutation
% 136.53/37.65 % (1000097)Time elapsed: 36.763 s
% 136.53/37.65 % (1000097)Peak memory usage: 249 MB
% 136.53/37.65 % (1000097)Instructions burned: 40850 (million)
% 136.53/37.65 % (1000091)Success in time 37.228 s
% 136.53/37.65 % Vampire exiting
%------------------------------------------------------------------------------