%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GEO294+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 : Theorem 16.58s 2.82s
% Output : Refutation 16.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 30
% Syntax : Number of formulae : 210 ( 66 unt; 10 def)
% Number of atoms : 1174 ( 330 equ)
% Maximal formula atoms : 22 ( 5 avg)
% Number of connectives : 1715 ( 751 ~; 819 |; 127 &)
% ( 13 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 11 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 21 con; 0-3 aty)
% Number of variables : 391 ( 0 sgn 364 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
ron(vd1201,vd1232),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(303, 0)') ).
fof(f2,negated_conjecture,
~ ron(vd1201,vd1232),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
vangle(vd1201,vd1185,vd1187) = v0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(302, 1241, 0)') ).
fof(f7,axiom,
vd1199 = vd1185,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(291, 1230, 0)') ).
fof(f9,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ron(X2,X6)
& ron(X0,X6)
& X0 != X4
& X0 != X2
& X6 = X7
& rline(X7)
& X4 = X5
& rpoint(X5)
& X2 = X3
& rpoint(X3)
& X0 = X1
& rpoint(X1) )
=> ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
<=> vangle(X2,X0,X4) = v0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(188), 0), imp(cond(axiom(188), 0)))') ).
fof(f16,axiom,
( ~ ? [X0] :
( ron(vd1187,X0)
& ron(vd1186,X0)
& ron(vd1185,X0)
& rline(X0) )
& vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187)
& vf(vd1178,vd1180) = vf(vd1185,vd1187)
& vf(vd1178,vd1179) = vf(vd1185,vd1186)
& ? [X1] :
( vd1187 = X1
& rpoint(X1) )
& ? [X2] :
( vd1186 = X2
& rpoint(X2) )
& ? [X3] :
( vd1185 = X3
& rpoint(X3) )
& vd1179 != vd1180
& vd1178 != vd1180
& vd1178 != vd1179
& ? [X4] :
( vd1180 = X4
& rpoint(X4) )
& ? [X5] :
( vd1179 = X5
& rpoint(X5) )
& ? [X6] :
( vd1178 = X6
& rpoint(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(f21,axiom,
ron(vd1199,vd1197),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(conjunct1(conjunct2(comma_conjunct2(plural(271)))), 0)') ).
fof(f27,axiom,
? [X0] :
( vd1201 = X0
& rpoint(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qe(s3(plural(271)))') ).
fof(f29,axiom,
? [X0] :
( vd1199 = X0
& rpoint(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qe(s1(plural(271)))') ).
fof(f35,axiom,
ron(vd1201,vd1234),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(s2(plural(294)), 0)') ).
fof(f36,axiom,
ron(vd1185,vd1234),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(s1(plural(294)), 0)') ).
fof(f37,axiom,
rline(vd1234),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(294, 0)') ).
fof(f38,axiom,
ron(vd1187,vd1232),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(s2(plural(293)), 0)') ).
fof(f39,axiom,
ron(vd1185,vd1232),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(s1(plural(293)), 0)') ).
fof(f40,axiom,
rline(vd1232),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(293, 0)') ).
fof(f50,axiom,
~ ron(vd1187,vd1197),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','neg(neg(270))') ).
fof(f60,axiom,
v0 = vd684,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','pred(axiom(137), 2)') ).
fof(f83,axiom,
! [X0,X1,X2,X3,X4] :
( ( X3 = X4
& ron(X2,X3)
& ron(X1,X3)
& ron(X0,X3)
& rline(X4)
& X1 != X2
& X0 != X2
& X0 != X1
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> ( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(91), 0), imp(cond(axiom(91), 0)))') ).
fof(f86,axiom,
! [X0,X1,X2,X3,X4] :
( ( X3 = X4
& ron(X2,X3)
& ron(X0,X3)
& rR(X1,X0,X2)
& rline(X4)
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> ron(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(85), 0), imp(cond(axiom(85), 0)))') ).
fof(f87,axiom,
! [X0,X1,X2,X3,X4] :
( ( X3 = X4
& ron(X1,X3)
& ron(X0,X3)
& rR(X1,X0,X2)
& rline(X4)
& ? [X5] :
( X2 = X5
& rpoint(X5) )
& ? [X6] :
( X1 = X6
& rpoint(X6) )
& ? [X7] :
( X0 = X7
& rpoint(X7) ) )
=> ron(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(83), 0), imp(cond(axiom(83), 0)))') ).
fof(f88,axiom,
! [X0,X1,X2] :
( ( rR(X1,X0,X2)
& ? [X3] :
( X2 = X3
& rpoint(X3) )
& ? [X4] :
( X1 = X4
& rpoint(X4) )
& ? [X5] :
( X0 = X5
& rpoint(X5) ) )
=> ( ~ rR(X0,X1,X2)
& X0 != X2
& X0 != X1
& rR(X1,X2,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(axiom(81), 0), imp(cond(axiom(81), 0)))') ).
fof(f156,plain,
~ ron(vd1201,vd1232),
inference(flattening,[],[f2]) ).
fof(f161,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
<=> vangle(X2,X0,X4) = v0 )
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f162,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
<=> vangle(X2,X0,X4) = v0 )
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(flattening,[],[f161]) ).
fof(f169,plain,
( ! [X0] :
( ~ ron(vd1187,X0)
| ~ ron(vd1186,X0)
| ~ ron(vd1185,X0)
| ~ rline(X0) )
& vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187)
& vf(vd1178,vd1180) = vf(vd1185,vd1187)
& vf(vd1178,vd1179) = vf(vd1185,vd1186)
& ? [X1] :
( vd1187 = X1
& rpoint(X1) )
& ? [X2] :
( vd1186 = X2
& rpoint(X2) )
& ? [X3] :
( vd1185 = X3
& rpoint(X3) )
& vd1179 != vd1180
& vd1178 != vd1180
& vd1178 != vd1179
& ? [X4] :
( vd1180 = X4
& rpoint(X4) )
& ? [X5] :
( vd1179 = X5
& rpoint(X5) )
& ? [X6] :
( vd1178 = X6
& rpoint(X6) ) ),
inference(ennf_transformation,[],[f16]) ).
fof(f238,plain,
! [X0,X1,X2,X3,X4] :
( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rline(X4)
| X1 = X2
| X0 = X2
| X0 = X1
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f83]) ).
fof(f239,plain,
! [X0,X1,X2,X3,X4] :
( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rline(X4)
| X1 = X2
| X0 = X2
| X0 = X1
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f238]) ).
fof(f244,plain,
! [X0,X1,X2,X3,X4] :
( ron(X1,X3)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f86]) ).
fof(f245,plain,
! [X0,X1,X2,X3,X4] :
( ron(X1,X3)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f244]) ).
fof(f246,plain,
! [X0,X1,X2,X3,X4] :
( ron(X2,X3)
| X3 != X4
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(ennf_transformation,[],[f87]) ).
fof(f247,plain,
! [X0,X1,X2,X3,X4] :
( ron(X2,X3)
| X3 != X4
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| ! [X5] :
( X2 != X5
| ~ rpoint(X5) )
| ! [X6] :
( X1 != X6
| ~ rpoint(X6) )
| ! [X7] :
( X0 != X7
| ~ rpoint(X7) ) ),
inference(flattening,[],[f246]) ).
fof(f248,plain,
! [X0,X1,X2] :
( ( ~ rR(X0,X1,X2)
& X0 != X2
& X0 != X1
& rR(X1,X2,X0) )
| ~ rR(X1,X0,X2)
| ! [X3] :
( X2 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X1 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X0 != X5
| ~ rpoint(X5) ) ),
inference(ennf_transformation,[],[f88]) ).
fof(f249,plain,
! [X0,X1,X2] :
( ( ~ rR(X0,X1,X2)
& X0 != X2
& X0 != X1
& rR(X1,X2,X0) )
| ~ rR(X1,X0,X2)
| ! [X3] :
( X2 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X1 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X0 != X5
| ~ rpoint(X5) ) ),
inference(flattening,[],[f248]) ).
fof(f374,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
| v0 != vangle(X2,X0,X4) )
& ( vangle(X2,X0,X4) = v0
| rR(X0,X2,X4)
| ~ ron(X4,X6) ) )
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(nnf_transformation,[],[f162]) ).
fof(f375,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ( ( ~ rR(X0,X2,X4)
& ron(X4,X6) )
| v0 != vangle(X2,X0,X4) )
& ( vangle(X2,X0,X4) = v0
| rR(X0,X2,X4)
| ~ ron(X4,X6) ) )
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(flattening,[],[f374]) ).
fof(f376,plain,
( ! [X0] :
( ~ ron(vd1187,X0)
| ~ ron(vd1186,X0)
| ~ ron(vd1185,X0)
| ~ rline(X0) )
& vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187)
& vf(vd1178,vd1180) = vf(vd1185,vd1187)
& vf(vd1178,vd1179) = vf(vd1185,vd1186)
& vd1187 = sK1
& rpoint(sK1)
& vd1186 = sK2
& rpoint(sK2)
& vd1185 = sK3
& rpoint(sK3)
& vd1179 != vd1180
& vd1178 != vd1180
& vd1178 != vd1179
& vd1180 = sK4
& rpoint(sK4)
& vd1179 = sK5
& rpoint(sK5)
& vd1178 = sK6
& rpoint(sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6]),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6)],[f169]) ).
fof(f377,plain,
( vd1201 = sK7
& rpoint(sK7) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X0,sK7)],[f27]) ).
fof(f379,plain,
( vd1199 = sK9
& rpoint(sK9) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X0,sK9)],[f29]) ).
fof(f450,plain,
~ ron(vd1201,vd1232),
inference(cnf_transformation,[],[f156]) ).
fof(f451,plain,
vangle(vd1201,vd1185,vd1187) = v0,
inference(cnf_transformation,[],[f3]) ).
fof(f455,plain,
vd1185 = vd1199,
inference(cnf_transformation,[],[f7]) ).
fof(f458,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ron(X4,X6)
| v0 != vangle(X2,X0,X4)
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(cnf_transformation,[],[f375]) ).
fof(f459,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rR(X0,X2,X4)
| v0 != vangle(X2,X0,X4)
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(cnf_transformation,[],[f375]) ).
fof(f475,plain,
rpoint(sK3),
inference(cnf_transformation,[],[f376]) ).
fof(f476,plain,
vd1185 = sK3,
inference(cnf_transformation,[],[f376]) ).
fof(f479,plain,
rpoint(sK1),
inference(cnf_transformation,[],[f376]) ).
fof(f480,plain,
vd1187 = sK1,
inference(cnf_transformation,[],[f376]) ).
fof(f489,plain,
ron(vd1199,vd1197),
inference(cnf_transformation,[],[f21]) ).
fof(f495,plain,
rpoint(sK7),
inference(cnf_transformation,[],[f377]) ).
fof(f496,plain,
vd1201 = sK7,
inference(cnf_transformation,[],[f377]) ).
fof(f500,plain,
vd1199 = sK9,
inference(cnf_transformation,[],[f379]) ).
fof(f506,plain,
ron(vd1201,vd1234),
inference(cnf_transformation,[],[f35]) ).
fof(f507,plain,
ron(vd1185,vd1234),
inference(cnf_transformation,[],[f36]) ).
fof(f508,plain,
rline(vd1234),
inference(cnf_transformation,[],[f37]) ).
fof(f509,plain,
ron(vd1187,vd1232),
inference(cnf_transformation,[],[f38]) ).
fof(f510,plain,
ron(vd1185,vd1232),
inference(cnf_transformation,[],[f39]) ).
fof(f511,plain,
rline(vd1232),
inference(cnf_transformation,[],[f40]) ).
fof(f524,plain,
~ ron(vd1187,vd1197),
inference(cnf_transformation,[],[f50]) ).
fof(f536,plain,
v0 = vd684,
inference(cnf_transformation,[],[f60]) ).
fof(f569,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rline(X4)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f239]) ).
fof(f572,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ron(X1,X3)
| X3 != X4
| ~ ron(X2,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f245]) ).
fof(f573,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ron(X2,X3)
| X3 != X4
| ~ ron(X1,X3)
| ~ ron(X0,X3)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(cnf_transformation,[],[f247]) ).
fof(f574,plain,
! [X2,X3,X0,X1,X4,X5] :
( rR(X1,X2,X0)
| ~ rR(X1,X0,X2)
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(cnf_transformation,[],[f249]) ).
fof(f577,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ rR(X0,X1,X2)
| ~ rR(X1,X0,X2)
| X2 != X3
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(cnf_transformation,[],[f249]) ).
fof(f748,plain,
vd1185 = sK9,
inference(definition_unfolding,[],[f455,f500]) ).
fof(f750,plain,
~ ron(sK7,vd1232),
inference(definition_unfolding,[],[f450,f496]) ).
fof(f751,plain,
vd684 = vangle(sK7,sK9,sK1),
inference(definition_unfolding,[],[f451,f496,f748,f480,f536]) ).
fof(f755,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ rR(X0,X2,X4)
| vangle(X2,X0,X4) != vd684
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(definition_unfolding,[],[f459,f536]) ).
fof(f756,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ron(X4,X6)
| vangle(X2,X0,X4) != vd684
| ~ ron(X2,X6)
| ~ ron(X0,X6)
| X0 = X4
| X0 = X2
| X6 != X7
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(definition_unfolding,[],[f458,f536]) ).
fof(f768,plain,
sK3 = sK9,
inference(definition_unfolding,[],[f476,f748]) ).
fof(f776,plain,
ron(sK9,vd1197),
inference(definition_unfolding,[],[f489,f500]) ).
fof(f787,plain,
ron(sK7,vd1234),
inference(definition_unfolding,[],[f506,f496]) ).
fof(f788,plain,
ron(sK9,vd1234),
inference(definition_unfolding,[],[f507,f748]) ).
fof(f789,plain,
ron(sK1,vd1232),
inference(definition_unfolding,[],[f509,f480]) ).
fof(f790,plain,
ron(sK9,vd1232),
inference(definition_unfolding,[],[f510,f748]) ).
fof(f796,plain,
~ ron(sK1,vd1197),
inference(definition_unfolding,[],[f524,f480]) ).
fof(f803,plain,
! [X2,X3,X0,X1,X7,X4,X5] :
( ~ rR(X0,X2,X4)
| vangle(X2,X0,X4) != vd684
| ~ ron(X2,X7)
| ~ ron(X0,X7)
| X0 = X4
| X0 = X2
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f755]) ).
fof(f804,plain,
! [X2,X3,X0,X1,X7,X5] :
( ~ rR(X0,X2,X5)
| vd684 != vangle(X2,X0,X5)
| ~ ron(X2,X7)
| ~ ron(X0,X7)
| X0 = X5
| X0 = X2
| ~ rline(X7)
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f803]) ).
fof(f805,plain,
! [X3,X0,X1,X7,X5] :
( ~ rR(X0,X3,X5)
| vd684 != vangle(X3,X0,X5)
| ~ ron(X3,X7)
| ~ ron(X0,X7)
| X0 = X5
| X0 = X3
| ~ rline(X7)
| ~ rpoint(X5)
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f804]) ).
fof(f806,plain,
! [X3,X1,X7,X5] :
( vd684 != vangle(X3,X1,X5)
| ~ rR(X1,X3,X5)
| ~ ron(X3,X7)
| ~ ron(X1,X7)
| X1 = X5
| X1 = X3
| ~ rline(X7)
| ~ rpoint(X5)
| ~ rpoint(X3)
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f805]) ).
fof(f807,plain,
! [X2,X3,X0,X1,X7,X4,X5] :
( ron(X4,X7)
| vangle(X2,X0,X4) != vd684
| ~ ron(X2,X7)
| ~ ron(X0,X7)
| X0 = X4
| X0 = X2
| ~ rline(X7)
| X4 != X5
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f756]) ).
fof(f808,plain,
! [X2,X3,X0,X1,X7,X5] :
( ron(X5,X7)
| vd684 != vangle(X2,X0,X5)
| ~ ron(X2,X7)
| ~ ron(X0,X7)
| X0 = X5
| X0 = X2
| ~ rline(X7)
| ~ rpoint(X5)
| X2 != X3
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f807]) ).
fof(f809,plain,
! [X3,X0,X1,X7,X5] :
( ron(X5,X7)
| vd684 != vangle(X3,X0,X5)
| ~ ron(X3,X7)
| ~ ron(X0,X7)
| X0 = X5
| X0 = X3
| ~ rline(X7)
| ~ rpoint(X5)
| ~ rpoint(X3)
| X0 != X1
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f808]) ).
fof(f810,plain,
! [X3,X1,X7,X5] :
( vd684 != vangle(X3,X1,X5)
| ron(X5,X7)
| ~ ron(X3,X7)
| ~ ron(X1,X7)
| X1 = X5
| X1 = X3
| ~ rline(X7)
| ~ rpoint(X5)
| ~ rpoint(X3)
| ~ rpoint(X1) ),
inference(equality_resolution,[],[f809]) ).
fof(f1000,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( rR(X1,X0,X2)
| rR(X0,X1,X2)
| rR(X2,X0,X1)
| ~ ron(X2,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rline(X4)
| X1 = X2
| X0 = X2
| X0 = X1
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f569]) ).
fof(f1001,plain,
! [X0,X1,X6,X7,X4,X5] :
( rR(X1,X0,X5)
| rR(X0,X1,X5)
| rR(X5,X0,X1)
| ~ ron(X5,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rline(X4)
| X1 = X5
| X0 = X5
| X0 = X1
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1000]) ).
fof(f1002,plain,
! [X0,X6,X7,X4,X5] :
( rR(X6,X0,X5)
| rR(X0,X6,X5)
| rR(X5,X0,X6)
| ~ ron(X5,X4)
| ~ ron(X6,X4)
| ~ ron(X0,X4)
| ~ rline(X4)
| X5 = X6
| X0 = X5
| X0 = X6
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1001]) ).
fof(f1003,plain,
! [X6,X7,X4,X5] :
( rR(X6,X7,X5)
| rR(X7,X6,X5)
| rR(X5,X7,X6)
| ~ ron(X5,X4)
| ~ ron(X6,X4)
| ~ ron(X7,X4)
| ~ rline(X4)
| X5 = X6
| X5 = X7
| X6 = X7
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1002]) ).
fof(f1012,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ron(X1,X4)
| ~ ron(X2,X4)
| ~ ron(X0,X4)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f572]) ).
fof(f1013,plain,
! [X0,X1,X6,X7,X4,X5] :
( ron(X1,X4)
| ~ ron(X5,X4)
| ~ ron(X0,X4)
| ~ rR(X1,X0,X5)
| ~ rline(X4)
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1012]) ).
fof(f1014,plain,
! [X0,X6,X7,X4,X5] :
( ron(X6,X4)
| ~ ron(X5,X4)
| ~ ron(X0,X4)
| ~ rR(X6,X0,X5)
| ~ rline(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1013]) ).
fof(f1015,plain,
! [X6,X7,X4,X5] :
( ron(X6,X4)
| ~ ron(X5,X4)
| ~ ron(X7,X4)
| ~ rR(X6,X7,X5)
| ~ rline(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1014]) ).
fof(f1016,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ron(X2,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rR(X1,X0,X2)
| ~ rline(X4)
| X2 != X5
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f573]) ).
fof(f1017,plain,
! [X0,X1,X6,X7,X4,X5] :
( ron(X5,X4)
| ~ ron(X1,X4)
| ~ ron(X0,X4)
| ~ rR(X1,X0,X5)
| ~ rline(X4)
| ~ rpoint(X5)
| X1 != X6
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1016]) ).
fof(f1018,plain,
! [X0,X6,X7,X4,X5] :
( ron(X5,X4)
| ~ ron(X6,X4)
| ~ ron(X0,X4)
| ~ rR(X6,X0,X5)
| ~ rline(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| X0 != X7
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1017]) ).
fof(f1019,plain,
! [X6,X7,X4,X5] :
( ron(X5,X4)
| ~ ron(X6,X4)
| ~ ron(X7,X4)
| ~ rR(X6,X7,X5)
| ~ rline(X4)
| ~ rpoint(X5)
| ~ rpoint(X6)
| ~ rpoint(X7) ),
inference(equality_resolution,[],[f1018]) ).
fof(f1020,plain,
! [X3,X0,X1,X4,X5] :
( ~ rR(X0,X1,X3)
| ~ rR(X1,X0,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f577]) ).
fof(f1021,plain,
! [X3,X0,X4,X5] :
( ~ rR(X0,X4,X3)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1020]) ).
fof(f1022,plain,
! [X3,X4,X5] :
( ~ rR(X5,X4,X3)
| ~ rR(X4,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1021]) ).
fof(f1031,plain,
! [X3,X0,X1,X4,X5] :
( rR(X1,X3,X0)
| ~ rR(X1,X0,X3)
| ~ rpoint(X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f574]) ).
fof(f1032,plain,
! [X3,X0,X4,X5] :
( rR(X4,X3,X0)
| ~ rR(X4,X0,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1031]) ).
fof(f1033,plain,
! [X3,X4,X5] :
( rR(X4,X3,X5)
| ~ rR(X4,X5,X3)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f1032]) ).
fof(f1560,plain,
ron(sK3,vd1197),
inference(forward_demodulation,[],[f776,f768]) ).
fof(f1563,plain,
ron(sK3,vd1234),
inference(forward_demodulation,[],[f788,f768]) ).
fof(f1564,plain,
ron(sK3,vd1232),
inference(forward_demodulation,[],[f790,f768]) ).
fof(f1573,plain,
vd684 = vangle(sK7,sK3,sK1),
inference(forward_demodulation,[],[f751,f768]) ).
fof(f2204,definition,
( spl55_22
<=> sK3 = sK7 ),
introduced(definition,[new_symbols(definition,[spl55_22])],[avatar_definition]) ).
fof(f2205,plain,
( sK3 = sK7
| ~ spl55_22 ),
inference(avatar_component_clause,[],[f2204]) ).
fof(f2421,plain,
! [X2,X0,X1] :
( ~ rR(X0,X1,X2)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rR(X2,X0,X1)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rpoint(X0) ),
inference(resolution,[],[f1033,f1022]) ).
fof(f2422,plain,
! [X2,X0,X1] :
( ~ rR(X0,X1,X2)
| ~ rR(X2,X0,X1)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rpoint(X2) ),
inference(duplicate_literal_removal,[],[f2421]) ).
fof(f3534,plain,
! [X0,X1] :
( ~ ron(X0,vd1232)
| ~ ron(X1,vd1232)
| ~ rR(sK7,X1,X0)
| ~ rline(vd1232)
| ~ rpoint(X0)
| ~ rpoint(sK7)
| ~ rpoint(X1) ),
inference(resolution,[],[f1015,f750]) ).
fof(f3542,plain,
! [X0,X1] :
( ~ ron(X0,vd1232)
| ~ ron(X1,vd1232)
| ~ rR(sK7,X1,X0)
| ~ rpoint(X0)
| ~ rpoint(sK7)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f3534,f511]) ).
fof(f3545,plain,
! [X0,X1] :
( ~ rR(sK7,X1,X0)
| ~ ron(X1,vd1232)
| ~ ron(X0,vd1232)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f3542,f495]) ).
fof(f3558,plain,
! [X0,X1] :
( ~ ron(X0,vd1232)
| ~ ron(X1,vd1232)
| ~ rR(X0,X1,sK7)
| ~ rline(vd1232)
| ~ rpoint(sK7)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(resolution,[],[f1019,f750]) ).
fof(f3566,plain,
! [X0,X1] :
( ~ ron(X0,vd1232)
| ~ ron(X1,vd1232)
| ~ rR(X0,X1,sK7)
| ~ rpoint(sK7)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f3558,f511]) ).
fof(f3569,plain,
! [X0,X1] :
( ~ rR(X0,X1,sK7)
| ~ ron(X1,vd1232)
| ~ ron(X0,vd1232)
| ~ rpoint(X0)
| ~ rpoint(X1) ),
inference(forward_subsumption_resolution,[],[f3566,f495]) ).
fof(f5518,plain,
! [X0] :
( vd684 != vd684
| ron(sK1,X0)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| sK3 = sK7
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK7)
| ~ rpoint(sK3) ),
inference(superposition,[],[f810,f1573]) ).
fof(f5523,plain,
! [X0] :
( ron(sK1,X0)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| sK3 = sK7
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK7)
| ~ rpoint(sK3) ),
inference(trivial_inequality_removal,[],[f5518]) ).
fof(f5528,plain,
! [X0] :
( ron(sK1,X0)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| sK3 = sK7
| ~ rline(X0)
| ~ rpoint(sK7)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f5523,f479]) ).
fof(f5533,plain,
! [X0] :
( ron(sK1,X0)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| sK3 = sK7
| ~ rline(X0)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f5528,f495]) ).
fof(f5538,plain,
! [X0] :
( ron(sK1,X0)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| sK3 = sK7
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[],[f5533,f475]) ).
fof(f5562,definition,
( spl55_50
<=> sK1 = sK3 ),
introduced(definition,[new_symbols(definition,[spl55_50])],[avatar_definition]) ).
fof(f5563,plain,
( sK1 = sK3
| ~ spl55_50 ),
inference(avatar_component_clause,[],[f5562]) ).
fof(f5565,definition,
( spl55_51
<=> ! [X0] :
( ron(sK1,X0)
| ~ rline(X0)
| ~ ron(sK3,X0)
| ~ ron(sK7,X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_51])],[avatar_definition]) ).
fof(f5566,plain,
( ! [X0] :
( ~ ron(sK7,X0)
| ~ rline(X0)
| ~ ron(sK3,X0)
| ron(sK1,X0) )
| ~ spl55_51 ),
inference(avatar_component_clause,[],[f5565]) ).
fof(f5567,plain,
( spl55_22
| spl55_50
| spl55_51 ),
inference(avatar_split_clause,[],[f5538,f5565,f5562,f2204]) ).
fof(f5639,plain,
! [X0] :
( vd684 != vd684
| ~ rR(sK3,sK7,sK1)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| sK3 = sK7
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK7)
| ~ rpoint(sK3) ),
inference(superposition,[],[f806,f1573]) ).
fof(f5644,plain,
! [X0] :
( ~ rR(sK3,sK7,sK1)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| sK3 = sK7
| ~ rline(X0)
| ~ rpoint(sK1)
| ~ rpoint(sK7)
| ~ rpoint(sK3) ),
inference(trivial_inequality_removal,[],[f5639]) ).
fof(f5649,plain,
! [X0] :
( ~ rR(sK3,sK7,sK1)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| sK3 = sK7
| ~ rline(X0)
| ~ rpoint(sK7)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f5644,f479]) ).
fof(f5654,plain,
! [X0] :
( ~ rR(sK3,sK7,sK1)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| sK3 = sK7
| ~ rline(X0)
| ~ rpoint(sK3) ),
inference(forward_subsumption_resolution,[],[f5649,f495]) ).
fof(f5659,plain,
! [X0] :
( ~ rR(sK3,sK7,sK1)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| sK1 = sK3
| sK3 = sK7
| ~ rline(X0) ),
inference(forward_subsumption_resolution,[],[f5654,f475]) ).
fof(f5677,definition,
( spl55_61
<=> ! [X0] :
( ~ ron(sK7,X0)
| ~ rline(X0)
| ~ ron(sK3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_61])],[avatar_definition]) ).
fof(f5678,plain,
( ! [X0] :
( ~ ron(sK7,X0)
| ~ rline(X0)
| ~ ron(sK3,X0) )
| ~ spl55_61 ),
inference(avatar_component_clause,[],[f5677]) ).
fof(f5680,definition,
( spl55_62
<=> rR(sK3,sK7,sK1) ),
introduced(definition,[new_symbols(definition,[spl55_62])],[avatar_definition]) ).
fof(f5681,plain,
( ~ rR(sK3,sK7,sK1)
| spl55_62 ),
inference(avatar_component_clause,[],[f5680]) ).
fof(f5682,plain,
( spl55_22
| spl55_50
| spl55_61
| ~ spl55_62 ),
inference(avatar_split_clause,[],[f5659,f5680,f5677,f5562,f2204]) ).
fof(f9157,definition,
( spl55_156
<=> sK1 = sK7 ),
introduced(definition,[new_symbols(definition,[spl55_156])],[avatar_definition]) ).
fof(f9158,plain,
( sK1 = sK7
| ~ spl55_156 ),
inference(avatar_component_clause,[],[f9157]) ).
fof(f12549,plain,
( ~ ron(sK3,vd1232)
| ~ spl55_22 ),
inference(superposition,[],[f750,f2205]) ).
fof(f12663,plain,
( $false
| ~ spl55_22 ),
inference(forward_subsumption_resolution,[],[f12549,f1564]) ).
fof(f12664,plain,
~ spl55_22,
inference(avatar_contradiction_clause,[],[f12663]) ).
fof(f13276,plain,
( ~ ron(sK3,vd1197)
| ~ spl55_50 ),
inference(superposition,[],[f796,f5563]) ).
fof(f13297,plain,
( $false
| ~ spl55_50 ),
inference(forward_subsumption_resolution,[],[f13276,f1560]) ).
fof(f13298,plain,
~ spl55_50,
inference(avatar_contradiction_clause,[],[f13297]) ).
fof(f15667,plain,
( ! [X0] :
( rR(sK7,sK3,sK1)
| rR(sK1,sK7,sK3)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ ron(sK7,X0)
| ~ rline(X0)
| sK1 = sK3
| sK1 = sK7
| sK3 = sK7
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ rpoint(sK7) )
| spl55_62 ),
inference(resolution,[],[f5681,f1003]) ).
fof(f15678,plain,
( ! [X0] :
( rR(sK7,sK3,sK1)
| rR(sK1,sK7,sK3)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ ron(sK7,X0)
| ~ rline(X0)
| sK1 = sK3
| sK1 = sK7
| sK3 = sK7
| ~ rpoint(sK3)
| ~ rpoint(sK7) )
| spl55_62 ),
inference(forward_subsumption_resolution,[],[f15667,f479]) ).
fof(f15685,plain,
( ! [X0] :
( rR(sK7,sK3,sK1)
| rR(sK1,sK7,sK3)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ ron(sK7,X0)
| ~ rline(X0)
| sK1 = sK3
| sK1 = sK7
| sK3 = sK7
| ~ rpoint(sK7) )
| spl55_62 ),
inference(forward_subsumption_resolution,[],[f15678,f475]) ).
fof(f15692,plain,
( ! [X0] :
( rR(sK7,sK3,sK1)
| rR(sK1,sK7,sK3)
| ~ ron(sK1,X0)
| ~ ron(sK3,X0)
| ~ ron(sK7,X0)
| ~ rline(X0)
| sK1 = sK3
| sK1 = sK7
| sK3 = sK7 )
| spl55_62 ),
inference(forward_subsumption_resolution,[],[f15685,f495]) ).
fof(f15709,definition,
( spl55_279
<=> rR(sK1,sK7,sK3) ),
introduced(definition,[new_symbols(definition,[spl55_279])],[avatar_definition]) ).
fof(f15710,plain,
( rR(sK1,sK7,sK3)
| ~ spl55_279 ),
inference(avatar_component_clause,[],[f15709]) ).
fof(f15712,definition,
( spl55_280
<=> rR(sK7,sK3,sK1) ),
introduced(definition,[new_symbols(definition,[spl55_280])],[avatar_definition]) ).
fof(f15713,plain,
( rR(sK7,sK3,sK1)
| ~ spl55_280 ),
inference(avatar_component_clause,[],[f15712]) ).
fof(f15719,plain,
( ~ ron(sK3,vd1232)
| ~ ron(sK1,vd1232)
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ spl55_280 ),
inference(resolution,[],[f15713,f3545]) ).
fof(f15730,plain,
( ~ ron(sK1,vd1232)
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ spl55_280 ),
inference(forward_subsumption_resolution,[],[f15719,f1564]) ).
fof(f15735,plain,
( ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ spl55_280 ),
inference(forward_subsumption_resolution,[],[f15730,f789]) ).
fof(f15740,plain,
( ~ rpoint(sK3)
| ~ spl55_280 ),
inference(forward_subsumption_resolution,[],[f15735,f479]) ).
fof(f15742,plain,
( $false
| ~ spl55_280 ),
inference(forward_subsumption_resolution,[],[f15740,f475]) ).
fof(f15743,plain,
~ spl55_280,
inference(avatar_contradiction_clause,[],[f15742]) ).
fof(f42811,plain,
( ~ rR(sK3,sK1,sK7)
| ~ rpoint(sK1)
| ~ rpoint(sK7)
| ~ rpoint(sK3)
| ~ spl55_279 ),
inference(resolution,[],[f2422,f15710]) ).
fof(f42877,plain,
( ~ rR(sK3,sK1,sK7)
| ~ rpoint(sK7)
| ~ rpoint(sK3)
| ~ spl55_279 ),
inference(forward_subsumption_resolution,[],[f42811,f479]) ).
fof(f42883,plain,
( ~ rR(sK3,sK1,sK7)
| ~ rpoint(sK3)
| ~ spl55_279 ),
inference(forward_subsumption_resolution,[],[f42877,f495]) ).
fof(f42884,plain,
( ~ rR(sK3,sK1,sK7)
| ~ spl55_279 ),
inference(forward_subsumption_resolution,[],[f42883,f475]) ).
fof(f42887,plain,
( ! [X0] :
( rR(sK1,sK3,sK7)
| rR(sK7,sK1,sK3)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| sK3 = sK7
| sK1 = sK7
| sK1 = sK3
| ~ rpoint(sK7)
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl55_279 ),
inference(resolution,[],[f42884,f1003]) ).
fof(f42897,plain,
( ! [X0] :
( rR(sK1,sK3,sK7)
| rR(sK7,sK1,sK3)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| sK3 = sK7
| sK1 = sK7
| sK1 = sK3
| ~ rpoint(sK3)
| ~ rpoint(sK1) )
| ~ spl55_279 ),
inference(forward_subsumption_resolution,[],[f42887,f495]) ).
fof(f42904,plain,
( ! [X0] :
( rR(sK1,sK3,sK7)
| rR(sK7,sK1,sK3)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| sK3 = sK7
| sK1 = sK7
| sK1 = sK3
| ~ rpoint(sK1) )
| ~ spl55_279 ),
inference(forward_subsumption_resolution,[],[f42897,f475]) ).
fof(f42911,plain,
( ! [X0] :
( rR(sK1,sK3,sK7)
| rR(sK7,sK1,sK3)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| ~ ron(sK1,X0)
| ~ rline(X0)
| sK3 = sK7
| sK1 = sK7
| sK1 = sK3 )
| ~ spl55_279 ),
inference(forward_subsumption_resolution,[],[f42904,f479]) ).
fof(f42919,plain,
( ! [X0] :
( rR(sK1,sK3,sK7)
| rR(sK7,sK1,sK3)
| ~ ron(sK7,X0)
| ~ ron(sK3,X0)
| ~ rline(X0)
| sK3 = sK7
| sK1 = sK7
| sK1 = sK3 )
| ~ spl55_51
| ~ spl55_279 ),
inference(forward_subsumption_resolution,[],[f42911,f5566]) ).
fof(f42927,definition,
( spl55_706
<=> rR(sK7,sK1,sK3) ),
introduced(definition,[new_symbols(definition,[spl55_706])],[avatar_definition]) ).
fof(f42928,plain,
( rR(sK7,sK1,sK3)
| ~ spl55_706 ),
inference(avatar_component_clause,[],[f42927]) ).
fof(f42930,definition,
( spl55_707
<=> rR(sK1,sK3,sK7) ),
introduced(definition,[new_symbols(definition,[spl55_707])],[avatar_definition]) ).
fof(f42931,plain,
( rR(sK1,sK3,sK7)
| ~ spl55_707 ),
inference(avatar_component_clause,[],[f42930]) ).
fof(f42932,plain,
( spl55_50
| spl55_156
| spl55_22
| spl55_61
| spl55_706
| spl55_707
| ~ spl55_51
| ~ spl55_279 ),
inference(avatar_split_clause,[],[f42919,f15709,f5565,f42930,f42927,f5677,f2204,f9157,f5562]) ).
fof(f42938,plain,
( ~ ron(sK3,vd1232)
| ~ ron(sK1,vd1232)
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ spl55_707 ),
inference(resolution,[],[f42931,f3569]) ).
fof(f42952,plain,
( ~ ron(sK1,vd1232)
| ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ spl55_707 ),
inference(forward_subsumption_resolution,[],[f42938,f1564]) ).
fof(f42957,plain,
( ~ rpoint(sK1)
| ~ rpoint(sK3)
| ~ spl55_707 ),
inference(forward_subsumption_resolution,[],[f42952,f789]) ).
fof(f42962,plain,
( ~ rpoint(sK3)
| ~ spl55_707 ),
inference(forward_subsumption_resolution,[],[f42957,f479]) ).
fof(f42964,plain,
( $false
| ~ spl55_707 ),
inference(forward_subsumption_resolution,[],[f42962,f475]) ).
fof(f42965,plain,
~ spl55_707,
inference(avatar_contradiction_clause,[],[f42964]) ).
fof(f42969,plain,
( ~ ron(sK1,vd1232)
| ~ ron(sK3,vd1232)
| ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ spl55_706 ),
inference(resolution,[],[f42928,f3545]) ).
fof(f42989,plain,
( ~ ron(sK3,vd1232)
| ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ spl55_706 ),
inference(forward_subsumption_resolution,[],[f42969,f789]) ).
fof(f42998,plain,
( ~ rpoint(sK3)
| ~ rpoint(sK1)
| ~ spl55_706 ),
inference(forward_subsumption_resolution,[],[f42989,f1564]) ).
fof(f43007,plain,
( ~ rpoint(sK1)
| ~ spl55_706 ),
inference(forward_subsumption_resolution,[],[f42998,f475]) ).
fof(f43013,plain,
( $false
| ~ spl55_706 ),
inference(forward_subsumption_resolution,[],[f43007,f479]) ).
fof(f43014,plain,
~ spl55_706,
inference(avatar_contradiction_clause,[],[f43013]) ).
fof(f43017,plain,
( ~ rline(vd1234)
| ~ ron(sK3,vd1234)
| ~ spl55_61 ),
inference(resolution,[],[f5678,f787]) ).
fof(f43061,plain,
( ~ ron(sK3,vd1234)
| ~ spl55_61 ),
inference(forward_subsumption_resolution,[],[f43017,f508]) ).
fof(f43066,plain,
( $false
| ~ spl55_61 ),
inference(forward_subsumption_resolution,[],[f43061,f1563]) ).
fof(f43067,plain,
~ spl55_61,
inference(avatar_contradiction_clause,[],[f43066]) ).
fof(f43132,plain,
( ~ ron(sK1,vd1232)
| ~ spl55_156 ),
inference(superposition,[],[f750,f9158]) ).
fof(f43304,plain,
( $false
| ~ spl55_156 ),
inference(forward_subsumption_resolution,[],[f43132,f789]) ).
fof(f43305,plain,
~ spl55_156,
inference(avatar_contradiction_clause,[],[f43304]) ).
fof(f43307,plain,
( ! [X0] :
( rR(sK7,sK3,sK1)
| rR(sK1,sK7,sK3)
| ~ ron(sK3,X0)
| ~ ron(sK7,X0)
| ~ rline(X0)
| sK1 = sK3
| sK1 = sK7
| sK3 = sK7 )
| ~ spl55_51
| spl55_62 ),
inference(forward_subsumption_resolution,[],[f15692,f5566]) ).
fof(f43309,plain,
( spl55_22
| spl55_156
| spl55_50
| spl55_61
| spl55_279
| spl55_280
| ~ spl55_51
| spl55_62 ),
inference(avatar_split_clause,[],[f43307,f5680,f5565,f15712,f15709,f5677,f5562,f9157,f2204]) ).
cnf(s46,plain,
( spl55_22
| spl55_50
| spl55_51 ),
inference(sat_conversion,[],[f5567]) ).
cnf(s54,plain,
( spl55_22
| spl55_50
| spl55_61
| ~ spl55_62 ),
inference(sat_conversion,[],[f5682]) ).
cnf(s203,plain,
~ spl55_22,
inference(sat_conversion,[],[f12664]) ).
cnf(s214,plain,
~ spl55_50,
inference(sat_conversion,[],[f13298]) ).
cnf(s274,plain,
~ spl55_280,
inference(sat_conversion,[],[f15743]) ).
cnf(s777,plain,
( spl55_22
| spl55_50
| ~ spl55_51
| spl55_61
| spl55_156
| ~ spl55_279
| spl55_706
| spl55_707 ),
inference(sat_conversion,[],[f42932]) ).
cnf(s780,plain,
~ spl55_707,
inference(sat_conversion,[],[f42965]) ).
cnf(s783,plain,
~ spl55_706,
inference(sat_conversion,[],[f43014]) ).
cnf(s785,plain,
~ spl55_61,
inference(sat_conversion,[],[f43067]) ).
cnf(s793,plain,
~ spl55_156,
inference(sat_conversion,[],[f43305]) ).
cnf(s794,plain,
( spl55_22
| spl55_50
| ~ spl55_51
| spl55_61
| spl55_62
| spl55_156
| spl55_279
| spl55_280 ),
inference(sat_conversion,[],[f43309]) ).
cnf(s798,plain,
( spl55_22
| spl55_50
| ~ spl55_51
| ~ spl55_279 ),
inference(rat,[],[s777,s780,s783,s793,s785]) ).
cnf(s908,plain,
~ spl55_62,
inference(rat,[],[s54,s785,s214,s203]) ).
cnf(s912,plain,
spl55_51,
inference(rat,[],[s46,s214,s203]) ).
cnf(s913,plain,
spl55_279,
inference(rat,[],[s794,s274,s908,s793,s203,s785,s214,s912]) ).
cnf(s914,plain,
$false,
inference(rat,[],[s798,s203,s214,s913,s912]) ).
fof(f43319,plain,
$false,
inference(avatar_sat_refutation,[],[s914]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO294+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % 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.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 08:02:56 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 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.13/0.85 % (2510861)Will run a generic schedule for satisfiability detection.
% 2.13/0.85 % (2510870)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1356417086:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.13/0.85 % (2510867)% WARNING: option uhcvi not known.
% 2.13/0.85 % (2510866)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3704332501_2999 on theBenchmark for (2999ds/0Mi)
% 2.13/0.85 % (2510867)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2226925759:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.13/0.85 % (2510868)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3028676267:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.13/0.85 % (2510869)dis+10_1_sil=32000:sp=arity:random_seed=1994578661:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.13/0.85 % (2510872)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1710811941:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.13/0.85 % (2510871)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2166673088:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.13/0.85 % (2510870)Instruction limit reached!
% 2.13/0.85 % (2510870)------------------------------
% 2.13/0.85 % (2510870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.13/0.85 % (2510870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.13/0.85 % (2510870)CaDiCaL version: 2.1.3
% 2.13/0.85 % (2510870)Termination reason: Instruction limit
% 2.13/0.85 % (2510870)Termination phase: Saturation
% 2.13/0.85 % (2510870)Time elapsed: 0.032 s
% 2.13/0.85 % (2510870)Peak memory usage: 13 MB
% 2.13/0.85 % (2510870)Instructions burned: 119 (million)
% 2.13/0.85 % Detected minimum model sizes of [3]
% 2.13/0.85 % Detected maximum model sizes of [max]
% 2.13/0.85 % (2510866)Cannot represent all propositional literals internally
% 2.13/0.85 % (2510866)Refutation not found, incomplete strategy
% 2.13/0.85 % (2510866)------------------------------
% 2.13/0.85 % (2510866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.13/0.85 % (2510866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.13/0.85 % (2510866)CaDiCaL version: 2.1.3
% 2.13/0.85 % (2510880)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2779777900:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.13/0.85 % (2510866)Termination reason: Refutation not found, incomplete strategy
% 2.13/0.85 % (2510866)Time elapsed: 0.037 s
% 2.13/0.85 % (2510866)Peak memory usage: 12 MB
% 2.13/0.85 % (2510866)Instructions burned: 75 (million)
% 2.13/0.85 % (2510866)------------------------------
% 2.13/0.85 % (2510866)------------------------------
% 2.13/0.85 % Detected minimum model sizes of [3]
% 2.13/0.85 % Detected maximum model sizes of [max]
% 2.13/0.85 % (2510880)Cannot represent all propositional literals internally
% 2.13/0.85 % (2510880)Refutation not found, incomplete strategy
% 2.13/0.85 % (2510880)------------------------------
% 2.13/0.85 % (2510880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.13/0.85 % (2510880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.13/0.85 % (2510880)CaDiCaL version: 2.1.3
% 2.13/0.85 % (2510880)Termination reason: Refutation not found, incomplete strategy
% 2.13/0.85 % (2510880)Time elapsed: 0.015 s
% 2.13/0.85 % (2510880)Peak memory usage: 12 MB
% 2.13/0.85 % (2510880)Instructions burned: 58 (million)
% 2.13/0.85 % (2510880)------------------------------
% 2.13/0.85 % (2510880)------------------------------
% 2.13/0.85 % (2510869)Instruction limit reached!
% 2.13/0.85 % (2510869)------------------------------
% 2.13/0.85 % (2510869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.13/0.85 % (2510869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.13/0.85 % (2510869)CaDiCaL version: 2.1.3
% 2.13/0.85 % (2510869)Termination reason: Instruction limit
% 2.13/0.85 % (2510869)Termination phase: Saturation
% 2.13/0.85 % (2510869)Time elapsed: 0.057 s
% 2.13/0.85 % (2510869)Peak memory usage: 13 MB
% 2.13/0.85 % (2510869)Instructions burned: 104 (million)
% 2.13/0.85 % (2510882)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=555039270:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.13/0.85 % (2510871)Instruction limit reached!
% 2.13/0.85 % (2510871)------------------------------
% 2.13/0.85 % (2510871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.13/0.85 % (2510871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.26 % (2510871)CaDiCaL version: 2.1.3
% 5.32/1.26 % (2510871)Termination reason: Instruction limit
% 5.32/1.26 % (2510871)Termination phase: Saturation
% 5.32/1.26 % (2510871)Time elapsed: 0.062 s
% 5.32/1.26 % (2510871)Peak memory usage: 13 MB
% 5.32/1.26 % (2510871)Instructions burned: 131 (million)
% 5.32/1.26 % (2510883)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=307375525:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 5.32/1.26 % (2510885)ott-21_1_sil=16000:fs=off:random_seed=1071944190:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 5.32/1.26 % (2510887)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=599600424:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 5.32/1.26 % (2510872)Instruction limit reached!
% 5.32/1.26 % (2510872)------------------------------
% 5.32/1.26 % (2510872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.32/1.26 % (2510872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.26 % (2510872)CaDiCaL version: 2.1.3
% 5.32/1.26 % (2510872)Termination reason: Instruction limit
% 5.32/1.26 % (2510872)Termination phase: Saturation
% 5.32/1.26 % (2510872)Time elapsed: 0.094 s
% 5.32/1.26 % (2510872)Peak memory usage: 15 MB
% 5.32/1.26 % (2510872)Instructions burned: 159 (million)
% 5.32/1.26 % (2510882)Instruction limit reached!
% 5.32/1.26 % (2510882)------------------------------
% 5.32/1.26 % (2510882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.32/1.26 % (2510882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.26 % (2510882)CaDiCaL version: 2.1.3
% 5.32/1.26 % (2510882)Termination reason: Instruction limit
% 5.32/1.26 % (2510882)Termination phase: Saturation
% 5.32/1.26 % (2510882)Time elapsed: 0.053 s
% 5.32/1.26 % (2510882)Peak memory usage: 12 MB
% 5.32/1.26 % (2510882)Instructions burned: 133 (million)
% 5.32/1.26 % (2510890)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=676193069:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 5.32/1.26 % (2510891)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=452096158:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 5.32/1.26 % Detected minimum model sizes of [3]
% 5.32/1.26 % Detected maximum model sizes of [max]
% 5.32/1.26 % (2510890)Cannot represent all propositional literals internally
% 5.32/1.26 % (2510890)Refutation not found, incomplete strategy
% 5.32/1.26 % (2510890)------------------------------
% 5.32/1.26 % (2510890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.32/1.26 % (2510890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.26 % (2510890)CaDiCaL version: 2.1.3
% 5.32/1.26 % (2510890)Termination reason: Refutation not found, incomplete strategy
% 5.32/1.26 % (2510890)Time elapsed: 0.028 s
% 5.32/1.26 % (2510890)Peak memory usage: 12 MB
% 5.32/1.26 % (2510890)Instructions burned: 60 (million)
% 5.32/1.26 % (2510890)------------------------------
% 5.32/1.26 % (2510890)------------------------------
% 5.32/1.26 % (2510894)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2354258859:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 5.32/1.26 % (2510885)Instruction limit reached!
% 5.32/1.26 % (2510885)------------------------------
% 5.32/1.26 % (2510885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.32/1.26 % (2510885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.32/1.26 % (2510885)CaDiCaL version: 2.1.3
% 5.32/1.26 % (2510885)Termination reason: Instruction limit
% 5.32/1.26 % (2510885)Termination phase: Saturation
% 5.32/1.26 % (2510885)Time elapsed: 0.095 s
% 5.32/1.26 % (2510885)Peak memory usage: 14 MB
% 5.32/1.26 % (2510885)Instructions burned: 181 (million)
% 5.32/1.26 % (2510896)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=1179328077:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 5.32/1.26 % (2510894)Cannot represent all propositional literals internally
% 5.32/1.26 % (2510894)Refutation not found, incomplete strategy
% 5.32/1.26 % (2510894)------------------------------
% 5.32/1.26 % (2510894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.32/1.26 % (2510894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.54 % (2510894)CaDiCaL version: 2.1.3
% 14.71/2.54 % (2510894)Termination reason: Refutation not found, incomplete strategy
% 14.71/2.54 % (2510894)Time elapsed: 0.028 s
% 14.71/2.54 % (2510894)Peak memory usage: 12 MB
% 14.71/2.54 % (2510894)Instructions burned: 59 (million)
% 14.71/2.54 % (2510894)------------------------------
% 14.71/2.54 % (2510894)------------------------------
% 14.71/2.54 % (2510898)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=829008183:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 14.71/2.54 % (2510883)Instruction limit reached!
% 14.71/2.54 % (2510883)------------------------------
% 14.71/2.54 % (2510883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.54 % (2510883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.54 % (2510883)CaDiCaL version: 2.1.3
% 14.71/2.54 % (2510883)Termination reason: Instruction limit
% 14.71/2.54 % (2510883)Termination phase: Saturation
% 14.71/2.54 % (2510883)Time elapsed: 0.179 s
% 14.71/2.54 % (2510883)Peak memory usage: 21 MB
% 14.71/2.54 % (2510883)Instructions burned: 686 (million)
% 14.71/2.54 % (2510900)fmb+10_1_sil=64000:random_seed=3215919887:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 14.71/2.54 % Detected minimum model sizes of [3]
% 14.71/2.54 % Detected maximum model sizes of [max]
% 14.71/2.54 % (2510900)Cannot represent all propositional literals internally
% 14.71/2.54 % (2510900)Refutation not found, incomplete strategy
% 14.71/2.54 % (2510900)------------------------------
% 14.71/2.54 % (2510900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.54 % (2510900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.54 % (2510900)CaDiCaL version: 2.1.3
% 14.71/2.54 % (2510900)Termination reason: Refutation not found, incomplete strategy
% 14.71/2.54 % (2510900)Time elapsed: 0.015 s
% 14.71/2.54 % (2510900)Peak memory usage: 12 MB
% 14.71/2.54 % (2510900)Instructions burned: 56 (million)
% 14.71/2.54 % (2510900)------------------------------
% 14.71/2.54 % (2510900)------------------------------
% 14.71/2.54 % (2510902)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=684614117:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 14.71/2.54 % Detected minimum model sizes of [3]
% 14.71/2.54 % Detected maximum model sizes of [max]
% 14.71/2.54 % (2510902)Cannot represent all propositional literals internally
% 14.71/2.54 % (2510902)Refutation not found, incomplete strategy
% 14.71/2.54 % (2510902)------------------------------
% 14.71/2.54 % (2510902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.54 % (2510902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.54 % (2510902)CaDiCaL version: 2.1.3
% 14.71/2.54 % (2510902)Termination reason: Refutation not found, incomplete strategy
% 14.71/2.54 % (2510902)Time elapsed: 0.015 s
% 14.71/2.54 % (2510902)Peak memory usage: 12 MB
% 14.71/2.54 % (2510902)Instructions burned: 59 (million)
% 14.71/2.54 % (2510902)------------------------------
% 14.71/2.54 % (2510902)------------------------------
% 14.71/2.54 % (2510904)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2714274976:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 14.71/2.54 % Detected minimum model sizes of [3]
% 14.71/2.54 % Detected maximum model sizes of [max]
% 14.71/2.54 % (2510904)Cannot represent all propositional literals internally
% 14.71/2.54 % (2510904)Refutation not found, incomplete strategy
% 14.71/2.54 % (2510904)------------------------------
% 14.71/2.54 % (2510904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.54 % (2510904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.54 % (2510904)CaDiCaL version: 2.1.3
% 14.71/2.54 % (2510904)Termination reason: Refutation not found, incomplete strategy
% 14.71/2.54 % (2510904)Time elapsed: 0.015 s
% 14.71/2.54 % (2510904)Peak memory usage: 12 MB
% 14.71/2.54 % (2510904)Instructions burned: 60 (million)
% 14.71/2.54 % (2510904)------------------------------
% 14.71/2.54 % (2510904)------------------------------
% 14.71/2.54 % (2510906)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2138347140:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 14.71/2.54 % (2510887)Instruction limit reached!
% 14.71/2.54 % (2510887)------------------------------
% 14.71/2.54 % (2510887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.54 % (2510887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.54 % (2510887)CaDiCaL version: 2.1.3
% 14.71/2.54 % (2510887)Termination reason: Instruction limit
% 16.58/2.82 % (2510887)Termination phase: Saturation
% 16.58/2.82 % (2510887)Time elapsed: 0.306 s
% 16.58/2.82 % (2510887)Peak memory usage: 15 MB
% 16.58/2.82 % (2510887)Instructions burned: 478 (million)
% 16.58/2.82 % (2510908)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=563543557:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 16.58/2.82 % (2510896)Instruction limit reached!
% 16.58/2.82 % (2510896)------------------------------
% 16.58/2.82 % (2510896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.58/2.82 % (2510896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.82 % (2510896)CaDiCaL version: 2.1.3
% 16.58/2.82 % (2510896)Termination reason: Instruction limit
% 16.58/2.82 % (2510896)Termination phase: Saturation
% 16.58/2.82 % (2510896)Time elapsed: 0.353 s
% 16.58/2.82 % (2510896)Peak memory usage: 20 MB
% 16.58/2.82 % (2510896)Instructions burned: 693 (million)
% 16.58/2.82 % (2510910)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1856825420:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 16.58/2.82 % Detected minimum model sizes of [3]
% 16.58/2.82 % Detected maximum model sizes of [max]
% 16.58/2.82 % (2510910)Cannot represent all propositional literals internally
% 16.58/2.82 % (2510910)Refutation not found, incomplete strategy
% 16.58/2.82 % (2510910)------------------------------
% 16.58/2.82 % (2510910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.58/2.82 % (2510910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.82 % (2510910)CaDiCaL version: 2.1.3
% 16.58/2.82 % (2510910)Termination reason: Refutation not found, incomplete strategy
% 16.58/2.82 % (2510910)Time elapsed: 0.036 s
% 16.58/2.82 % (2510910)Peak memory usage: 12 MB
% 16.58/2.82 % (2510910)Instructions burned: 75 (million)
% 16.58/2.82 % (2510910)------------------------------
% 16.58/2.82 % (2510910)------------------------------
% 16.58/2.82 % (2510912)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2305469241:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 16.58/2.82 % Detected minimum model sizes of [3]
% 16.58/2.82 % Detected maximum model sizes of [max]
% 16.58/2.82 % (2510912)Cannot represent all propositional literals internally
% 16.58/2.82 % (2510912)Refutation not found, incomplete strategy
% 16.58/2.82 % (2510912)------------------------------
% 16.58/2.82 % (2510912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.58/2.82 % (2510912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.82 % (2510912)CaDiCaL version: 2.1.3
% 16.58/2.82 % (2510912)Termination reason: Refutation not found, incomplete strategy
% 16.58/2.82 % (2510912)Time elapsed: 0.029 s
% 16.58/2.82 % (2510912)Peak memory usage: 12 MB
% 16.58/2.82 % (2510912)Instructions burned: 61 (million)
% 16.58/2.82 % (2510912)------------------------------
% 16.58/2.82 % (2510912)------------------------------
% 16.58/2.82 % (2510898)Instruction limit reached!
% 16.58/2.82 % (2510898)------------------------------
% 16.58/2.82 % (2510898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.58/2.82 % (2510898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.82 % (2510898)CaDiCaL version: 2.1.3
% 16.58/2.82 % (2510898)Termination reason: Instruction limit
% 16.58/2.82 % (2510898)Termination phase: Saturation
% 16.58/2.82 % (2510898)Time elapsed: 0.457 s
% 16.58/2.82 % (2510898)Peak memory usage: 21 MB
% 16.58/2.82 % (2510898)Instructions burned: 879 (million)
% 16.58/2.82 % (2510914)ott-2_1_sil=16000:newcnf=on:random_seed=763598537:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 16.58/2.82 % (2510915)ott+10_1_sil=32000:tgt=ground:random_seed=2798252855:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 16.58/2.82 % (2510891)Instruction limit reached!
% 16.58/2.82 % (2510891)------------------------------
% 16.58/2.82 % (2510891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.58/2.82 % (2510891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.82 % (2510891)CaDiCaL version: 2.1.3
% 16.58/2.82 % (2510891)Termination reason: Instruction limit
% 16.58/2.82 % (2510891)Termination phase: Saturation
% 16.58/2.82 % (2510891)Time elapsed: 0.609 s
% 16.58/2.82 % (2510891)Peak memory usage: 24 MB
% 16.58/2.82 % (2510891)Instructions burned: 1180 (million)
% 16.58/2.82 % (2510918)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2522359716:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 16.58/2.82 % Detected minimum model sizes of [3]
% 16.58/2.82 % Detected maximum model sizes of [max]
% 16.58/2.82 % (2510918)Cannot represent all propositional literals internally
% 16.58/2.82 % (2510918)Refutation not found, incomplete strategy
% 16.58/2.82 % (2510918)------------------------------
% 16.58/2.82 % (2510918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.58/2.82 % (2510918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.82 % (2510918)CaDiCaL version: 2.1.3
% 16.58/2.82 % (2510918)Termination reason: Refutation not found, incomplete strategy
% 16.58/2.82 % (2510918)Time elapsed: 0.036 s
% 16.58/2.82 % (2510918)Peak memory usage: 12 MB
% 16.58/2.82 % (2510918)Instructions burned: 75 (million)
% 16.58/2.82 % (2510918)------------------------------
% 16.58/2.82 % (2510918)------------------------------
% 16.58/2.82 % (2510920)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3053500517:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 16.58/2.82 % (2510908)Instruction limit reached!
% 16.58/2.82 % (2510908)------------------------------
% 16.58/2.82 % (2510908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.58/2.82 % (2510908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.82 % (2510908)CaDiCaL version: 2.1.3
% 16.58/2.82 % (2510908)Termination reason: Instruction limit
% 16.58/2.82 % (2510908)Termination phase: Saturation
% 16.58/2.82 % (2510908)Time elapsed: 0.592 s
% 16.58/2.82 % (2510908)Peak memory usage: 15 MB
% 16.58/2.82 % (2510908)Instructions burned: 1473 (million)
% 16.58/2.82 % (2510922)dis+21_1_sil=32000:sas=cadical:random_seed=2032465647:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi)
% 16.58/2.82 % (2510914)Instruction limit reached!
% 16.58/2.82 % (2510914)------------------------------
% 16.58/2.82 % (2510914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.58/2.82 % (2510914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.82 % (2510914)CaDiCaL version: 2.1.3
% 16.58/2.82 % (2510914)Termination reason: Instruction limit
% 16.58/2.82 % (2510914)Termination phase: Saturation
% 16.58/2.82 % (2510914)Time elapsed: 0.432 s
% 16.58/2.82 % (2510914)Peak memory usage: 16 MB
% 16.58/2.82 % (2510914)Instructions burned: 870 (million)
% 16.58/2.82 % (2510924)ott+11_1_sil=16000:gs=on:random_seed=1857447715:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi)
% 16.58/2.82 % (2510906)Instruction limit reached!
% 16.58/2.82 % (2510906)------------------------------
% 16.58/2.82 % (2510906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.58/2.82 % (2510906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.82 % (2510906)CaDiCaL version: 2.1.3
% 16.58/2.82 % (2510906)Termination reason: Instruction limit
% 16.58/2.82 % (2510906)Termination phase: Saturation
% 16.58/2.82 % (2510906)Time elapsed: 1.095 s
% 16.58/2.82 % (2510906)Peak memory usage: 25 MB
% 16.58/2.82 % (2510906)Instructions burned: 5135 (million)
% 16.58/2.82 % (2510926)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4166328466:fmbsr=1.6:i=67534_2985 on theBenchmark for (2985ds/67534Mi)
% 16.58/2.82 % Detected minimum model sizes of [3]
% 16.58/2.82 % Detected maximum model sizes of [max]
% 16.58/2.82 % (2510926)Cannot represent all propositional literals internally
% 16.58/2.82 % (2510926)Refutation not found, incomplete strategy
% 16.58/2.82 % (2510926)------------------------------
% 16.58/2.82 % (2510926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.58/2.82 % (2510926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.82 % (2510926)CaDiCaL version: 2.1.3
% 16.58/2.82 % (2510926)Termination reason: Refutation not found, incomplete strategy
% 16.58/2.82 % (2510926)Time elapsed: 0.016 s
% 16.58/2.82 % (2510926)Peak memory usage: 12 MB
% 16.58/2.82 % (2510926)Instructions burned: 65 (million)
% 16.58/2.82 % (2510926)------------------------------
% 16.58/2.82 % (2510926)------------------------------
% 16.58/2.82 % (2510928)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4268452692:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi)
% 16.58/2.82 % (2510924)Instruction limit reached!
% 16.58/2.82 % (2510924)------------------------------
% 16.58/2.82 % (2510924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.58/2.82 % (2510924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.82 % (2510924)CaDiCaL version: 2.1.3
% 16.58/2.82 % (2510924)Termination reason: Instruction limit
% 16.58/2.82 % (2510924)Termination phase: Saturation
% 16.58/2.82 % (2510924)Time elapsed: 0.956 s
% 16.58/2.82 % (2510924)Peak memory usage: 18 MB
% 16.58/2.82 % (2510924)Instructions burned: 2253 (million)
% 16.58/2.82 % (2510930)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4061053351:i=29340_2978 on theBenchmark for (2978ds/29340Mi)
% 16.58/2.82 % (2510920) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2510861-2510920"...
% 16.58/2.82 % (2510920)...printing done.
% 16.58/2.82 % (2510920)Refutation found. Thanks to Tanya!
% 16.58/2.82 % SZS status Theorem for theBenchmark
% 16.58/2.82 % SZS output start Proof for theBenchmark
% See solution above
% 16.58/2.82 % (2510920)------------------------------
% 16.58/2.82 % (2510920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.58/2.82 % (2510920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.82 % (2510920)CaDiCaL version: 2.1.3
% 16.58/2.82 % (2510920)Termination reason: Refutation
% 16.58/2.82 % (2510920)Time elapsed: 1.528 s
% 16.58/2.82 % (2510920)Peak memory usage: 29 MB
% 16.58/2.82 % (2510920)Instructions burned: 2887 (million)
% 16.58/2.82 % (2510861)Success in time 2.395 s
% 16.58/2.82 % Vampire exiting
%------------------------------------------------------------------------------