%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GEO292+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:54:22 AM UTC 2026
% Result : ContradictoryAxioms 107.69s 33.25s
% Output : Refutation 107.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 24
% Syntax : Number of formulae : 200 ( 68 unt; 6 def)
% Number of atoms : 1286 ( 426 equ)
% Maximal formula atoms : 26 ( 6 avg)
% Number of connectives : 1737 ( 651 ~; 902 |; 162 &)
% ( 14 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 41 ( 9 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 7 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 18 con; 0-3 aty)
% Number of variables : 449 ( 0 sgn 403 !; 46 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
rline(vd1197),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(269, 0)') ).
fof(f12,axiom,
( ~ ? [X0] :
( rline(X0)
& ron(vd1185,X0)
& ron(vd1187,X0)
& ron(vd1186,X0) )
& vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187)
& vd1179 != vd1180
& ? [X4] :
( vd1180 = X4
& rpoint(X4) )
& vf(vd1178,vd1179) = vf(vd1185,vd1186)
& vd1178 != vd1180
& vf(vd1178,vd1180) = vf(vd1185,vd1187)
& ? [X1] :
( vd1187 = X1
& rpoint(X1) )
& ? [X2] :
( rpoint(X2)
& vd1186 = X2 )
& vd1178 != vd1179
& ? [X5] :
( vd1179 = X5
& rpoint(X5) )
& ? [X3] :
( rpoint(X3)
& vd1185 = X3 )
& ? [X6] :
( rpoint(X6)
& vd1178 = X6 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))') ).
fof(f15,axiom,
~ rR(vd1186,vd1199,vd1185),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','neg(neg(conjunct2(conjunct2(comma_conjunct2(plural(271))))))') ).
fof(f17,axiom,
vd1200 = vd1186,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(conjunct1(comma_conjunct2(plural(271))), 1212, 0)') ).
fof(f24,axiom,
? [X0] :
( vd1200 = X0
& rpoint(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qe(s2(plural(271)))') ).
fof(f25,axiom,
? [X0] :
( rpoint(X0)
& vd1199 = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qe(s1(plural(271)))') ).
fof(f28,axiom,
ron(vd1187,vd1232),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(s2(plural(293)), 0)') ).
fof(f29,axiom,
ron(vd1185,vd1232),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(s1(plural(293)), 0)') ).
fof(f30,axiom,
rline(vd1232),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(293, 0)') ).
fof(f31,axiom,
ron(vd1185,vd1197),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(s3(plural(274)), 0)') ).
fof(f35,axiom,
! [X1,X0] :
( ( ? [X3] :
( X0 = X3
& rpoint(X3) )
& ? [X2] :
( X1 = X2
& rpoint(X2) ) )
=> ( vf(X0,X1) = v0
<=> X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))') ).
fof(f38,axiom,
vd1199 = vd1185,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(291, 1230, 0)') ).
fof(f43,axiom,
ron(vd1200,vd1197),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(s2(plural(274)), 0)') ).
fof(f47,axiom,
~ ron(vd1187,vd1197),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','neg(neg(270))') ).
fof(f48,axiom,
! [X0,X3,X2,X7,X4,X1,X5,X6] :
( ( X2 = X3
& X6 = X7
& X4 = X5
& ron(X0,X6)
& rpoint(X3)
& X0 != X4
& rpoint(X5)
& ron(X2,X6)
& X0 = X1
& X0 != X2
& rline(X7)
& rpoint(X1) )
=> ( vangle(X2,X0,X4) = v0
<=> ( ~ rR(X0,X2,X4)
& ron(X4,X6) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(188), 0), imp(cond(axiom(188), 0)))') ).
fof(f59,axiom,
v0 = vd684,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(axiom(137), 2)') ).
fof(f64,axiom,
! [X3,X4,X1,X2,X0,X5,X6] :
( ( ron(X3,X5)
& ? [X11] :
( rpoint(X11)
& X2 = X11 )
& ron(X0,X5)
& ~ rR(X0,X2,X4)
& ~ rR(X0,X1,X3)
& X2 != X0
& ? [X12] :
( rpoint(X12)
& X1 = X12 )
& ron(X1,X5)
& X1 != X0
& ? [X13] :
( rpoint(X13)
& X0 = X13 )
& ? [X8] :
( X5 = X8
& rline(X8) )
& ? [X7] :
( X6 = X7
& rline(X7) )
& ? [X9] :
( X4 = X9
& rpoint(X9) )
& ron(X4,X6)
& ? [X10] :
( X3 = X10
& rpoint(X10) )
& X4 != X0
& X3 != X0
& ron(X2,X6) )
=> vangle(X1,X0,X2) = vangle(X3,X0,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(194), 0), imp(cond(axiom(194), 0)))') ).
fof(f99,axiom,
! [X2,X0,X3,X4,X1] :
( ( ? [X7] :
( X0 = X7
& rpoint(X7) )
& X3 = X4
& rR(X1,X0,X2)
& ron(X2,X3)
& ? [X5] :
( rpoint(X5)
& X2 = X5 )
& rline(X4)
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ron(X0,X3) )
=> ron(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(85), 0), imp(cond(axiom(85), 0)))') ).
fof(f152,plain,
! [X6,X1,X4,X2,X5,X0,X3] :
( ( ron(X1,X6)
& ron(X2,X5)
& ~ rR(X4,X3,X1)
& ? [X7] :
( X3 = X7
& rpoint(X7) )
& ron(X4,X5)
& X2 != X4
& ? [X9] :
( X4 = X9
& rpoint(X9) )
& X3 != X4
& ? [X8] :
( X2 = X8
& rpoint(X8) )
& X1 != X4
& X0 != X4
& ron(X3,X6)
& ? [X13] :
( X0 = X13
& rpoint(X13) )
& ? [X10] :
( rline(X10)
& X5 = X10 )
& ron(X0,X5)
& ~ rR(X4,X2,X0)
& ? [X11] :
( X6 = X11
& rline(X11) )
& ? [X12] :
( rpoint(X12)
& X1 = X12 ) )
=> vangle(X2,X4,X3) = vangle(X0,X4,X1) ),
inference(rectify,[],[f64]) ).
fof(f169,plain,
! [X1,X0] :
( ( ? [X2] :
( rpoint(X2)
& X1 = X2 )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ( v0 = vf(X1,X0)
<=> X0 = X1 ) ),
inference(rectify,[],[f35]) ).
fof(f206,plain,
! [X3,X0,X6,X7,X5,X1,X4,X2] :
( ( rpoint(X1)
& X4 = X6
& rpoint(X6)
& X0 != X2
& X0 != X4
& X3 = X7
& rpoint(X5)
& X0 = X5
& X1 = X2
& rline(X3)
& ron(X0,X7)
& ron(X2,X7) )
=> ( vangle(X2,X0,X4) = v0
<=> ( ron(X4,X7)
& ~ rR(X0,X2,X4) ) ) ),
inference(rectify,[],[f48]) ).
fof(f212,plain,
( ~ ? [X0] :
( rline(X0)
& ron(vd1185,X0)
& ron(vd1187,X0)
& ron(vd1186,X0) )
& vf(vd1178,vd1180) = vf(vd1185,vd1187)
& vf(vd1178,vd1179) = vf(vd1185,vd1186)
& ? [X6] :
( rpoint(X6)
& vd1178 = X6 )
& ? [X5] :
( vd1185 = X5
& rpoint(X5) )
& ? [X3] :
( rpoint(X3)
& vd1186 = X3 )
& ? [X1] :
( rpoint(X1)
& vd1180 = X1 )
& ? [X2] :
( rpoint(X2)
& vd1187 = X2 )
& vd1179 != vd1180
& vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187)
& vd1178 != vd1180
& ? [X4] :
( rpoint(X4)
& vd1179 = X4 )
& vd1178 != vd1179 ),
inference(rectify,[],[f12]) ).
fof(f242,plain,
! [X0,X1,X4,X3,X2] :
( ( ? [X7] :
( X4 = X7
& rpoint(X7) )
& X2 = X3
& ? [X6] :
( X0 = X6
& rpoint(X6) )
& ron(X0,X2)
& ron(X1,X2)
& ? [X5] :
( rpoint(X5)
& X1 = X5 )
& rline(X3)
& rR(X4,X1,X0) )
=> ron(X4,X2) ),
inference(rectify,[],[f99]) ).
fof(f291,plain,
! [X6,X1,X4,X2,X5,X0,X3] :
( vangle(X2,X4,X3) = vangle(X0,X4,X1)
| ~ ron(X1,X6)
| ~ ron(X2,X5)
| rR(X4,X3,X1)
| ! [X7] :
( X3 != X7
| ~ rpoint(X7) )
| ~ ron(X4,X5)
| X2 = X4
| ! [X9] :
( X4 != X9
| ~ rpoint(X9) )
| X3 = X4
| ! [X8] :
( X2 != X8
| ~ rpoint(X8) )
| X1 = X4
| X0 = X4
| ~ ron(X3,X6)
| ! [X13] :
( X0 != X13
| ~ rpoint(X13) )
| ! [X10] :
( ~ rline(X10)
| X5 != X10 )
| ~ ron(X0,X5)
| rR(X4,X2,X0)
| ! [X11] :
( X6 != X11
| ~ rline(X11) )
| ! [X12] :
( X1 != X12
| ~ rpoint(X12) ) ),
inference(ennf_transformation,[],[f152]) ).
fof(f292,plain,
! [X4,X5,X6,X0,X3,X2,X1] :
( rR(X4,X3,X1)
| ~ ron(X4,X5)
| ! [X8] :
( X2 != X8
| ~ rpoint(X8) )
| ! [X11] :
( X6 != X11
| ~ rline(X11) )
| ~ ron(X1,X6)
| ! [X9] :
( X4 != X9
| ~ rpoint(X9) )
| ! [X12] :
( X1 != X12
| ~ rpoint(X12) )
| ! [X13] :
( X0 != X13
| ~ rpoint(X13) )
| ! [X7] :
( X3 != X7
| ~ rpoint(X7) )
| X3 = X4
| ~ ron(X2,X5)
| rR(X4,X2,X0)
| X2 = X4
| X1 = X4
| X0 = X4
| ! [X10] :
( ~ rline(X10)
| X5 != X10 )
| ~ ron(X3,X6)
| vangle(X2,X4,X3) = vangle(X0,X4,X1)
| ~ ron(X0,X5) ),
inference(flattening,[],[f291]) ).
fof(f293,plain,
! [X1,X0] :
( ( v0 = vf(X1,X0)
<=> X0 = X1 )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( ~ rpoint(X3)
| X0 != X3 ) ),
inference(ennf_transformation,[],[f169]) ).
fof(f294,plain,
! [X0,X1] :
( ( v0 = vf(X1,X0)
<=> X0 = X1 )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( ~ rpoint(X3)
| X0 != X3 ) ),
inference(flattening,[],[f293]) ).
fof(f307,plain,
( ? [X3] :
( rpoint(X3)
& vd1186 = X3 )
& ! [X0] :
( ~ ron(vd1185,X0)
| ~ rline(X0)
| ~ ron(vd1187,X0)
| ~ ron(vd1186,X0) )
& vf(vd1178,vd1180) = vf(vd1185,vd1187)
& ? [X4] :
( rpoint(X4)
& vd1179 = X4 )
& ? [X5] :
( vd1185 = X5
& rpoint(X5) )
& vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187)
& vd1178 != vd1180
& ? [X2] :
( rpoint(X2)
& vd1187 = X2 )
& ? [X6] :
( rpoint(X6)
& vd1178 = X6 )
& vd1179 != vd1180
& vd1178 != vd1179
& vf(vd1178,vd1179) = vf(vd1185,vd1186)
& ? [X1] :
( rpoint(X1)
& vd1180 = X1 ) ),
inference(ennf_transformation,[],[f212]) ).
fof(f318,plain,
! [X3,X0,X6,X7,X5,X1,X4,X2] :
( ( vangle(X2,X0,X4) = v0
<=> ( ron(X4,X7)
& ~ rR(X0,X2,X4) ) )
| ~ rpoint(X1)
| X4 != X6
| ~ rpoint(X6)
| X0 = X2
| X0 = X4
| X3 != X7
| ~ rpoint(X5)
| X0 != X5
| X1 != X2
| ~ rline(X3)
| ~ ron(X0,X7)
| ~ ron(X2,X7) ),
inference(ennf_transformation,[],[f206]) ).
fof(f319,plain,
! [X6,X5,X7,X2,X3,X4,X1,X0] :
( X4 != X6
| X0 = X2
| ( vangle(X2,X0,X4) = v0
<=> ( ron(X4,X7)
& ~ rR(X0,X2,X4) ) )
| ~ rline(X3)
| X0 != X5
| ~ ron(X2,X7)
| ~ ron(X0,X7)
| ~ rpoint(X1)
| X1 != X2
| ~ rpoint(X6)
| X3 != X7
| ~ rpoint(X5)
| X0 = X4 ),
inference(flattening,[],[f318]) ).
fof(f370,plain,
! [X0,X1,X4,X3,X2] :
( ron(X4,X2)
| ! [X7] :
( ~ rpoint(X7)
| X4 != X7 )
| X2 != X3
| ! [X6] :
( X0 != X6
| ~ rpoint(X6) )
| ~ ron(X0,X2)
| ~ ron(X1,X2)
| ! [X5] :
( X1 != X5
| ~ rpoint(X5) )
| ~ rline(X3)
| ~ rR(X4,X1,X0) ),
inference(ennf_transformation,[],[f242]) ).
fof(f371,plain,
! [X0,X4,X2,X1,X3] :
( ron(X4,X2)
| ~ rR(X4,X1,X0)
| ~ ron(X1,X2)
| X2 != X3
| ! [X5] :
( X1 != X5
| ~ rpoint(X5) )
| ! [X7] :
( ~ rpoint(X7)
| X4 != X7 )
| ! [X6] :
( X0 != X6
| ~ rpoint(X6) )
| ~ ron(X0,X2)
| ~ rline(X3) ),
inference(flattening,[],[f370]) ).
fof(f481,plain,
vd1199 = sK5,
inference(cnf_transformation,[],[f25]) ).
fof(f492,plain,
v0 = vd684,
inference(cnf_transformation,[],[f59]) ).
fof(f500,plain,
vd1186 = vd1200,
inference(cnf_transformation,[],[f17]) ).
fof(f507,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ ron(X0,X5)
| vangle(X2,X4,X3) = vangle(X0,X4,X1)
| ~ ron(X3,X6)
| X5 != X10
| ~ rline(X10)
| X0 = X4
| X1 = X4
| X2 = X4
| rR(X4,X2,X0)
| ~ ron(X2,X5)
| X3 = X4
| ~ rpoint(X7)
| X3 != X7
| ~ rpoint(X13)
| X0 != X13
| ~ rpoint(X12)
| X1 != X12
| ~ rpoint(X9)
| X4 != X9
| ~ ron(X1,X6)
| ~ rline(X11)
| X6 != X11
| ~ rpoint(X8)
| X2 != X8
| ~ ron(X4,X5)
| rR(X4,X3,X1) ),
inference(cnf_transformation,[],[f292]) ).
fof(f515,plain,
ron(vd1185,vd1232),
inference(cnf_transformation,[],[f29]) ).
fof(f531,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rline(X3)
| ~ ron(X0,X2)
| ~ rpoint(X6)
| X0 != X6
| X4 != X7
| ~ rpoint(X7)
| ~ rpoint(X5)
| X1 != X5
| X2 != X3
| ~ ron(X1,X2)
| ~ rR(X4,X1,X0)
| ron(X4,X2) ),
inference(cnf_transformation,[],[f371]) ).
fof(f545,plain,
ron(vd1187,vd1232),
inference(cnf_transformation,[],[f28]) ).
fof(f546,plain,
ron(vd1185,vd1197),
inference(cnf_transformation,[],[f31]) ).
fof(f548,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( X0 = X4
| ~ rpoint(X5)
| X3 != X7
| ~ rpoint(X6)
| X1 != X2
| ~ rpoint(X1)
| ~ ron(X0,X7)
| ~ ron(X2,X7)
| X0 != X5
| ~ rline(X3)
| ron(X4,X7)
| v0 != vangle(X2,X0,X4)
| X0 = X2
| X4 != X6 ),
inference(cnf_transformation,[],[f319]) ).
fof(f549,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( X0 = X4
| ~ rpoint(X5)
| X3 != X7
| ~ rpoint(X6)
| X1 != X2
| ~ rpoint(X1)
| ~ ron(X0,X7)
| ~ ron(X2,X7)
| X0 != X5
| ~ rline(X3)
| rR(X0,X2,X4)
| ~ ron(X4,X7)
| v0 = vangle(X2,X0,X4)
| X0 = X2
| X4 != X6 ),
inference(cnf_transformation,[],[f319]) ).
fof(f557,plain,
rline(vd1232),
inference(cnf_transformation,[],[f30]) ).
fof(f558,plain,
rpoint(sK17),
inference(cnf_transformation,[],[f24]) ).
fof(f559,plain,
vd1200 = sK17,
inference(cnf_transformation,[],[f24]) ).
fof(f580,plain,
~ ron(vd1187,vd1197),
inference(cnf_transformation,[],[f47]) ).
fof(f646,plain,
rline(vd1197),
inference(cnf_transformation,[],[f11]) ).
fof(f651,plain,
! [X2,X3,X0,X1] :
( X0 != X3
| ~ rpoint(X3)
| ~ rpoint(X2)
| X1 != X2
| X0 != X1
| v0 = vf(X1,X0) ),
inference(cnf_transformation,[],[f294]) ).
fof(f652,plain,
! [X2,X3,X0,X1] :
( X0 != X3
| ~ rpoint(X3)
| ~ rpoint(X2)
| X1 != X2
| X0 = X1
| v0 != vf(X1,X0) ),
inference(cnf_transformation,[],[f294]) ).
fof(f653,plain,
ron(vd1200,vd1197),
inference(cnf_transformation,[],[f43]) ).
fof(f670,plain,
! [X0] :
( ~ ron(vd1186,X0)
| ~ ron(vd1187,X0)
| ~ rline(X0)
| ~ ron(vd1185,X0) ),
inference(cnf_transformation,[],[f307]) ).
fof(f671,plain,
vd1179 = sK41,
inference(cnf_transformation,[],[f307]) ).
fof(f672,plain,
rpoint(sK41),
inference(cnf_transformation,[],[f307]) ).
fof(f673,plain,
rpoint(sK40),
inference(cnf_transformation,[],[f307]) ).
fof(f674,plain,
vd1185 = sK40,
inference(cnf_transformation,[],[f307]) ).
fof(f675,plain,
vd1187 = sK39,
inference(cnf_transformation,[],[f307]) ).
fof(f676,plain,
rpoint(sK39),
inference(cnf_transformation,[],[f307]) ).
fof(f677,plain,
vd1178 = sK38,
inference(cnf_transformation,[],[f307]) ).
fof(f678,plain,
rpoint(sK38),
inference(cnf_transformation,[],[f307]) ).
fof(f681,plain,
vf(vd1178,vd1179) = vf(vd1185,vd1186),
inference(cnf_transformation,[],[f307]) ).
fof(f682,plain,
vd1179 != vd1178,
inference(cnf_transformation,[],[f307]) ).
fof(f746,plain,
vd1185 = vd1199,
inference(cnf_transformation,[],[f38]) ).
fof(f777,plain,
~ rR(vd1186,vd1199,vd1185),
inference(cnf_transformation,[],[f15]) ).
fof(f782,plain,
vd1186 = sK17,
inference(definition_unfolding,[],[f500,f559]) ).
fof(f789,plain,
ron(sK40,vd1232),
inference(definition_unfolding,[],[f515,f674]) ).
fof(f793,plain,
ron(sK39,vd1232),
inference(definition_unfolding,[],[f545,f675]) ).
fof(f794,plain,
ron(sK40,vd1197),
inference(definition_unfolding,[],[f546,f674]) ).
fof(f795,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( X0 = X4
| ~ rpoint(X5)
| X3 != X7
| ~ rpoint(X6)
| X1 != X2
| ~ rpoint(X1)
| ~ ron(X0,X7)
| ~ ron(X2,X7)
| X0 != X5
| ~ rline(X3)
| rR(X0,X2,X4)
| ~ ron(X4,X7)
| vangle(X2,X0,X4) = vd684
| X0 = X2
| X4 != X6 ),
inference(definition_unfolding,[],[f549,f492]) ).
fof(f796,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( X0 = X4
| ~ rpoint(X5)
| X3 != X7
| ~ rpoint(X6)
| X1 != X2
| ~ rpoint(X1)
| ~ ron(X0,X7)
| ~ ron(X2,X7)
| X0 != X5
| ~ rline(X3)
| ron(X4,X7)
| vangle(X2,X0,X4) != vd684
| X0 = X2
| X4 != X6 ),
inference(definition_unfolding,[],[f548,f492]) ).
fof(f799,plain,
~ ron(sK39,vd1197),
inference(definition_unfolding,[],[f580,f675]) ).
fof(f811,plain,
! [X2,X3,X0,X1] :
( X0 != X3
| ~ rpoint(X3)
| ~ rpoint(X2)
| X1 != X2
| X0 = X1
| vf(X1,X0) != vd684 ),
inference(definition_unfolding,[],[f652,f492]) ).
fof(f812,plain,
! [X2,X3,X0,X1] :
( X0 != X3
| ~ rpoint(X3)
| ~ rpoint(X2)
| X1 != X2
| X0 != X1
| vf(X1,X0) = vd684 ),
inference(definition_unfolding,[],[f651,f492]) ).
fof(f813,plain,
ron(sK17,vd1197),
inference(definition_unfolding,[],[f653,f559]) ).
fof(f820,plain,
sK38 != sK41,
inference(definition_unfolding,[],[f682,f671,f677]) ).
fof(f821,plain,
vf(sK40,sK17) = vf(sK38,sK41),
inference(definition_unfolding,[],[f681,f677,f671,f674,f782]) ).
fof(f822,plain,
! [X0] :
( ~ ron(sK17,X0)
| ~ rline(X0)
| ~ ron(sK40,X0)
| ~ ron(sK39,X0) ),
inference(definition_unfolding,[],[f670,f782,f675,f674]) ).
fof(f828,plain,
sK5 = sK40,
inference(definition_unfolding,[],[f746,f674,f481]) ).
fof(f829,plain,
~ rR(sK17,sK5,sK40),
inference(definition_unfolding,[],[f777,f782,f481,f674]) ).
fof(f916,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X12,X13] :
( ~ ron(X0,X10)
| vangle(X2,X4,X3) = vangle(X0,X4,X1)
| ~ ron(X3,X6)
| ~ rline(X10)
| X0 = X4
| X1 = X4
| X2 = X4
| rR(X4,X2,X0)
| ~ ron(X2,X10)
| X3 = X4
| ~ rpoint(X7)
| X3 != X7
| ~ rpoint(X13)
| X0 != X13
| ~ rpoint(X12)
| X1 != X12
| ~ rpoint(X9)
| X4 != X9
| ~ ron(X1,X6)
| ~ rline(X11)
| X6 != X11
| ~ rpoint(X8)
| X2 != X8
| ~ ron(X4,X10)
| rR(X4,X3,X1) ),
inference(equality_resolution,[],[f507]) ).
fof(f917,plain,
! [X2,X10,X0,X11,X1,X8,X6,X9,X7,X4,X12,X13] :
( ~ ron(X0,X10)
| vangle(X0,X4,X1) = vangle(X2,X4,X7)
| ~ ron(X7,X6)
| ~ rline(X10)
| X0 = X4
| X1 = X4
| X2 = X4
| rR(X4,X2,X0)
| ~ ron(X2,X10)
| X4 = X7
| ~ rpoint(X7)
| ~ rpoint(X13)
| X0 != X13
| ~ rpoint(X12)
| X1 != X12
| ~ rpoint(X9)
| X4 != X9
| ~ ron(X1,X6)
| ~ rline(X11)
| X6 != X11
| ~ rpoint(X8)
| X2 != X8
| ~ ron(X4,X10)
| rR(X4,X7,X1) ),
inference(equality_resolution,[],[f916]) ).
fof(f918,plain,
! [X2,X10,X11,X1,X8,X6,X9,X7,X4,X12,X13] :
( ~ ron(X13,X10)
| vangle(X2,X4,X7) = vangle(X13,X4,X1)
| ~ ron(X7,X6)
| ~ rline(X10)
| X4 = X13
| X1 = X4
| X2 = X4
| rR(X4,X2,X13)
| ~ ron(X2,X10)
| X4 = X7
| ~ rpoint(X7)
| ~ rpoint(X13)
| ~ rpoint(X12)
| X1 != X12
| ~ rpoint(X9)
| X4 != X9
| ~ ron(X1,X6)
| ~ rline(X11)
| X6 != X11
| ~ rpoint(X8)
| X2 != X8
| ~ ron(X4,X10)
| rR(X4,X7,X1) ),
inference(equality_resolution,[],[f917]) ).
fof(f919,plain,
! [X2,X10,X11,X8,X6,X9,X7,X4,X12,X13] :
( ~ ron(X13,X10)
| vangle(X2,X4,X7) = vangle(X13,X4,X12)
| ~ ron(X7,X6)
| ~ rline(X10)
| X4 = X13
| X4 = X12
| X2 = X4
| rR(X4,X2,X13)
| ~ ron(X2,X10)
| X4 = X7
| ~ rpoint(X7)
| ~ rpoint(X13)
| ~ rpoint(X12)
| ~ rpoint(X9)
| X4 != X9
| ~ ron(X12,X6)
| ~ rline(X11)
| X6 != X11
| ~ rpoint(X8)
| X2 != X8
| ~ ron(X4,X10)
| rR(X4,X7,X12) ),
inference(equality_resolution,[],[f918]) ).
fof(f920,plain,
! [X2,X10,X11,X8,X6,X9,X7,X12,X13] :
( ~ ron(X13,X10)
| vangle(X2,X9,X7) = vangle(X13,X9,X12)
| ~ ron(X7,X6)
| ~ rline(X10)
| X9 = X13
| X9 = X12
| X2 = X9
| rR(X9,X2,X13)
| ~ ron(X2,X10)
| X7 = X9
| ~ rpoint(X7)
| ~ rpoint(X13)
| ~ rpoint(X12)
| ~ rpoint(X9)
| ~ ron(X12,X6)
| ~ rline(X11)
| X6 != X11
| ~ rpoint(X8)
| X2 != X8
| ~ ron(X9,X10)
| rR(X9,X7,X12) ),
inference(equality_resolution,[],[f919]) ).
fof(f921,plain,
! [X2,X10,X11,X8,X9,X7,X12,X13] :
( ~ ron(X13,X10)
| vangle(X2,X9,X7) = vangle(X13,X9,X12)
| ~ ron(X7,X11)
| ~ rline(X10)
| X9 = X13
| X9 = X12
| X2 = X9
| rR(X9,X2,X13)
| ~ ron(X2,X10)
| X7 = X9
| ~ rpoint(X7)
| ~ rpoint(X13)
| ~ rpoint(X12)
| ~ rpoint(X9)
| ~ ron(X12,X11)
| ~ rline(X11)
| ~ rpoint(X8)
| X2 != X8
| ~ ron(X9,X10)
| rR(X9,X7,X12) ),
inference(equality_resolution,[],[f920]) ).
fof(f922,plain,
! [X10,X11,X8,X9,X7,X12,X13] :
( X9 = X13
| rR(X9,X8,X13)
| X9 = X12
| ~ rline(X10)
| ~ rline(X11)
| ~ ron(X7,X11)
| vangle(X13,X9,X12) = vangle(X8,X9,X7)
| ~ ron(X9,X10)
| X7 = X9
| X8 = X9
| ~ ron(X8,X10)
| ~ rpoint(X7)
| ~ rpoint(X13)
| ~ ron(X13,X10)
| ~ ron(X12,X11)
| ~ rpoint(X12)
| rR(X9,X7,X12)
| ~ rpoint(X8)
| ~ rpoint(X9) ),
inference(equality_resolution,[],[f921]) ).
fof(f993,plain,
! [X2,X3,X1,X6,X7,X4,X5] :
( ~ rline(X3)
| ~ ron(X6,X2)
| ~ rpoint(X6)
| X4 != X7
| ~ rpoint(X7)
| ~ rpoint(X5)
| X1 != X5
| X2 != X3
| ~ ron(X1,X2)
| ~ rR(X4,X1,X6)
| ron(X4,X2) ),
inference(equality_resolution,[],[f531]) ).
fof(f994,plain,
! [X2,X3,X1,X6,X7,X5] :
( ~ rline(X3)
| ~ ron(X6,X2)
| ~ rpoint(X6)
| ~ rpoint(X7)
| ~ rpoint(X5)
| X1 != X5
| X2 != X3
| ~ ron(X1,X2)
| ~ rR(X7,X1,X6)
| ron(X7,X2) ),
inference(equality_resolution,[],[f993]) ).
fof(f995,plain,
! [X2,X3,X6,X7,X5] :
( ~ rline(X3)
| ~ ron(X6,X2)
| ~ rpoint(X6)
| ~ rpoint(X7)
| ~ rpoint(X5)
| X2 != X3
| ~ ron(X5,X2)
| ~ rR(X7,X5,X6)
| ron(X7,X2) ),
inference(equality_resolution,[],[f994]) ).
fof(f996,plain,
! [X3,X6,X7,X5] :
( ~ ron(X6,X3)
| ~ rpoint(X7)
| ~ ron(X5,X3)
| ~ rpoint(X5)
| ~ rline(X3)
| ~ rpoint(X6)
| ron(X7,X3)
| ~ rR(X7,X5,X6) ),
inference(equality_resolution,[],[f995]) ).
fof(f1031,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( X0 = X4
| ~ rpoint(X5)
| ~ rpoint(X6)
| X1 != X2
| ~ rpoint(X1)
| ~ ron(X0,X7)
| ~ ron(X2,X7)
| X0 != X5
| ~ rline(X7)
| rR(X0,X2,X4)
| ~ ron(X4,X7)
| vangle(X2,X0,X4) = vd684
| X0 = X2
| X4 != X6 ),
inference(equality_resolution,[],[f795]) ).
fof(f1032,plain,
! [X2,X0,X6,X7,X4,X5] :
( X0 = X4
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X2)
| ~ ron(X0,X7)
| ~ ron(X2,X7)
| X0 != X5
| ~ rline(X7)
| rR(X0,X2,X4)
| ~ ron(X4,X7)
| vangle(X2,X0,X4) = vd684
| X0 = X2
| X4 != X6 ),
inference(equality_resolution,[],[f1031]) ).
fof(f1033,plain,
! [X2,X6,X7,X4,X5] :
( X4 = X5
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X2)
| ~ ron(X5,X7)
| ~ ron(X2,X7)
| ~ rline(X7)
| rR(X5,X2,X4)
| ~ ron(X4,X7)
| vd684 = vangle(X2,X5,X4)
| X2 = X5
| X4 != X6 ),
inference(equality_resolution,[],[f1032]) ).
fof(f1034,plain,
! [X2,X6,X7,X5] :
( ~ ron(X6,X7)
| ~ rpoint(X5)
| rR(X5,X2,X6)
| ~ ron(X5,X7)
| ~ rpoint(X2)
| X2 = X5
| ~ rpoint(X6)
| ~ rline(X7)
| ~ ron(X2,X7)
| vd684 = vangle(X2,X5,X6)
| X5 = X6 ),
inference(equality_resolution,[],[f1033]) ).
fof(f1035,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( X0 = X4
| ~ rpoint(X5)
| ~ rpoint(X6)
| X1 != X2
| ~ rpoint(X1)
| ~ ron(X0,X7)
| ~ ron(X2,X7)
| X0 != X5
| ~ rline(X7)
| ron(X4,X7)
| vangle(X2,X0,X4) != vd684
| X0 = X2
| X4 != X6 ),
inference(equality_resolution,[],[f796]) ).
fof(f1036,plain,
! [X2,X0,X6,X7,X4,X5] :
( X0 = X4
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X2)
| ~ ron(X0,X7)
| ~ ron(X2,X7)
| X0 != X5
| ~ rline(X7)
| ron(X4,X7)
| vangle(X2,X0,X4) != vd684
| X0 = X2
| X4 != X6 ),
inference(equality_resolution,[],[f1035]) ).
fof(f1037,plain,
! [X2,X6,X7,X4,X5] :
( X4 = X5
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X2)
| ~ ron(X5,X7)
| ~ ron(X2,X7)
| ~ rline(X7)
| ron(X4,X7)
| vd684 != vangle(X2,X5,X4)
| X2 = X5
| X4 != X6 ),
inference(equality_resolution,[],[f1036]) ).
fof(f1038,plain,
! [X2,X6,X7,X5] :
( ~ rline(X7)
| ~ ron(X5,X7)
| ~ rpoint(X6)
| X2 = X5
| vd684 != vangle(X2,X5,X6)
| ron(X6,X7)
| X5 = X6
| ~ rpoint(X2)
| ~ ron(X2,X7)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1037]) ).
fof(f1302,plain,
! [X2,X3,X1] :
( ~ rpoint(X3)
| ~ rpoint(X2)
| X1 != X2
| X1 = X3
| vd684 != vf(X1,X3) ),
inference(equality_resolution,[],[f811]) ).
fof(f1303,plain,
! [X2,X3] :
( vd684 != vf(X2,X3)
| ~ rpoint(X3)
| X2 = X3
| ~ rpoint(X2) ),
inference(equality_resolution,[],[f1302]) ).
fof(f1304,plain,
! [X2,X3,X1] :
( ~ rpoint(X3)
| ~ rpoint(X2)
| X1 != X2
| X1 != X3
| vd684 = vf(X1,X3) ),
inference(equality_resolution,[],[f812]) ).
fof(f1305,plain,
! [X2,X3] :
( ~ rpoint(X3)
| ~ rpoint(X2)
| X2 != X3
| vd684 = vf(X2,X3) ),
inference(equality_resolution,[],[f1304]) ).
fof(f1306,plain,
! [X3] :
( vd684 = vf(X3,X3)
| ~ rpoint(X3)
| ~ rpoint(X3) ),
inference(equality_resolution,[],[f1305]) ).
fof(f1654,plain,
~ rpoint(sK39),
inference(consistent_polarity_flipping,[],[f676]) ).
fof(f1680,plain,
~ rpoint(sK40),
inference(consistent_polarity_flipping,[],[f673]) ).
fof(f1706,plain,
~ rline(vd1197),
inference(consistent_polarity_flipping,[],[f646]) ).
fof(f1717,plain,
! [X3,X6,X7,X5] :
( ~ ron(X5,X3)
| rline(X3)
| ~ ron(X6,X3)
| ron(X7,X3)
| rpoint(X5)
| rpoint(X6)
| rpoint(X7)
| rR(X7,X5,X6) ),
inference(consistent_polarity_flipping,[],[f996]) ).
fof(f1738,plain,
! [X2,X3] :
( vd684 != vf(X2,X3)
| X2 = X3
| rpoint(X3)
| rpoint(X2) ),
inference(consistent_polarity_flipping,[],[f1303]) ).
fof(f1745,plain,
~ rpoint(sK38),
inference(consistent_polarity_flipping,[],[f678]) ).
fof(f1753,plain,
~ rpoint(sK17),
inference(consistent_polarity_flipping,[],[f558]) ).
fof(f1754,plain,
~ rpoint(sK41),
inference(consistent_polarity_flipping,[],[f672]) ).
fof(f1760,plain,
! [X2,X6,X7,X5] :
( ~ rR(X5,X2,X6)
| rline(X7)
| X5 = X6
| ~ ron(X6,X7)
| rpoint(X6)
| vd684 = vangle(X2,X5,X6)
| ~ ron(X2,X7)
| ~ ron(X5,X7)
| rpoint(X5)
| X2 = X5
| rpoint(X2) ),
inference(consistent_polarity_flipping,[],[f1034]) ).
fof(f1787,plain,
! [X10,X11,X8,X9,X7,X12,X13] :
( ~ rR(X9,X8,X13)
| rpoint(X13)
| X9 = X13
| rpoint(X9)
| rpoint(X12)
| X9 = X12
| rpoint(X7)
| ~ ron(X12,X11)
| X7 = X9
| X8 = X9
| ~ ron(X9,X10)
| vangle(X13,X9,X12) = vangle(X8,X9,X7)
| ~ ron(X8,X10)
| ~ rR(X9,X7,X12)
| ~ ron(X13,X10)
| rline(X10)
| ~ ron(X7,X11)
| rline(X11)
| rpoint(X8) ),
inference(consistent_polarity_flipping,[],[f922]) ).
fof(f1815,plain,
~ rline(vd1232),
inference(consistent_polarity_flipping,[],[f557]) ).
fof(f1817,plain,
! [X3] :
( rpoint(X3)
| rpoint(X3)
| vd684 = vf(X3,X3) ),
inference(consistent_polarity_flipping,[],[f1306]) ).
fof(f1850,plain,
! [X0] :
( ~ ron(sK39,X0)
| ~ ron(sK40,X0)
| rline(X0)
| ~ ron(sK17,X0) ),
inference(consistent_polarity_flipping,[],[f822]) ).
fof(f1855,plain,
rR(sK17,sK5,sK40),
inference(consistent_polarity_flipping,[],[f829]) ).
fof(f1858,plain,
! [X2,X6,X7,X5] :
( vd684 != vangle(X2,X5,X6)
| ~ ron(X2,X7)
| rpoint(X5)
| rpoint(X2)
| ~ ron(X5,X7)
| ron(X6,X7)
| X5 = X6
| X2 = X5
| rpoint(X6)
| rline(X7) ),
inference(consistent_polarity_flipping,[],[f1038]) ).
fof(f1899,plain,
! [X3] :
( rpoint(X3)
| vd684 = vf(X3,X3) ),
inference(duplicate_literal_removal,[],[f1817]) ).
fof(f1944,definition,
( spl66_12
<=> sK5 = sK40 ),
introduced(definition,[new_symbols(definition,[spl66_12])],[avatar_definition]) ).
fof(f1946,plain,
( sK5 = sK40
| ~ spl66_12 ),
inference(avatar_component_clause,[],[f1944]) ).
fof(f1964,plain,
spl66_12,
inference(avatar_split_clause,[],[f828,f1944]) ).
fof(f1967,plain,
( rR(sK17,sK40,sK40)
| ~ spl66_12 ),
inference(forward_demodulation,[],[f1855,f1946]) ).
fof(f1982,plain,
vd684 = vf(sK40,sK40),
inference(resolution,[],[f1899,f1680]) ).
fof(f2227,plain,
( ~ ron(sK17,vd1232)
| ~ ron(sK40,vd1232)
| rline(vd1232) ),
inference(resolution,[],[f1850,f793]) ).
fof(f2228,plain,
( ~ ron(sK17,vd1232)
| rline(vd1232) ),
inference(forward_subsumption_resolution,[],[f2227,f789]) ).
fof(f2229,plain,
~ ron(sK17,vd1232),
inference(forward_subsumption_resolution,[],[f2228,f1815]) ).
fof(f2395,plain,
( sK38 = sK41
| rpoint(sK38)
| vd684 != vf(sK40,sK17)
| rpoint(sK41) ),
inference(superposition,[],[f1738,f821]) ).
fof(f2400,plain,
( rpoint(sK41)
| rpoint(sK38)
| vd684 != vf(sK40,sK17) ),
inference(forward_subsumption_resolution,[],[f2395,f820]) ).
fof(f2405,plain,
( rpoint(sK38)
| vd684 != vf(sK40,sK17) ),
inference(forward_subsumption_resolution,[],[f2400,f1754]) ).
fof(f2418,plain,
vd684 != vf(sK40,sK17),
inference(forward_subsumption_resolution,[],[f2405,f1745]) ).
fof(f3236,plain,
! [X0,X1] :
( rpoint(X0)
| ron(X1,vd1232)
| rpoint(sK39)
| rR(X1,sK39,X0)
| rpoint(X1)
| ~ ron(X0,vd1232)
| rline(vd1232) ),
inference(resolution,[],[f1717,f793]) ).
fof(f3268,plain,
! [X0,X1] :
( ~ ron(X0,vd1232)
| rpoint(X1)
| ron(X1,vd1232)
| rline(vd1232)
| rpoint(X0)
| rR(X1,sK39,X0) ),
inference(forward_subsumption_resolution,[],[f3236,f1654]) ).
fof(f3288,plain,
! [X0,X1] :
( rR(X1,sK39,X0)
| rpoint(X0)
| ~ ron(X0,vd1232)
| ron(X1,vd1232)
| rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f3268,f1815]) ).
fof(f4334,definition,
( spl66_18
<=> ! [X0] :
( ~ ron(sK40,X0)
| rline(X0)
| ~ ron(sK17,X0) ) ),
introduced(definition,[new_symbols(definition,[spl66_18])],[avatar_definition]) ).
fof(f4335,plain,
( ! [X0] :
( ~ ron(sK17,X0)
| ~ ron(sK40,X0)
| rline(X0) )
| ~ spl66_18 ),
inference(avatar_component_clause,[],[f4334]) ).
fof(f4337,definition,
( spl66_19
<=> sK17 = sK40 ),
introduced(definition,[new_symbols(definition,[spl66_19])],[avatar_definition]) ).
fof(f4338,plain,
( sK17 != sK40
| spl66_19 ),
inference(avatar_component_clause,[],[f4337]) ).
fof(f4339,plain,
( sK17 = sK40
| ~ spl66_19 ),
inference(avatar_component_clause,[],[f4337]) ).
fof(f4728,plain,
( ! [X0] :
( rline(X0)
| vd684 = vangle(sK40,sK17,sK40)
| ~ ron(sK40,X0)
| rpoint(sK40)
| ~ ron(sK40,X0)
| sK17 = sK40
| rpoint(sK17)
| sK17 = sK40
| rpoint(sK40)
| ~ ron(sK17,X0) )
| ~ spl66_12 ),
inference(resolution,[],[f1760,f1967]) ).
fof(f4743,plain,
( ! [X0] :
( rpoint(sK17)
| rpoint(sK40)
| rline(X0)
| ~ ron(sK40,X0)
| sK17 = sK40
| vd684 = vangle(sK40,sK17,sK40)
| ~ ron(sK17,X0) )
| ~ spl66_12 ),
inference(duplicate_literal_removal,[],[f4728]) ).
fof(f4747,plain,
( ! [X0] :
( rpoint(sK40)
| rline(X0)
| ~ ron(sK40,X0)
| ~ ron(sK17,X0)
| vd684 = vangle(sK40,sK17,sK40)
| sK17 = sK40 )
| ~ spl66_12 ),
inference(forward_subsumption_resolution,[],[f4743,f1753]) ).
fof(f4749,plain,
( ! [X0] :
( rline(X0)
| ~ ron(sK40,X0)
| ~ ron(sK17,X0)
| vd684 = vangle(sK40,sK17,sK40)
| sK17 = sK40 )
| ~ spl66_12 ),
inference(forward_subsumption_resolution,[],[f4747,f1680]) ).
fof(f4751,definition,
( spl66_49
<=> vd684 = vangle(sK40,sK17,sK40) ),
introduced(definition,[new_symbols(definition,[spl66_49])],[avatar_definition]) ).
fof(f4753,plain,
( vd684 = vangle(sK40,sK17,sK40)
| ~ spl66_49 ),
inference(avatar_component_clause,[],[f4751]) ).
fof(f4754,plain,
( spl66_18
| spl66_49
| spl66_19
| ~ spl66_12 ),
inference(avatar_split_clause,[],[f4749,f1944,f4337,f4751,f4334]) ).
fof(f5143,plain,
( ! [X2,X3,X0,X1] :
( ~ ron(sK40,X3)
| rpoint(sK17)
| sK17 = X1
| sK17 = sK40
| rpoint(sK40)
| sK17 = sK40
| ~ rR(sK17,X1,X0)
| rline(X2)
| sK17 = X0
| ~ ron(sK40,X3)
| rline(X3)
| rpoint(X1)
| ~ ron(X1,X2)
| ~ ron(sK17,X3)
| rpoint(X0)
| ~ ron(X0,X2)
| vangle(sK40,sK17,X0) = vangle(sK40,sK17,X1)
| rpoint(sK40) )
| ~ spl66_12 ),
inference(resolution,[],[f1787,f1967]) ).
fof(f5156,plain,
( ! [X2,X3,X0,X1] :
( ~ rR(sK17,X1,X0)
| rpoint(X0)
| rline(X3)
| vangle(sK40,sK17,X0) = vangle(sK40,sK17,X1)
| ~ ron(sK17,X3)
| ~ ron(X0,X2)
| rpoint(X1)
| ~ ron(sK40,X3)
| sK17 = X0
| sK17 = sK40
| ~ ron(X1,X2)
| sK17 = X1
| rline(X2)
| rpoint(sK40)
| rpoint(sK17) )
| ~ spl66_12 ),
inference(duplicate_literal_removal,[],[f5143]) ).
fof(f5163,plain,
( ! [X2,X3,X0,X1] :
( sK17 = sK40
| ~ ron(sK40,X3)
| sK17 = X1
| rpoint(X1)
| ~ rR(sK17,X1,X0)
| rpoint(X0)
| rline(X3)
| ~ ron(X1,X2)
| sK17 = X0
| rpoint(sK17)
| ~ ron(sK17,X3)
| vangle(sK40,sK17,X0) = vangle(sK40,sK17,X1)
| ~ ron(X0,X2)
| rline(X2) )
| ~ spl66_12 ),
inference(forward_subsumption_resolution,[],[f5156,f1680]) ).
fof(f5166,plain,
( ! [X2,X3,X0,X1] :
( rline(X3)
| ~ ron(sK17,X3)
| sK17 = X0
| rline(X2)
| ~ rR(sK17,X1,X0)
| sK17 = X1
| vangle(sK40,sK17,X0) = vangle(sK40,sK17,X1)
| ~ ron(X0,X2)
| ~ ron(X1,X2)
| ~ ron(sK40,X3)
| rpoint(X0)
| sK17 = sK40
| rpoint(X1) )
| ~ spl66_12 ),
inference(forward_subsumption_resolution,[],[f5163,f1753]) ).
fof(f5168,definition,
( spl66_53
<=> ! [X2,X0,X1] :
( sK17 = X0
| rpoint(X1)
| rpoint(X0)
| ~ ron(X1,X2)
| ~ ron(X0,X2)
| vangle(sK40,sK17,X0) = vangle(sK40,sK17,X1)
| sK17 = X1
| ~ rR(sK17,X1,X0)
| rline(X2) ) ),
introduced(definition,[new_symbols(definition,[spl66_53])],[avatar_definition]) ).
fof(f5169,plain,
( ! [X2,X0,X1] :
( ~ ron(X0,X2)
| sK17 = X1
| rline(X2)
| ~ rR(sK17,X1,X0)
| rpoint(X0)
| ~ ron(X1,X2)
| sK17 = X0
| vangle(sK40,sK17,X0) = vangle(sK40,sK17,X1)
| rpoint(X1) )
| ~ spl66_53 ),
inference(avatar_component_clause,[],[f5168]) ).
fof(f5170,plain,
( spl66_53
| spl66_18
| spl66_19
| ~ spl66_12 ),
inference(avatar_split_clause,[],[f5166,f1944,f4337,f4334,f5168]) ).
fof(f5425,plain,
( vd684 != vf(sK40,sK40)
| ~ spl66_19 ),
inference(superposition,[],[f2418,f4339]) ).
fof(f5438,plain,
( $false
| ~ spl66_19 ),
inference(forward_subsumption_resolution,[],[f5425,f1982]) ).
fof(f5439,plain,
~ spl66_19,
inference(avatar_contradiction_clause,[],[f5438]) ).
fof(f5916,plain,
( rline(vd1197)
| ~ ron(sK40,vd1197)
| ~ spl66_18 ),
inference(resolution,[],[f4335,f813]) ).
fof(f5925,plain,
( ~ ron(sK40,vd1197)
| ~ spl66_18 ),
inference(forward_subsumption_resolution,[],[f5916,f1706]) ).
fof(f5935,plain,
( $false
| ~ spl66_18 ),
inference(forward_subsumption_resolution,[],[f5925,f794]) ).
fof(f5936,plain,
~ spl66_18,
inference(avatar_contradiction_clause,[],[f5935]) ).
fof(f9317,definition,
( spl66_133
<=> sK39 = sK17 ),
introduced(definition,[new_symbols(definition,[spl66_133])],[avatar_definition]) ).
fof(f9318,plain,
( sK39 != sK17
| spl66_133 ),
inference(avatar_component_clause,[],[f9317]) ).
fof(f9319,plain,
( sK39 = sK17
| ~ spl66_133 ),
inference(avatar_component_clause,[],[f9317]) ).
fof(f9475,plain,
( ~ ron(sK17,vd1197)
| ~ spl66_133 ),
inference(superposition,[],[f799,f9319]) ).
fof(f9509,plain,
( $false
| ~ spl66_133 ),
inference(forward_subsumption_resolution,[],[f9475,f813]) ).
fof(f9510,plain,
~ spl66_133,
inference(avatar_contradiction_clause,[],[f9509]) ).
fof(f96849,plain,
( ! [X0] :
( rline(vd1232)
| sK17 = X0
| rpoint(X0)
| rpoint(sK40)
| vangle(sK40,sK17,X0) = vangle(sK40,sK17,sK40)
| sK17 = sK40
| ~ rR(sK17,X0,sK40)
| ~ ron(X0,vd1232) )
| ~ spl66_53 ),
inference(resolution,[],[f5169,f789]) ).
fof(f96926,plain,
( ! [X0] :
( vangle(sK40,sK17,X0) = vangle(sK40,sK17,sK40)
| sK17 = sK40
| sK17 = X0
| rpoint(X0)
| ~ ron(X0,vd1232)
| ~ rR(sK17,X0,sK40)
| rpoint(sK40) )
| ~ spl66_53 ),
inference(forward_subsumption_resolution,[],[f96849,f1815]) ).
fof(f96948,plain,
( ! [X0] :
( vangle(sK40,sK17,X0) = vangle(sK40,sK17,sK40)
| rpoint(X0)
| ~ rR(sK17,X0,sK40)
| rpoint(sK40)
| sK17 = X0
| ~ ron(X0,vd1232) )
| spl66_19
| ~ spl66_53 ),
inference(forward_subsumption_resolution,[],[f96926,f4338]) ).
fof(f96956,plain,
( ! [X0] :
( vangle(sK40,sK17,X0) = vangle(sK40,sK17,sK40)
| sK17 = X0
| ~ ron(X0,vd1232)
| rpoint(X0)
| ~ rR(sK17,X0,sK40) )
| spl66_19
| ~ spl66_53 ),
inference(forward_subsumption_resolution,[],[f96948,f1680]) ).
fof(f96961,plain,
( ! [X0] :
( ~ rR(sK17,X0,sK40)
| rpoint(X0)
| sK17 = X0
| vd684 = vangle(sK40,sK17,X0)
| ~ ron(X0,vd1232) )
| spl66_19
| ~ spl66_49
| ~ spl66_53 ),
inference(forward_demodulation,[],[f96956,f4753]) ).
fof(f615925,plain,
( sK39 = sK17
| rpoint(sK17)
| rpoint(sK40)
| ~ ron(sK40,vd1232)
| vd684 = vangle(sK40,sK17,sK39)
| ron(sK17,vd1232)
| rpoint(sK39)
| ~ ron(sK39,vd1232)
| spl66_19
| ~ spl66_49
| ~ spl66_53 ),
inference(resolution,[],[f96961,f3288]) ).
fof(f616094,plain,
( ~ ron(sK40,vd1232)
| rpoint(sK39)
| rpoint(sK40)
| ~ ron(sK39,vd1232)
| rpoint(sK17)
| ron(sK17,vd1232)
| vd684 = vangle(sK40,sK17,sK39)
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(forward_subsumption_resolution,[],[f615925,f9318]) ).
fof(f616166,plain,
( rpoint(sK39)
| ron(sK17,vd1232)
| rpoint(sK17)
| rpoint(sK40)
| ~ ron(sK39,vd1232)
| vd684 = vangle(sK40,sK17,sK39)
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(forward_subsumption_resolution,[],[f616094,f789]) ).
fof(f616235,plain,
( rpoint(sK17)
| ron(sK17,vd1232)
| vd684 = vangle(sK40,sK17,sK39)
| rpoint(sK40)
| ~ ron(sK39,vd1232)
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(forward_subsumption_resolution,[],[f616166,f1654]) ).
fof(f616252,plain,
( rpoint(sK40)
| vd684 = vangle(sK40,sK17,sK39)
| ron(sK17,vd1232)
| ~ ron(sK39,vd1232)
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(forward_subsumption_resolution,[],[f616235,f1753]) ).
fof(f616255,plain,
( ~ ron(sK39,vd1232)
| ron(sK17,vd1232)
| vd684 = vangle(sK40,sK17,sK39)
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(forward_subsumption_resolution,[],[f616252,f1680]) ).
fof(f616257,plain,
( ron(sK17,vd1232)
| vd684 = vangle(sK40,sK17,sK39)
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(forward_subsumption_resolution,[],[f616255,f793]) ).
fof(f616258,plain,
( vd684 = vangle(sK40,sK17,sK39)
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(forward_subsumption_resolution,[],[f616257,f2229]) ).
fof(f617678,plain,
( ! [X0] :
( rpoint(sK40)
| rline(X0)
| ~ ron(sK40,X0)
| sK17 = sK40
| rpoint(sK39)
| ron(sK39,X0)
| rpoint(sK17)
| vd684 != vd684
| ~ ron(sK17,X0)
| sK39 = sK17 )
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(superposition,[],[f1858,f616258]) ).
fof(f617684,plain,
( ! [X0] :
( rline(X0)
| sK39 = sK17
| ron(sK39,X0)
| ~ ron(sK17,X0)
| sK17 = sK40
| ~ ron(sK40,X0)
| rpoint(sK17)
| rpoint(sK39)
| rpoint(sK40) )
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(trivial_inequality_removal,[],[f617678]) ).
fof(f617692,plain,
( ! [X0] :
( ron(sK39,X0)
| ~ ron(sK17,X0)
| rpoint(sK17)
| sK17 = sK40
| rline(X0)
| rpoint(sK39)
| ~ ron(sK40,X0)
| rpoint(sK40) )
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(forward_subsumption_resolution,[],[f617684,f9318]) ).
fof(f617700,plain,
( ! [X0] :
( rpoint(sK40)
| rline(X0)
| rpoint(sK39)
| sK17 = sK40
| ~ ron(sK40,X0)
| ron(sK39,X0)
| ~ ron(sK17,X0) )
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(forward_subsumption_resolution,[],[f617692,f1753]) ).
fof(f617708,plain,
( ! [X0] :
( rline(X0)
| ron(sK39,X0)
| sK17 = sK40
| ~ ron(sK17,X0)
| ~ ron(sK40,X0)
| rpoint(sK39) )
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(forward_subsumption_resolution,[],[f617700,f1680]) ).
fof(f617719,plain,
( ! [X0] :
( rline(X0)
| ~ ron(sK17,X0)
| rpoint(sK39)
| ron(sK39,X0)
| ~ ron(sK40,X0) )
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(forward_subsumption_resolution,[],[f617708,f4338]) ).
fof(f617725,plain,
( ! [X0] :
( ron(sK39,X0)
| rline(X0)
| ~ ron(sK17,X0)
| ~ ron(sK40,X0) )
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(forward_subsumption_resolution,[],[f617719,f1654]) ).
fof(f617735,plain,
( ! [X0] :
( ~ ron(sK40,X0)
| ~ ron(sK17,X0)
| rline(X0) )
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(forward_subsumption_resolution,[],[f617725,f1850]) ).
fof(f617738,plain,
( spl66_18
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(avatar_split_clause,[],[f617735,f9317,f5168,f4751,f4337,f4334]) ).
cnf(s17,plain,
spl66_12,
inference(sat_conversion,[],[f1964]) ).
cnf(s47,plain,
( ~ spl66_12
| spl66_18
| spl66_19
| spl66_49 ),
inference(sat_conversion,[],[f4754]) ).
cnf(s50,plain,
( ~ spl66_12
| spl66_18
| spl66_19
| spl66_53 ),
inference(sat_conversion,[],[f5170]) ).
cnf(s65,plain,
~ spl66_19,
inference(sat_conversion,[],[f5439]) ).
cnf(s67,plain,
~ spl66_18,
inference(sat_conversion,[],[f5936]) ).
cnf(s144,plain,
~ spl66_133,
inference(sat_conversion,[],[f9510]) ).
cnf(s8282,plain,
( spl66_18
| spl66_19
| ~ spl66_49
| ~ spl66_53
| spl66_133 ),
inference(sat_conversion,[],[f617738]) ).
cnf(s10182,plain,
( ~ spl66_12
| spl66_53 ),
inference(rat,[],[s50,s65,s67]) ).
cnf(s10184,plain,
( ~ spl66_12
| spl66_49 ),
inference(rat,[],[s47,s65,s67]) ).
cnf(s10247,plain,
spl66_53,
inference(rat,[],[s10182,s17]) ).
cnf(s10248,plain,
spl66_49,
inference(rat,[],[s10184,s17]) ).
cnf(s10277,plain,
$false,
inference(rat,[],[s8282,s144,s65,s67,s10247,s10248]) ).
fof(f617741,plain,
$false,
inference(avatar_sat_refutation,[],[s10277]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO292+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n026.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.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 08:03:11 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
% 2.69/0.92 % (2511312)Will run a generic schedule for satisfiability detection.
% 2.69/0.92 % (2511323)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2855288809:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.69/0.92 % (2511318)% WARNING: option uhcvi not known.
% 2.69/0.92 % (2511317)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1632894349_2999 on theBenchmark for (2999ds/0Mi)
% 2.69/0.92 % (2511319)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1199920532:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.69/0.92 % (2511318)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=474288412:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.69/0.92 % (2511320)dis+10_1_sil=32000:sp=arity:random_seed=3894489347:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.69/0.92 % (2511321)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1666708235:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.69/0.92 % (2511322)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1723248464:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.69/0.92 % Detected minimum model sizes of [3]
% 2.69/0.92 % Detected maximum model sizes of [max]
% 2.69/0.92 % (2511317)Cannot represent all propositional literals internally
% 2.69/0.92 % (2511317)Refutation not found, incomplete strategy
% 2.69/0.92 % (2511317)------------------------------
% 2.69/0.92 % (2511317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.92 % (2511317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.92 % (2511317)CaDiCaL version: 2.1.3
% 2.69/0.92 % (2511317)Termination reason: Refutation not found, incomplete strategy
% 2.69/0.92 % (2511317)Time elapsed: 0.035 s
% 2.69/0.92 % (2511317)Peak memory usage: 12 MB
% 2.69/0.92 % (2511317)Instructions burned: 72 (million)
% 2.69/0.92 % (2511317)------------------------------
% 2.69/0.92 % (2511317)------------------------------
% 2.69/0.92 % (2511323)Instruction limit reached!
% 2.69/0.92 % (2511323)------------------------------
% 2.69/0.92 % (2511323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.92 % (2511323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.92 % (2511323)CaDiCaL version: 2.1.3
% 2.69/0.92 % (2511323)Termination reason: Instruction limit
% 2.69/0.92 % (2511323)Termination phase: Saturation
% 2.69/0.92 % (2511323)Time elapsed: 0.053 s
% 2.69/0.92 % (2511323)Peak memory usage: 15 MB
% 2.69/0.92 % (2511323)Instructions burned: 160 (million)
% 2.69/0.92 % (2511320)Instruction limit reached!
% 2.69/0.92 % (2511320)------------------------------
% 2.69/0.92 % (2511320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.92 % (2511320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.92 % (2511320)CaDiCaL version: 2.1.3
% 2.69/0.92 % (2511320)Termination reason: Instruction limit
% 2.69/0.92 % (2511320)Termination phase: Saturation
% 2.69/0.92 % (2511320)Time elapsed: 0.056 s
% 2.69/0.92 % (2511320)Peak memory usage: 13 MB
% 2.69/0.92 % (2511320)Instructions burned: 103 (million)
% 2.69/0.92 % (2511331)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2589610984:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.69/0.92 % (2511332)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3244076142:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.69/0.92 % (2511321)Instruction limit reached!
% 2.69/0.92 % (2511321)------------------------------
% 2.69/0.92 % (2511321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.92 % (2511321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.92 % (2511321)CaDiCaL version: 2.1.3
% 2.69/0.92 % (2511321)Termination reason: Instruction limit
% 2.69/0.92 % (2511321)Termination phase: Saturation
% 2.69/0.92 % (2511321)Time elapsed: 0.058 s
% 2.69/0.92 % (2511321)Peak memory usage: 13 MB
% 2.69/0.92 % (2511321)Instructions burned: 117 (million)
% 2.69/0.92 % (2511322)Instruction limit reached!
% 2.69/0.92 % (2511322)------------------------------
% 2.69/0.92 % (2511322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.92 % (2511322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.92 % (2511322)CaDiCaL version: 2.1.3
% 2.69/0.92 % (2511322)Termination reason: Instruction limit
% 2.69/0.92 % (2511322)Termination phase: Saturation
% 2.69/0.92 % (2511322)Time elapsed: 0.062 s
% 5.12/1.24 % (2511322)Peak memory usage: 13 MB
% 5.12/1.24 % (2511322)Instructions burned: 131 (million)
% 5.12/1.24 % (2511334)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=1698901658:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 5.12/1.24 % (2511336)ott-21_1_sil=16000:fs=off:random_seed=4043868474:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 5.12/1.24 % (2511337)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2180902443:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.12/1.24 % Detected minimum model sizes of [3]
% 5.12/1.24 % Detected maximum model sizes of [max]
% 5.12/1.24 % (2511331)Cannot represent all propositional literals internally
% 5.12/1.24 % (2511331)Refutation not found, incomplete strategy
% 5.12/1.24 % (2511331)------------------------------
% 5.12/1.24 % (2511331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.12/1.24 % (2511331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.12/1.24 % (2511332)Instruction limit reached!
% 5.12/1.24 % (2511332)------------------------------
% 5.12/1.24 % (2511332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.12/1.24 % (2511331)CaDiCaL version: 2.1.3
% 5.12/1.24 % (2511332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.12/1.24 % (2511332)CaDiCaL version: 2.1.3
% 5.12/1.24 % (2511331)Termination reason: Refutation not found, incomplete strategy
% 5.12/1.24 % (2511331)Time elapsed: 0.028 s
% 5.12/1.24 % (2511332)Termination reason: Instruction limit
% 5.12/1.24 % (2511332)Termination phase: Saturation
% 5.12/1.24 % (2511332)Time elapsed: 0.027 s
% 5.12/1.24 % (2511332)Peak memory usage: 12 MB
% 5.12/1.24 % (2511332)Instructions burned: 134 (million)
% 5.12/1.24 % (2511331)Peak memory usage: 12 MB
% 5.12/1.24 % (2511331)Instructions burned: 58 (million)
% 5.12/1.24 % (2511331)------------------------------
% 5.12/1.24 % (2511331)------------------------------
% 5.12/1.24 % (2511341)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2981539793:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 5.12/1.24 % (2511342)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=93539892:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 5.12/1.24 % Detected minimum model sizes of [3]
% 5.12/1.24 % Detected maximum model sizes of [max]
% 5.12/1.24 % (2511341)Cannot represent all propositional literals internally
% 5.12/1.24 % (2511341)Refutation not found, incomplete strategy
% 5.12/1.24 % (2511341)------------------------------
% 5.12/1.24 % (2511341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.12/1.24 % (2511341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.12/1.24 % (2511341)CaDiCaL version: 2.1.3
% 5.12/1.24 % (2511341)Termination reason: Refutation not found, incomplete strategy
% 5.12/1.24 % (2511341)Time elapsed: 0.015 s
% 5.12/1.24 % (2511341)Peak memory usage: 12 MB
% 5.12/1.24 % (2511341)Instructions burned: 60 (million)
% 5.12/1.24 % (2511341)------------------------------
% 5.12/1.24 % (2511341)------------------------------
% 5.12/1.24 % (2511345)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2528894937:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 5.12/1.24 % (2511345)Cannot represent all propositional literals internally
% 5.12/1.24 % (2511345)Refutation not found, incomplete strategy
% 5.12/1.24 % (2511345)------------------------------
% 5.12/1.24 % (2511345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.12/1.24 % (2511345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.12/1.24 % (2511345)CaDiCaL version: 2.1.3
% 5.12/1.24 % (2511345)Termination reason: Refutation not found, incomplete strategy
% 5.12/1.24 % (2511345)Time elapsed: 0.015 s
% 5.12/1.24 % (2511345)Peak memory usage: 12 MB
% 5.12/1.24 % (2511345)Instructions burned: 60 (million)
% 5.12/1.24 % (2511345)------------------------------
% 5.12/1.24 % (2511345)------------------------------
% 5.12/1.24 % (2511347)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=1756836907:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 5.12/1.24 % (2511336)Instruction limit reached!
% 5.12/1.24 % (2511336)------------------------------
% 5.12/1.24 % (2511336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.42 % (2511336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.42 % (2511336)CaDiCaL version: 2.1.3
% 13.87/2.42 % (2511336)Termination reason: Instruction limit
% 13.87/2.42 % (2511336)Termination phase: Saturation
% 13.87/2.42 % (2511336)Time elapsed: 0.093 s
% 13.87/2.42 % (2511336)Peak memory usage: 14 MB
% 13.87/2.42 % (2511336)Instructions burned: 182 (million)
% 13.87/2.42 % (2511349)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2176839852:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 13.87/2.42 % (2511337)Instruction limit reached!
% 13.87/2.42 % (2511337)------------------------------
% 13.87/2.42 % (2511337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.42 % (2511337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.42 % (2511337)CaDiCaL version: 2.1.3
% 13.87/2.42 % (2511337)Termination reason: Instruction limit
% 13.87/2.42 % (2511337)Termination phase: Saturation
% 13.87/2.42 % (2511337)Time elapsed: 0.299 s
% 13.87/2.42 % (2511337)Peak memory usage: 15 MB
% 13.87/2.42 % (2511337)Instructions burned: 478 (million)
% 13.87/2.42 % (2511351)fmb+10_1_sil=64000:random_seed=3358661163:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 13.87/2.42 % (2511349)Instruction limit reached!
% 13.87/2.42 % (2511349)------------------------------
% 13.87/2.42 % (2511349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.42 % (2511349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.42 % (2511349)CaDiCaL version: 2.1.3
% 13.87/2.42 % (2511349)Termination reason: Instruction limit
% 13.87/2.42 % (2511349)Termination phase: Saturation
% 13.87/2.42 % (2511349)Time elapsed: 0.239 s
% 13.87/2.42 % (2511349)Peak memory usage: 21 MB
% 13.87/2.42 % (2511349)Instructions burned: 879 (million)
% 13.87/2.42 % Detected minimum model sizes of [3]
% 13.87/2.42 % Detected maximum model sizes of [max]
% 13.87/2.42 % (2511351)Cannot represent all propositional literals internally
% 13.87/2.42 % (2511351)Refutation not found, incomplete strategy
% 13.87/2.42 % (2511351)------------------------------
% 13.87/2.42 % (2511351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.42 % (2511351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.42 % (2511351)CaDiCaL version: 2.1.3
% 13.87/2.42 % (2511351)Termination reason: Refutation not found, incomplete strategy
% 13.87/2.42 % (2511351)Time elapsed: 0.028 s
% 13.87/2.42 % (2511351)Peak memory usage: 12 MB
% 13.87/2.42 % (2511351)Instructions burned: 56 (million)
% 13.87/2.42 % (2511351)------------------------------
% 13.87/2.42 % (2511351)------------------------------
% 13.87/2.42 % (2511353)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2717940694:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 13.87/2.42 % (2511334)Instruction limit reached!
% 13.87/2.42 % (2511334)------------------------------
% 13.87/2.42 % (2511334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.42 % (2511334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.42 % (2511334)CaDiCaL version: 2.1.3
% 13.87/2.42 % (2511334)Termination reason: Instruction limit
% 13.87/2.42 % (2511334)Termination phase: Saturation
% 13.87/2.42 % (2511334)Time elapsed: 0.360 s
% 13.87/2.42 % (2511334)Peak memory usage: 22 MB
% 13.87/2.42 % (2511334)Instructions burned: 685 (million)
% 13.87/2.42 % Detected minimum model sizes of [3]
% 13.87/2.42 % Detected maximum model sizes of [max]
% 13.87/2.42 % (2511353)Cannot represent all propositional literals internally
% 13.87/2.42 % (2511353)Refutation not found, incomplete strategy
% 13.87/2.42 % (2511353)------------------------------
% 13.87/2.42 % (2511353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.42 % (2511353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.42 % (2511353)CaDiCaL version: 2.1.3
% 13.87/2.42 % (2511353)Termination reason: Refutation not found, incomplete strategy
% 13.87/2.42 % (2511353)Time elapsed: 0.015 s
% 13.87/2.42 % (2511353)Peak memory usage: 12 MB
% 13.87/2.42 % (2511353)Instructions burned: 60 (million)
% 13.87/2.42 % (2511353)------------------------------
% 13.87/2.42 % (2511353)------------------------------
% 13.87/2.42 % (2511354)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2493373344:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 13.87/2.42 % (2511356)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1911197684:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 13.87/2.42 % (2511357)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4117437303:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 20.09/3.33 % Detected minimum model sizes of [3]
% 20.09/3.33 % Detected maximum model sizes of [max]
% 20.09/3.33 % (2511354)Cannot represent all propositional literals internally
% 20.09/3.33 % (2511354)Refutation not found, incomplete strategy
% 20.09/3.33 % (2511354)------------------------------
% 20.09/3.33 % (2511354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.09/3.33 % (2511354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.09/3.33 % (2511354)CaDiCaL version: 2.1.3
% 20.09/3.33 % (2511354)Termination reason: Refutation not found, incomplete strategy
% 20.09/3.33 % (2511354)Time elapsed: 0.029 s
% 20.09/3.33 % (2511354)Peak memory usage: 12 MB
% 20.09/3.33 % (2511354)Instructions burned: 60 (million)
% 20.09/3.33 % (2511354)------------------------------
% 20.09/3.33 % (2511354)------------------------------
% 20.09/3.33 % (2511361)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1615506381:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 20.09/3.33 % Detected minimum model sizes of [3]
% 20.09/3.33 % Detected maximum model sizes of [max]
% 20.09/3.33 % (2511361)Cannot represent all propositional literals internally
% 20.09/3.33 % (2511361)Refutation not found, incomplete strategy
% 20.09/3.33 % (2511361)------------------------------
% 20.09/3.33 % (2511361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.09/3.33 % (2511361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.09/3.33 % (2511361)CaDiCaL version: 2.1.3
% 20.09/3.33 % (2511361)Termination reason: Refutation not found, incomplete strategy
% 20.09/3.33 % (2511361)Time elapsed: 0.035 s
% 20.09/3.33 % (2511361)Peak memory usage: 12 MB
% 20.09/3.33 % (2511361)Instructions burned: 72 (million)
% 20.09/3.33 % (2511361)------------------------------
% 20.09/3.33 % (2511361)------------------------------
% 20.09/3.33 % (2511347)Instruction limit reached!
% 20.09/3.33 % (2511347)------------------------------
% 20.09/3.33 % (2511347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.09/3.33 % (2511347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.09/3.33 % (2511347)CaDiCaL version: 2.1.3
% 20.09/3.33 % (2511347)Termination reason: Instruction limit
% 20.09/3.33 % (2511347)Termination phase: Saturation
% 20.09/3.33 % (2511347)Time elapsed: 0.384 s
% 20.09/3.33 % (2511347)Peak memory usage: 21 MB
% 20.09/3.33 % (2511347)Instructions burned: 697 (million)
% 20.09/3.33 % (2511363)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=827412424:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 20.09/3.33 % (2511364)ott-2_1_sil=16000:newcnf=on:random_seed=547754886:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 20.09/3.33 % Detected minimum model sizes of [3]
% 20.09/3.33 % Detected maximum model sizes of [max]
% 20.09/3.33 % (2511363)Cannot represent all propositional literals internally
% 20.09/3.33 % (2511363)Refutation not found, incomplete strategy
% 20.09/3.33 % (2511363)------------------------------
% 20.09/3.33 % (2511363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.09/3.33 % (2511363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.09/3.33 % (2511363)CaDiCaL version: 2.1.3
% 20.09/3.33 % (2511363)Termination reason: Refutation not found, incomplete strategy
% 20.09/3.33 % (2511363)Time elapsed: 0.029 s
% 20.09/3.33 % (2511363)Peak memory usage: 12 MB
% 20.09/3.33 % (2511363)Instructions burned: 61 (million)
% 20.09/3.33 % (2511363)------------------------------
% 20.09/3.33 % (2511363)------------------------------
% 20.09/3.33 % (2511367)ott+10_1_sil=32000:tgt=ground:random_seed=587706248:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 20.09/3.33 % (2511342)Instruction limit reached!
% 20.09/3.33 % (2511342)------------------------------
% 20.09/3.33 % (2511342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.09/3.33 % (2511342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.09/3.33 % (2511342)CaDiCaL version: 2.1.3
% 20.09/3.33 % (2511342)Termination reason: Instruction limit
% 20.09/3.33 % (2511342)Termination phase: Saturation
% 20.09/3.33 % (2511342)Time elapsed: 0.610 s
% 20.09/3.33 % (2511342)Peak memory usage: 21 MB
% 20.09/3.33 % (2511342)Instructions burned: 1179 (million)
% 20.09/3.33 % (2511369)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1836806880:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 57.30/8.58 % Detected minimum model sizes of [3]
% 57.30/8.58 % Detected maximum model sizes of [max]
% 57.30/8.58 % (2511369)Cannot represent all propositional literals internally
% 57.30/8.58 % (2511369)Refutation not found, incomplete strategy
% 57.30/8.58 % (2511369)------------------------------
% 57.30/8.58 % (2511369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.30/8.58 % (2511369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.30/8.58 % (2511369)CaDiCaL version: 2.1.3
% 57.30/8.58 % (2511369)Termination reason: Refutation not found, incomplete strategy
% 57.30/8.58 % (2511369)Time elapsed: 0.035 s
% 57.30/8.58 % (2511369)Peak memory usage: 12 MB
% 57.30/8.58 % (2511369)Instructions burned: 72 (million)
% 57.30/8.58 % (2511369)------------------------------
% 57.30/8.58 % (2511369)------------------------------
% 57.30/8.58 % (2511371)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2251858424:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 57.30/8.58 % (2511357)Instruction limit reached!
% 57.30/8.58 % (2511357)------------------------------
% 57.30/8.58 % (2511357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.30/8.58 % (2511357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.30/8.58 % (2511357)CaDiCaL version: 2.1.3
% 57.30/8.58 % (2511357)Termination reason: Instruction limit
% 57.30/8.58 % (2511357)Termination phase: Saturation
% 57.30/8.58 % (2511357)Time elapsed: 0.332 s
% 57.30/8.58 % (2511357)Peak memory usage: 18 MB
% 57.30/8.58 % (2511357)Instructions burned: 1475 (million)
% 57.30/8.58 % (2511373)dis+21_1_sil=32000:sas=cadical:random_seed=62420353:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi)
% 57.30/8.58 % (2511364)Instruction limit reached!
% 57.30/8.58 % (2511364)------------------------------
% 57.30/8.58 % (2511364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.30/8.58 % (2511364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.30/8.58 % (2511364)CaDiCaL version: 2.1.3
% 57.30/8.58 % (2511364)Termination reason: Instruction limit
% 57.30/8.58 % (2511364)Termination phase: Saturation
% 57.30/8.58 % (2511364)Time elapsed: 0.431 s
% 57.30/8.58 % (2511364)Peak memory usage: 16 MB
% 57.30/8.58 % (2511364)Instructions burned: 870 (million)
% 57.30/8.58 % (2511375)ott+11_1_sil=16000:gs=on:random_seed=1168778551:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi)
% 57.30/8.58 % (2511373)Instruction limit reached!
% 57.30/8.58 % (2511373)------------------------------
% 57.30/8.58 % (2511373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.30/8.58 % (2511373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.30/8.58 % (2511373)CaDiCaL version: 2.1.3
% 57.30/8.58 % (2511373)Termination reason: Instruction limit
% 57.30/8.58 % (2511373)Termination phase: Saturation
% 57.30/8.58 % (2511373)Time elapsed: 0.989 s
% 57.30/8.58 % (2511373)Peak memory usage: 39 MB
% 57.30/8.58 % (2511373)Instructions burned: 3777 (million)
% 57.30/8.58 % (2511377)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2572398487:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi)
% 57.30/8.58 % Detected minimum model sizes of [3]
% 57.30/8.58 % Detected maximum model sizes of [max]
% 57.30/8.58 % (2511377)Cannot represent all propositional literals internally
% 57.30/8.58 % (2511377)Refutation not found, incomplete strategy
% 57.30/8.58 % (2511377)------------------------------
% 57.30/8.58 % (2511377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.30/8.58 % (2511377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.30/8.58 % (2511377)CaDiCaL version: 2.1.3
% 57.30/8.58 % (2511377)Termination reason: Refutation not found, incomplete strategy
% 57.30/8.58 % (2511377)Time elapsed: 0.016 s
% 57.30/8.58 % (2511377)Peak memory usage: 12 MB
% 57.30/8.58 % (2511377)Instructions burned: 65 (million)
% 57.30/8.58 % (2511377)------------------------------
% 57.30/8.58 % (2511377)------------------------------
% 57.30/8.58 % (2511379)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1144421270:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi)
% 57.30/8.58 % (2511375)Instruction limit reached!
% 57.30/8.58 % (2511375)------------------------------
% 57.30/8.58 % (2511375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.30/8.58 % (2511375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.39/15.80 % (2511375)CaDiCaL version: 2.1.3
% 108.39/15.80 % (2511375)Termination reason: Instruction limit
% 108.39/15.80 % (2511375)Termination phase: Saturation
% 108.39/15.80 % (2511375)Time elapsed: 0.937 s
% 108.39/15.80 % (2511375)Peak memory usage: 17 MB
% 108.39/15.80 % (2511375)Instructions burned: 2253 (million)
% 108.39/15.80 % (2511381)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1064265362:i=29340_2980 on theBenchmark for (2980ds/29340Mi)
% 108.39/15.80 % (2511371)Instruction limit reached!
% 108.39/15.80 % (2511371)------------------------------
% 108.39/15.80 % (2511371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.39/15.80 % (2511371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.39/15.80 % (2511371)CaDiCaL version: 2.1.3
% 108.39/15.80 % (2511371)Termination reason: Instruction limit
% 108.39/15.80 % (2511371)Termination phase: Saturation
% 108.39/15.80 % (2511371)Time elapsed: 1.792 s
% 108.39/15.80 % (2511371)Peak memory usage: 33 MB
% 108.39/15.80 % (2511371)Instructions burned: 3513 (million)
% 108.39/15.80 % (2511383)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2048356678:i=5211_2973 on theBenchmark for (2973ds/5211Mi)
% 108.39/15.80 % (2511379)Instruction limit reached!
% 108.39/15.80 % (2511379)------------------------------
% 108.39/15.80 % (2511379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.39/15.80 % (2511379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.39/15.80 % (2511379)CaDiCaL version: 2.1.3
% 108.39/15.80 % (2511379)Termination reason: Instruction limit
% 108.39/15.80 % (2511379)Termination phase: Saturation
% 108.39/15.80 % (2511379)Time elapsed: 0.899 s
% 108.39/15.80 % (2511379)Peak memory usage: 27 MB
% 108.39/15.80 % (2511379)Instructions burned: 4591 (million)
% 108.39/15.80 % (2511385)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3147496227:i=5497:nm=2_2972 on theBenchmark for (2972ds/5497Mi)
% 108.39/15.80 % Detected minimum model sizes of [3]
% 108.39/15.80 % Detected maximum model sizes of [max]
% 108.39/15.80 % (2511385)Cannot represent all propositional literals internally
% 108.39/15.80 % (2511385)Refutation not found, incomplete strategy
% 108.39/15.80 % (2511385)------------------------------
% 108.39/15.80 % (2511385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.39/15.80 % (2511385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.39/15.80 % (2511385)CaDiCaL version: 2.1.3
% 108.39/15.80 % (2511385)Termination reason: Refutation not found, incomplete strategy
% 108.39/15.80 % (2511385)Time elapsed: 0.031 s
% 108.39/15.80 % (2511385)Peak memory usage: 12 MB
% 108.39/15.80 % (2511385)Instructions burned: 63 (million)
% 108.39/15.80 % (2511385)------------------------------
% 108.39/15.80 % (2511385)------------------------------
% 108.39/15.80 % (2511387)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2323905001:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi)
% 108.39/15.80 % Detected minimum model sizes of [3]
% 108.39/15.80 % Detected maximum model sizes of [max]
% 108.39/15.80 % (2511387)Cannot represent all propositional literals internally
% 108.39/15.80 % (2511387)Refutation not found, incomplete strategy
% 108.39/15.80 % (2511387)------------------------------
% 108.39/15.80 % (2511387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.39/15.80 % (2511387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.39/15.80 % (2511387)CaDiCaL version: 2.1.3
% 108.39/15.80 % (2511387)Termination reason: Refutation not found, incomplete strategy
% 108.39/15.80 % (2511387)Time elapsed: 0.030 s
% 108.39/15.80 % (2511387)Peak memory usage: 12 MB
% 108.39/15.80 % (2511387)Instructions burned: 65 (million)
% 108.39/15.80 % (2511387)------------------------------
% 108.39/15.80 % (2511387)------------------------------
% 108.39/15.80 % (2511389)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2889932009:i=14071_2971 on theBenchmark for (2971ds/14071Mi)
% 108.39/15.80 % Detected minimum model sizes of [3]
% 108.39/15.80 % Detected maximum model sizes of [max]
% 108.39/15.80 % (2511389)Cannot represent all propositional literals internally
% 108.39/15.80 % (2511389)Refutation not found, incomplete strategy
% 108.39/15.80 % (2511389)------------------------------
% 108.39/15.80 % (2511389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.39/15.80 % (2511389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.39/15.80 % (2511389)CaDiCaL version: 2.1.3
% 108.39/15.80 % (2511389)Termination reason: Refutation not found, incomplete strategy
% 108.39/15.80 % (2511389)Time elapsed: 0.015 s
% 108.39/15.80 % (2511389)Peak memory usage: 12 MB
% 108.39/15.80 % (2511389)Instructions burned: 60 (million)
% 108.90/15.97 % (2511389)------------------------------
% 108.90/15.97 % (2511389)------------------------------
% 108.90/15.97 % (2511391)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3514993402:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi)
% 108.90/15.97 % (2511356)Instruction limit reached!
% 108.90/15.97 % (2511356)------------------------------
% 108.90/15.97 % (2511356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.90/15.97 % (2511356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.90/15.97 % (2511356)CaDiCaL version: 2.1.3
% 108.90/15.97 % (2511356)Termination reason: Instruction limit
% 108.90/15.97 % (2511356)Termination phase: Saturation
% 108.90/15.97 % (2511356)Time elapsed: 2.513 s
% 108.90/15.97 % (2511356)Peak memory usage: 37 MB
% 108.90/15.97 % (2511356)Instructions burned: 5133 (million)
% 108.90/15.97 % (2511393)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1303999583:i=8173:av=off_2969 on theBenchmark for (2969ds/8173Mi)
% 108.90/15.97 % (2511367)Instruction limit reached!
% 108.90/15.97 % (2511367)------------------------------
% 108.90/15.97 % (2511367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.90/15.97 % (2511367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.90/15.97 % (2511367)CaDiCaL version: 2.1.3
% 108.90/15.97 % (2511367)Termination reason: Instruction limit
% 108.90/15.97 % (2511367)Termination phase: Saturation
% 108.90/15.97 % (2511367)Time elapsed: 2.694 s
% 108.90/15.97 % (2511367)Peak memory usage: 64 MB
% 108.90/15.97 % (2511367)Instructions burned: 5115 (million)
% 108.90/15.97 % (2511395)dis+10_16:1_sil=16000:random_seed=1632559692:i=9155:fsr=off_2966 on theBenchmark for (2966ds/9155Mi)
% 108.90/15.97 % (2511383)Instruction limit reached!
% 108.90/15.97 % (2511383)------------------------------
% 108.90/15.97 % (2511383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.90/15.97 % (2511383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.90/15.97 % (2511383)CaDiCaL version: 2.1.3
% 108.90/15.97 % (2511383)Termination reason: Instruction limit
% 108.90/15.97 % (2511383)Termination phase: Saturation
% 108.90/15.97 % (2511383)Time elapsed: 2.426 s
% 108.90/15.97 % (2511383)Peak memory usage: 33 MB
% 108.90/15.97 % (2511383)Instructions burned: 5212 (million)
% 108.90/15.97 % (2511397)ott-3_8_sil=64000:random_seed=1475621394:i=20139:bs=on_2949 on theBenchmark for (2949ds/20139Mi)
% 108.90/15.97 % (2511393)Instruction limit reached!
% 108.90/15.97 % (2511393)------------------------------
% 108.90/15.97 % (2511393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.90/15.97 % (2511393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.90/15.97 % (2511393)CaDiCaL version: 2.1.3
% 108.90/15.97 % (2511393)Termination reason: Instruction limit
% 108.90/15.97 % (2511393)Termination phase: Saturation
% 108.90/15.97 % (2511393)Time elapsed: 4.319 s
% 108.90/15.97 % (2511393)Peak memory usage: 104 MB
% 108.90/15.97 % (2511393)Instructions burned: 8173 (million)
% 108.90/15.97 % (2511399)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3643435930:fmbsr=2:i=32576_2926 on theBenchmark for (2926ds/32576Mi)
% 108.90/15.97 % Detected minimum model sizes of [3]
% 108.90/15.97 % Detected maximum model sizes of [max]
% 108.90/15.97 % (2511399)Cannot represent all propositional literals internally
% 108.90/15.97 % (2511399)Refutation not found, incomplete strategy
% 108.90/15.97 % (2511399)------------------------------
% 108.90/15.97 % (2511399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.90/15.97 % (2511399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.90/15.97 % (2511399)CaDiCaL version: 2.1.3
% 108.90/15.97 % (2511399)Termination reason: Refutation not found, incomplete strategy
% 108.90/15.97 % (2511399)Time elapsed: 0.036 s
% 108.90/15.97 % (2511399)Peak memory usage: 12 MB
% 108.90/15.97 % (2511399)Instructions burned: 72 (million)
% 108.90/15.97 % (2511399)------------------------------
% 108.90/15.97 % (2511399)------------------------------
% 108.90/15.97 % (2511401)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3868392229:i=11404_2925 on theBenchmark for (2925ds/11404Mi)
% 108.90/15.97 % (2511395)Instruction limit reached!
% 108.90/15.97 % (2511395)------------------------------
% 108.90/15.97 % (2511395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.90/15.97 % (2511395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.90/15.97 % (2511395)CaDiCaL version: 2.1.3
% 108.90/15.97 % (2511395)Termination reason: Instruction limit
% 108.90/15.97 % (2511395)Termination phase: Saturation
% 152.32/21.99 % (2511395)Time elapsed: 4.785 s
% 152.32/21.99 % (2511395)Peak memory usage: 67 MB
% 152.32/21.99 % (2511395)Instructions burned: 9156 (million)
% 152.32/21.99 % (2511403)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4138816504:i=14134_2918 on theBenchmark for (2918ds/14134Mi)
% 152.32/21.99 % (2511391)Instruction limit reached!
% 152.32/21.99 % (2511391)------------------------------
% 152.32/21.99 % (2511391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 152.32/21.99 % (2511391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.32/21.99 % (2511391)CaDiCaL version: 2.1.3
% 152.32/21.99 % (2511391)Termination reason: Instruction limit
% 152.32/21.99 % (2511391)Termination phase: Saturation
% 152.32/21.99 % (2511391)Time elapsed: 8.266 s
% 152.32/21.99 % (2511391)Peak memory usage: 119 MB
% 152.32/21.99 % (2511391)Instructions burned: 22567 (million)
% 152.32/21.99 % (2511405)dis+33_16_sil=32000:sac=on:random_seed=3330066850:i=15851:nm=0_2888 on theBenchmark for (2888ds/15851Mi)
% 152.32/21.99 % (2511401)Instruction limit reached!
% 152.32/21.99 % (2511401)------------------------------
% 152.32/21.99 % (2511401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 152.32/21.99 % (2511401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.32/21.99 % (2511401)CaDiCaL version: 2.1.3
% 152.32/21.99 % (2511401)Termination reason: Instruction limit
% 152.32/21.99 % (2511401)Termination phase: Saturation
% 152.32/21.99 % (2511401)Time elapsed: 6.173 s
% 152.32/21.99 % (2511401)Peak memory usage: 90 MB
% 152.32/21.99 % (2511401)Instructions burned: 11405 (million)
% 152.32/21.99 % (2511407)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1814015263:avsq=on:i=17627:add=on:amm=off_2863 on theBenchmark for (2863ds/17627Mi)
% 152.32/21.99 % (2511381)Instruction limit reached!
% 152.32/21.99 % (2511381)------------------------------
% 152.32/21.99 % (2511381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 152.32/21.99 % (2511381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.32/21.99 % (2511381)CaDiCaL version: 2.1.3
% 152.32/21.99 % (2511381)Termination reason: Instruction limit
% 152.32/21.99 % (2511381)Termination phase: Saturation
% 152.32/21.99 % (2511381)Time elapsed: 12.864 s
% 152.32/21.99 % (2511381)Peak memory usage: 441 MB
% 152.32/21.99 % (2511381)Instructions burned: 29340 (million)
% 152.32/21.99 % (2511409)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1303003073:s2a=on:i=53295_2850 on theBenchmark for (2850ds/53295Mi)
% 152.32/21.99 % (2511397)Instruction limit reached!
% 152.32/21.99 % (2511397)------------------------------
% 152.32/21.99 % (2511397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 152.32/21.99 % (2511397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.32/21.99 % (2511397)CaDiCaL version: 2.1.3
% 152.32/21.99 % (2511397)Termination reason: Instruction limit
% 152.32/21.99 % (2511397)Termination phase: Saturation
% 152.32/21.99 % (2511397)Time elapsed: 9.961 s
% 152.32/21.99 % (2511397)Peak memory usage: 79 MB
% 152.32/21.99 % (2511397)Instructions burned: 20139 (million)
% 152.32/21.99 % (2511411)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=283796324:i=26857:ins=20_2849 on theBenchmark for (2849ds/26857Mi)
% 152.32/21.99 % Detected minimum model sizes of [3]
% 152.32/21.99 % Detected maximum model sizes of [max]
% 152.32/21.99 % (2511411)Cannot represent all propositional literals internally
% 152.32/21.99 % (2511411)Refutation not found, incomplete strategy
% 152.32/21.99 % (2511411)------------------------------
% 152.32/21.99 % (2511411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 152.32/21.99 % (2511411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.32/21.99 % (2511411)CaDiCaL version: 2.1.3
% 152.32/21.99 % (2511411)Termination reason: Refutation not found, incomplete strategy
% 152.32/21.99 % (2511411)Time elapsed: 0.029 s
% 152.32/21.99 % (2511411)Peak memory usage: 12 MB
% 152.32/21.99 % (2511411)Instructions burned: 60 (million)
% 152.32/21.99 % (2511411)------------------------------
% 152.32/21.99 % (2511411)------------------------------
% 152.32/21.99 % (2511413)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1888973962:i=28120:bs=on:fsr=off_2848 on theBenchmark for (2848ds/28120Mi)
% 152.32/21.99 % (2511405)Instruction limit reached!
% 152.32/21.99 % (2511405)------------------------------
% 152.32/21.99 % (2511405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 152.32/21.99 % (2511405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.32/21.99 % (2511405)CaDiCaL version: 2.1.3
% 163.54/23.51 % (2511405)Termination reason: Instruction limit
% 163.54/23.51 % (2511405)Termination phase: Saturation
% 163.54/23.51 % (2511405)Time elapsed: 4.175 s
% 163.54/23.51 % (2511405)Peak memory usage: 166 MB
% 163.54/23.51 % (2511405)Instructions burned: 15852 (million)
% 163.54/23.51 % (2511415)fmb+10_1_sil=256000:fmbss=7:random_seed=2273953181:fmbsr=1.6:i=182295_2846 on theBenchmark for (2846ds/182295Mi)
% 163.54/23.51 % Detected minimum model sizes of [3]
% 163.54/23.51 % Detected maximum model sizes of [max]
% 163.54/23.51 % (2511415)Cannot represent all propositional literals internally
% 163.54/23.51 % (2511415)Refutation not found, incomplete strategy
% 163.54/23.51 % (2511415)------------------------------
% 163.54/23.51 % (2511415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.54/23.51 % (2511415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.54/23.51 % (2511415)CaDiCaL version: 2.1.3
% 163.54/23.51 % (2511415)Termination reason: Refutation not found, incomplete strategy
% 163.54/23.51 % (2511415)Time elapsed: 0.015 s
% 163.54/23.51 % (2511415)Peak memory usage: 12 MB
% 163.54/23.51 % (2511415)Instructions burned: 60 (million)
% 163.54/23.51 % (2511415)------------------------------
% 163.54/23.51 % (2511415)------------------------------
% 163.54/23.51 % (2511417)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2435854739:i=44625:gsp=on_2845 on theBenchmark for (2845ds/44625Mi)
% 163.54/23.51 % Detected minimum model sizes of [3]
% 163.54/23.51 % Detected maximum model sizes of [max]
% 163.54/23.51 % (2511417)Cannot represent all propositional literals internally
% 163.54/23.51 % (2511417)Refutation not found, incomplete strategy
% 163.54/23.51 % (2511417)------------------------------
% 163.54/23.51 % (2511417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.54/23.51 % (2511417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.54/23.51 % (2511417)CaDiCaL version: 2.1.3
% 163.54/23.51 % (2511417)Termination reason: Refutation not found, incomplete strategy
% 163.54/23.51 % (2511417)Time elapsed: 0.025 s
% 163.54/23.51 % (2511417)Peak memory usage: 12 MB
% 163.54/23.51 % (2511417)Instructions burned: 100 (million)
% 163.54/23.51 % (2511417)------------------------------
% 163.54/23.51 % (2511417)------------------------------
% 163.54/23.51 % (2511419)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3658921782:i=160505_2845 on theBenchmark for (2845ds/160505Mi)
% 163.54/23.51 % Detected minimum model sizes of [3]
% 163.54/23.51 % Detected maximum model sizes of [max]
% 163.54/23.51 % (2511419)Cannot represent all propositional literals internally
% 163.54/23.51 % (2511419)Refutation not found, incomplete strategy
% 163.54/23.51 % (2511419)------------------------------
% 163.54/23.51 % (2511419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.54/23.51 % (2511419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.54/23.51 % (2511419)CaDiCaL version: 2.1.3
% 163.54/23.51 % (2511419)Termination reason: Refutation not found, incomplete strategy
% 163.54/23.51 % (2511419)Time elapsed: 0.019 s
% 163.54/23.51 % (2511419)Peak memory usage: 12 MB
% 163.54/23.51 % (2511419)Instructions burned: 60 (million)
% 163.54/23.51 % (2511419)------------------------------
% 163.54/23.51 % (2511419)------------------------------
% 163.54/23.51 % (2511421)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1632941882:fmbsr=1.3:i=225729_2845 on theBenchmark for (2845ds/225729Mi)
% 163.54/23.51 % Detected minimum model sizes of [3]
% 163.54/23.51 % Detected maximum model sizes of [max]
% 163.54/23.51 % (2511421)Cannot represent all propositional literals internally
% 163.54/23.51 % (2511421)Refutation not found, incomplete strategy
% 163.54/23.51 % (2511421)------------------------------
% 163.54/23.51 % (2511421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.54/23.51 % (2511421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.54/23.51 % (2511421)CaDiCaL version: 2.1.3
% 163.54/23.51 % (2511421)Termination reason: Refutation not found, incomplete strategy
% 163.54/23.51 % (2511421)Time elapsed: 0.015 s
% 163.54/23.51 % (2511421)Peak memory usage: 12 MB
% 163.54/23.51 % (2511421)Instructions burned: 60 (million)
% 163.54/23.51 % (2511421)------------------------------
% 163.54/23.51 % (2511421)------------------------------
% 163.54/23.51 % (2511423)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1004134750:fmbsr=2:i=185024:ins=7_2844 on theBenchmark for (2844ds/185024Mi)
% 163.54/23.51 % Detected minimum model sizes of [3]
% 163.54/23.51 % Detected maximum model sizes of [max]
% 163.54/23.51 % (2511423)Cannot represent all propositional literals internally
% 163.54/23.51 % (2511423)Refutation not found, incomplete strategy
% 163.54/23.51 % (2511423)------------------------------
% 183.61/26.35 % (2511423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.61/26.35 % (2511423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.61/26.35 % (2511423)CaDiCaL version: 2.1.3
% 183.61/26.35 % (2511423)Termination reason: Refutation not found, incomplete strategy
% 183.61/26.35 % (2511423)Time elapsed: 0.016 s
% 183.61/26.35 % (2511423)Peak memory usage: 12 MB
% 183.61/26.35 % (2511423)Instructions burned: 60 (million)
% 183.61/26.35 % (2511423)------------------------------
% 183.61/26.35 % (2511423)------------------------------
% 183.61/26.35 % (2511425)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2130327328:rtra=on_2844 on theBenchmark for (2844ds/0Mi)
% 183.61/26.35 % Detected minimum model sizes of [3]
% 183.61/26.35 % Detected maximum model sizes of [max]
% 183.61/26.35 % (2511425)Cannot represent all propositional literals internally
% 183.61/26.35 % (2511425)Refutation not found, incomplete strategy
% 183.61/26.35 % (2511425)------------------------------
% 183.61/26.35 % (2511425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.61/26.35 % (2511425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.61/26.35 % (2511425)CaDiCaL version: 2.1.3
% 183.61/26.35 % (2511425)Termination reason: Refutation not found, incomplete strategy
% 183.61/26.35 % (2511425)Time elapsed: 0.027 s
% 183.61/26.35 % (2511425)Peak memory usage: 12 MB
% 183.61/26.35 % (2511425)Instructions burned: 75 (million)
% 183.61/26.35 % (2511425)------------------------------
% 183.61/26.35 % (2511425)------------------------------
% 183.61/26.35 % (2511427)% WARNING: option uhcvi not known.
% 183.61/26.35 % (2511427)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1868017432:i=271062:add=off:rtra=on:rawr=on_2844 on theBenchmark for (2844ds/271062Mi)
% 183.61/26.35 % (2511403)Instruction limit reached!
% 183.61/26.35 % (2511403)------------------------------
% 183.61/26.35 % (2511403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.61/26.35 % (2511403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.61/26.35 % (2511403)CaDiCaL version: 2.1.3
% 183.61/26.35 % (2511403)Termination reason: Instruction limit
% 183.61/26.35 % (2511403)Termination phase: Saturation
% 183.61/26.35 % (2511403)Time elapsed: 7.857 s
% 183.61/26.35 % (2511403)Peak memory usage: 136 MB
% 183.61/26.35 % (2511403)Instructions burned: 14134 (million)
% 183.61/26.35 % (2511429)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4210414198:i=176048:add=on:rtra=on:rawr=on_2839 on theBenchmark for (2839ds/176048Mi)
% 183.61/26.35 % (2511407)Instruction limit reached!
% 183.61/26.35 % (2511407)------------------------------
% 183.61/26.35 % (2511407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.61/26.35 % (2511407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.61/26.35 % (2511407)CaDiCaL version: 2.1.3
% 183.61/26.35 % (2511407)Termination reason: Instruction limit
% 183.61/26.35 % (2511407)Termination phase: Saturation
% 183.61/26.35 % (2511407)Time elapsed: 7.617 s
% 183.61/26.35 % (2511407)Peak memory usage: 94 MB
% 183.61/26.35 % (2511407)Instructions burned: 17627 (million)
% 183.61/26.35 % (2511431)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2866220449:i=206:fgj=on:rtra=on_2787 on theBenchmark for (2787ds/206Mi)
% 183.61/26.35 % (2511431)Instruction limit reached!
% 183.61/26.35 % (2511431)------------------------------
% 183.61/26.35 % (2511431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.61/26.35 % (2511431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.61/26.35 % (2511431)CaDiCaL version: 2.1.3
% 183.61/26.35 % (2511431)Termination reason: Instruction limit
% 183.61/26.35 % (2511431)Termination phase: Saturation
% 183.61/26.35 % (2511431)Time elapsed: 0.123 s
% 183.61/26.35 % (2511431)Peak memory usage: 14 MB
% 183.61/26.35 % (2511431)Instructions burned: 207 (million)
% 183.61/26.35 % (2511433)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1002431538:i=232:rtra=on_2785 on theBenchmark for (2785ds/232Mi)
% 183.61/26.35 % (2511433)Instruction limit reached!
% 183.61/26.35 % (2511433)------------------------------
% 183.61/26.35 % (2511433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.61/26.35 % (2511433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.61/26.35 % (2511433)CaDiCaL version: 2.1.3
% 183.61/26.35 % (2511433)Termination reason: Instruction limit
% 183.61/26.35 % (2511433)Termination phase: Saturation
% 183.61/26.35 % (2511433)Time elapsed: 0.130 s
% 183.61/26.35 % (2511433)Peak memory usage: 16 MB
% 107.69/33.25 % (2511433)Instructions burned: 233 (million)
% 107.69/33.25 % (2511435)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=604081582:i=262:rtra=on_2784 on theBenchmark for (2784ds/262Mi)
% 107.69/33.25 % (2511435)Instruction limit reached!
% 107.69/33.25 % (2511435)------------------------------
% 107.69/33.25 % (2511435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511435)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511435)Termination reason: Instruction limit
% 107.69/33.25 % (2511435)Termination phase: Saturation
% 107.69/33.25 % (2511435)Time elapsed: 0.134 s
% 107.69/33.25 % (2511435)Peak memory usage: 14 MB
% 107.69/33.25 % (2511435)Instructions burned: 263 (million)
% 107.69/33.25 % (2511437)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=500539916:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2782 on theBenchmark for (2782ds/318Mi)
% 107.69/33.25 % (2511437)Instruction limit reached!
% 107.69/33.25 % (2511437)------------------------------
% 107.69/33.25 % (2511437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511437)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511437)Termination reason: Instruction limit
% 107.69/33.25 % (2511437)Termination phase: Saturation
% 107.69/33.25 % (2511437)Time elapsed: 0.195 s
% 107.69/33.25 % (2511437)Peak memory usage: 19 MB
% 107.69/33.25 % (2511437)Instructions burned: 319 (million)
% 107.69/33.25 % (2511439)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3828846523:i=1428:nm=2:rtra=on_2780 on theBenchmark for (2780ds/1428Mi)
% 107.69/33.25 % Detected minimum model sizes of [3]
% 107.69/33.25 % Detected maximum model sizes of [max]
% 107.69/33.25 % (2511439)Cannot represent all propositional literals internally
% 107.69/33.25 % (2511439)Refutation not found, incomplete strategy
% 107.69/33.25 % (2511439)------------------------------
% 107.69/33.25 % (2511439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511439)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511439)Termination reason: Refutation not found, incomplete strategy
% 107.69/33.25 % (2511439)Time elapsed: 0.032 s
% 107.69/33.25 % (2511439)Peak memory usage: 12 MB
% 107.69/33.25 % (2511439)Instructions burned: 61 (million)
% 107.69/33.25 % (2511439)------------------------------
% 107.69/33.25 % (2511439)------------------------------
% 107.69/33.25 % (2511441)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3416767899:i=262:bd=preordered:rtra=on:fsd=on_2780 on theBenchmark for (2780ds/262Mi)
% 107.69/33.25 % (2511441)Instruction limit reached!
% 107.69/33.25 % (2511441)------------------------------
% 107.69/33.25 % (2511441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511441)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511441)Termination reason: Instruction limit
% 107.69/33.25 % (2511441)Termination phase: Saturation
% 107.69/33.25 % (2511441)Time elapsed: 0.114 s
% 107.69/33.25 % (2511441)Peak memory usage: 13 MB
% 107.69/33.25 % (2511441)Instructions burned: 264 (million)
% 107.69/33.25 % (2511443)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=137928643:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2778 on theBenchmark for (2778ds/1368Mi)
% 107.69/33.25 % (2511443)Instruction limit reached!
% 107.69/33.25 % (2511443)------------------------------
% 107.69/33.25 % (2511443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511443)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511443)Termination reason: Instruction limit
% 107.69/33.25 % (2511443)Termination phase: Saturation
% 107.69/33.25 % (2511443)Time elapsed: 0.721 s
% 107.69/33.25 % (2511443)Peak memory usage: 30 MB
% 107.69/33.25 % (2511443)Instructions burned: 1369 (million)
% 107.69/33.25 % (2511445)ott-21_1_sil=16000:si=on:fs=off:random_seed=3317193283:i=360:av=off:fsr=off:rtra=on_2771 on theBenchmark for (2771ds/360Mi)
% 107.69/33.25 % (2511445)Instruction limit reached!
% 107.69/33.25 % (2511445)------------------------------
% 107.69/33.25 % (2511445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511445)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511445)Termination reason: Instruction limit
% 107.69/33.25 % (2511445)Termination phase: Saturation
% 107.69/33.25 % (2511445)Time elapsed: 0.197 s
% 107.69/33.25 % (2511445)Peak memory usage: 16 MB
% 107.69/33.25 % (2511445)Instructions burned: 361 (million)
% 107.69/33.25 % (2511447)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3354826323:i=954:bd=all:rtra=on_2769 on theBenchmark for (2769ds/954Mi)
% 107.69/33.25 % (2511447)Instruction limit reached!
% 107.69/33.25 % (2511447)------------------------------
% 107.69/33.25 % (2511447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511447)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511447)Termination reason: Instruction limit
% 107.69/33.25 % (2511447)Termination phase: Saturation
% 107.69/33.25 % (2511447)Time elapsed: 0.597 s
% 107.69/33.25 % (2511447)Peak memory usage: 18 MB
% 107.69/33.25 % (2511447)Instructions burned: 955 (million)
% 107.69/33.25 % (2511449)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3360378921:fmbsr=1.3:i=1730:ins=25:rtra=on_2762 on theBenchmark for (2762ds/1730Mi)
% 107.69/33.25 % Detected minimum model sizes of [3]
% 107.69/33.25 % Detected maximum model sizes of [max]
% 107.69/33.25 % (2511449)Cannot represent all propositional literals internally
% 107.69/33.25 % (2511449)Refutation not found, incomplete strategy
% 107.69/33.25 % (2511449)------------------------------
% 107.69/33.25 % (2511449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511449)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511449)Termination reason: Refutation not found, incomplete strategy
% 107.69/33.25 % (2511449)Time elapsed: 0.033 s
% 107.69/33.25 % (2511449)Peak memory usage: 12 MB
% 107.69/33.25 % (2511449)Instructions burned: 63 (million)
% 107.69/33.25 % (2511449)------------------------------
% 107.69/33.25 % (2511449)------------------------------
% 107.69/33.25 % (2511451)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2438269092:i=2358:rtra=on_2762 on theBenchmark for (2762ds/2358Mi)
% 107.69/33.25 % (2511451)Instruction limit reached!
% 107.69/33.25 % (2511451)------------------------------
% 107.69/33.25 % (2511451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511451)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511451)Termination reason: Instruction limit
% 107.69/33.25 % (2511451)Termination phase: Saturation
% 107.69/33.25 % (2511451)Time elapsed: 1.365 s
% 107.69/33.25 % (2511451)Peak memory usage: 30 MB
% 107.69/33.25 % (2511451)Instructions burned: 2358 (million)
% 107.69/33.25 % (2511453)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1722190729:i=1778:ins=1:rtra=on_2748 on theBenchmark for (2748ds/1778Mi)
% 107.69/33.25 % (2511453)Cannot represent all propositional literals internally
% 107.69/33.25 % (2511453)Refutation not found, incomplete strategy
% 107.69/33.25 % (2511453)------------------------------
% 107.69/33.25 % (2511453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511453)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511453)Termination reason: Refutation not found, incomplete strategy
% 107.69/33.25 % (2511453)Time elapsed: 0.033 s
% 107.69/33.25 % (2511453)Peak memory usage: 12 MB
% 107.69/33.25 % (2511453)Instructions burned: 62 (million)
% 107.69/33.25 % (2511453)------------------------------
% 107.69/33.25 % (2511453)------------------------------
% 107.69/33.25 % (2511455)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3294430595:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2748 on theBenchmark for (2748ds/1384Mi)
% 107.69/33.25 % (2511455)Instruction limit reached!
% 107.69/33.25 % (2511455)------------------------------
% 107.69/33.25 % (2511455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511455)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511455)Termination reason: Instruction limit
% 107.69/33.25 % (2511455)Termination phase: Saturation
% 107.69/33.25 % (2511455)Time elapsed: 0.707 s
% 107.69/33.25 % (2511455)Peak memory usage: 19 MB
% 107.69/33.25 % (2511455)Instructions burned: 1384 (million)
% 107.69/33.25 % (2511457)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3171262561:i=1758:kws=inv_precedence:fsr=off:rtra=on_2740 on theBenchmark for (2740ds/1758Mi)
% 107.69/33.25 % (2511457)Instruction limit reached!
% 107.69/33.25 % (2511457)------------------------------
% 107.69/33.25 % (2511457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511457)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511457)Termination reason: Instruction limit
% 107.69/33.25 % (2511457)Termination phase: Saturation
% 107.69/33.25 % (2511457)Time elapsed: 0.959 s
% 107.69/33.25 % (2511457)Peak memory usage: 27 MB
% 107.69/33.25 % (2511457)Instructions burned: 1759 (million)
% 107.69/33.25 % (2511459)fmb+10_1_sil=64000:si=on:random_seed=721162589:i=44122:nm=2:rtra=on:gsp=on_2730 on theBenchmark for (2730ds/44122Mi)
% 107.69/33.25 % Detected minimum model sizes of [3]
% 107.69/33.25 % Detected maximum model sizes of [max]
% 107.69/33.25 % (2511459)Cannot represent all propositional literals internally
% 107.69/33.25 % (2511459)Refutation not found, incomplete strategy
% 107.69/33.25 % (2511459)------------------------------
% 107.69/33.25 % (2511459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511459)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511459)Termination reason: Refutation not found, incomplete strategy
% 107.69/33.25 % (2511459)Time elapsed: 0.031 s
% 107.69/33.25 % (2511459)Peak memory usage: 12 MB
% 107.69/33.25 % (2511459)Instructions burned: 58 (million)
% 107.69/33.25 % (2511459)------------------------------
% 107.69/33.25 % (2511459)------------------------------
% 107.69/33.25 % (2511461)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=4221810641:i=19030:nm=5:rtra=on_2730 on theBenchmark for (2730ds/19030Mi)
% 107.69/33.25 % Detected minimum model sizes of [3]
% 107.69/33.25 % Detected maximum model sizes of [max]
% 107.69/33.25 % (2511461)Cannot represent all propositional literals internally
% 107.69/33.25 % (2511461)Refutation not found, incomplete strategy
% 107.69/33.25 % (2511461)------------------------------
% 107.69/33.25 % (2511461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511461)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511461)Termination reason: Refutation not found, incomplete strategy
% 107.69/33.25 % (2511461)Time elapsed: 0.033 s
% 107.69/33.25 % (2511461)Peak memory usage: 12 MB
% 107.69/33.25 % (2511461)Instructions burned: 62 (million)
% 107.69/33.25 % (2511461)------------------------------
% 107.69/33.25 % (2511461)------------------------------
% 107.69/33.25 % (2511463)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2936074414:fmbsr=1.7:i=1840:rtra=on_2729 on theBenchmark for (2729ds/1840Mi)
% 107.69/33.25 % Detected minimum model sizes of [3]
% 107.69/33.25 % Detected maximum model sizes of [max]
% 107.69/33.25 % (2511463)Cannot represent all propositional literals internally
% 107.69/33.25 % (2511463)Refutation not found, incomplete strategy
% 107.69/33.25 % (2511463)------------------------------
% 107.69/33.25 % (2511463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.25 % (2511463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.25 % (2511463)CaDiCaL version: 2.1.3
% 107.69/33.25 % (2511463)Termination reason: Refutation not found, incomplete strategy
% 107.69/33.25 % (2511463)Time elapsed: 0.033 s
% 107.69/33.25 % (2511463)Peak memory usage: 12 MB
% 107.69/33.25 % (2511463)Instructions burned: 62 (million)
% 107.69/33.25 % (2511463)------------------------------
% 107.69/33.25 % (2511463)------------------------------
% 107.69/33.25 % (2511465)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=605866891:i=10262:rtra=on_2729 on theBenchmark for (2729ds/10262Mi)
% 107.69/33.25 % (2511427) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2511312-2511427"...
% 107.69/33.25 % (2511427)...printing done.
% 107.69/33.25 % (2511427)Refutation found. Thanks to Tanya!
% 107.69/33.25 % SZS status ContradictoryAxioms for theBenchmark
% 107.69/33.25 % SZS output start Proof for theBenchmark
% See solution above
% 107.69/33.26 % (2511427)------------------------------
% 107.69/33.26 % (2511427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.69/33.26 % (2511427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.69/33.26 % (2511427)CaDiCaL version: 2.1.3
% 107.69/33.26 % (2511427)Termination reason: Refutation
% 107.69/33.26 % (2511427)Time elapsed: 17.129 s
% 107.69/33.26 % (2511427)Peak memory usage: 246 MB
% 107.69/33.26 % (2511427)Instructions burned: 55575 (million)
% 107.69/33.26 % (2511312)Success in time 32.826 s
% 107.69/33.26 % Vampire exiting
%------------------------------------------------------------------------------