%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL670+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:59:57 AM UTC 2026
% Result : Theorem 1.86s 0.79s
% Output : Refutation 1.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 11
% Syntax : Number of formulae : 101 ( 18 unt; 9 def)
% Number of atoms : 661 ( 0 equ)
% Maximal formula atoms : 49 ( 6 avg)
% Number of connectives : 1172 ( 612 ~; 485 |; 66 &)
% ( 9 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 15 ( 14 usr; 10 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-1 aty)
% Number of variables : 350 ( 0 sgn 314 !; 36 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(f2,conjecture,
~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p4(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p3(X0) )
| ~ p2(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ! [X0] :
( ~ r1(X1,X0)
| p3(X0) )
| ~ p2(X1) ) )
& p2(X0)
& ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p2(X1) ) ) ) ) )
| ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ p2(X0) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p2(X1) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
& ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',main) ).
fof(f3,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p4(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p3(X0) )
| ~ p2(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ! [X0] :
( ~ r1(X1,X0)
| p3(X0) )
| ~ p2(X1) ) )
& p2(X0)
& ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p2(X1) ) ) ) ) )
| ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ p2(X0) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p2(X1) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
& ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f4,plain,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p4(X1) )
| ~ ! [X2] :
( ~ r1(X0,X2)
| ~ ( ~ ! [X3] :
( ~ r1(X2,X3)
| ~ ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p3(X5) )
| ~ p2(X4) ) )
| ~ ! [X6] :
( ~ r1(X2,X6)
| ~ ( ~ ! [X7] :
( ~ r1(X6,X7)
| ~ ( ! [X8] :
( ~ r1(X7,X8)
| p3(X8) )
| ~ p2(X7) ) )
& p2(X6)
& ~ ! [X9] :
( ~ r1(X6,X9)
| ~ ! [X10] :
( ~ r1(X9,X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ~ p2(X11) ) ) ) ) )
| ( ~ ! [X12] :
( ~ r1(X2,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ~ ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p3(X15) )
| ~ p2(X14) ) ) )
& ! [X16] :
( ~ r1(X2,X16)
| ~ ! [X17] :
( ~ r1(X16,X17)
| ~ p2(X17) ) ) ) ) )
| ~ ! [X18] :
( ~ r1(X0,X18)
| ~ ( ~ ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) )
& ! [X21] :
( ~ r1(X18,X21)
| p1(X21) ) ) )
| ! [X22] :
( ~ r1(X0,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ~ ! [X24] :
( ~ r1(X23,X24)
| p1(X24) ) )
| ! [X25] :
( ~ r1(X22,X25)
| p1(X25) ) )
| ! [X26] :
( ~ r1(X0,X26)
| ~ ! [X27] :
( ~ r1(X26,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| p2(X28) ) ) )
| ~ ! [X29] :
( ~ r1(X0,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ~ p1(X31) ) )
| ~ ! [X32] :
( ~ r1(X29,X32)
| ~ p1(X32) ) ) ),
inference(rectify,[],[f3]) ).
fof(f5,plain,
? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p4(X1) )
| ~ ! [X2] :
( ~ r1(X0,X2)
| ~ ( ~ ! [X3] :
( ~ r1(X2,X3)
| ~ ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p3(X5) )
| ~ p2(X4) ) )
| ~ ! [X6] :
( ~ r1(X2,X6)
| ~ ( ~ ! [X7] :
( ~ r1(X6,X7)
| ~ ( ! [X8] :
( ~ r1(X7,X8)
| p3(X8) )
| ~ p2(X7) ) )
& p2(X6)
& ~ ! [X9] :
( ~ r1(X6,X9)
| ~ ! [X10] :
( ~ r1(X9,X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ~ p2(X11) ) ) ) ) )
| ( ~ ! [X12] :
( ~ r1(X2,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ~ ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p3(X15) )
| ~ p2(X14) ) ) )
& ! [X16] :
( ~ r1(X2,X16)
| ~ ! [X17] :
( ~ r1(X16,X17)
| ~ p2(X17) ) ) ) ) )
| ~ ! [X18] :
( ~ r1(X0,X18)
| ~ ( ~ ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) )
& ! [X21] :
( ~ r1(X18,X21)
| p1(X21) ) ) )
| ! [X22] :
( ~ r1(X0,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ~ ! [X24] :
( ~ r1(X23,X24)
| p1(X24) ) )
| ! [X25] :
( ~ r1(X22,X25)
| p1(X25) ) )
| ! [X26] :
( ~ r1(X0,X26)
| ~ ! [X27] :
( ~ r1(X26,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| p2(X28) ) ) )
| ~ ! [X29] :
( ~ r1(X0,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ~ p1(X31) ) )
| ~ ! [X32] :
( ~ r1(X29,X32)
| ~ p1(X32) ) ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p4(X1) )
| ~ ! [X2] :
( ~ r1(X0,X2)
| ~ ( ~ ! [X3] :
( ~ r1(X2,X3)
| ~ ! [X4] :
( ~ r1(X3,X4)
| ! [X5] : ~ r1(X4,X5)
| ~ p2(X4) ) )
| ~ ! [X6] :
( ~ r1(X2,X6)
| ~ ( ~ ! [X7] :
( ~ r1(X6,X7)
| ~ ( ! [X8] : ~ r1(X7,X8)
| ~ p2(X7) ) )
& p2(X6)
& ~ ! [X9] :
( ~ r1(X6,X9)
| ~ ! [X10] :
( ~ r1(X9,X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ~ p2(X11) ) ) ) ) )
| ( ~ ! [X12] :
( ~ r1(X2,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ~ ! [X14] :
( ~ r1(X13,X14)
| ! [X15] : ~ r1(X14,X15)
| ~ p2(X14) ) ) )
& ! [X16] :
( ~ r1(X2,X16)
| ~ ! [X17] :
( ~ r1(X16,X17)
| ~ p2(X17) ) ) ) ) )
| ~ ! [X18] :
( ~ r1(X0,X18)
| ~ ( ~ ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) )
& ! [X21] :
( ~ r1(X18,X21)
| p1(X21) ) ) )
| ! [X22] :
( ~ r1(X0,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ~ ! [X24] :
( ~ r1(X23,X24)
| p1(X24) ) )
| ! [X25] :
( ~ r1(X22,X25)
| p1(X25) ) )
| ! [X26] :
( ~ r1(X0,X26)
| ~ ! [X27] :
( ~ r1(X26,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| p2(X28) ) ) )
| ~ ! [X29] :
( ~ r1(X0,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ~ p1(X31) ) )
| ~ ! [X32] :
( ~ r1(X29,X32)
| ~ p1(X32) ) ) ),
inference(pure_predicate_removal,[],[f5]) ).
fof(f7,plain,
? [X0] :
~ ( ~ ! [X2] :
( ~ r1(X0,X2)
| ~ ( ~ ! [X3] :
( ~ r1(X2,X3)
| ~ ! [X4] :
( ~ r1(X3,X4)
| ! [X5] : ~ r1(X4,X5)
| ~ p2(X4) ) )
| ~ ! [X6] :
( ~ r1(X2,X6)
| ~ ( ~ ! [X7] :
( ~ r1(X6,X7)
| ~ ( ! [X8] : ~ r1(X7,X8)
| ~ p2(X7) ) )
& p2(X6)
& ~ ! [X9] :
( ~ r1(X6,X9)
| ~ ! [X10] :
( ~ r1(X9,X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ~ p2(X11) ) ) ) ) )
| ( ~ ! [X12] :
( ~ r1(X2,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ~ ! [X14] :
( ~ r1(X13,X14)
| ! [X15] : ~ r1(X14,X15)
| ~ p2(X14) ) ) )
& ! [X16] :
( ~ r1(X2,X16)
| ~ ! [X17] :
( ~ r1(X16,X17)
| ~ p2(X17) ) ) ) ) )
| ~ ! [X18] :
( ~ r1(X0,X18)
| ~ ( ~ ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) )
& ! [X21] :
( ~ r1(X18,X21)
| p1(X21) ) ) )
| ! [X22] :
( ~ r1(X0,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ~ ! [X24] :
( ~ r1(X23,X24)
| p1(X24) ) )
| ! [X25] :
( ~ r1(X22,X25)
| p1(X25) ) )
| ! [X26] :
( ~ r1(X0,X26)
| ~ ! [X27] :
( ~ r1(X26,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| p2(X28) ) ) )
| ~ ! [X29] :
( ~ r1(X0,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ~ p1(X31) ) )
| ~ ! [X32] :
( ~ r1(X29,X32)
| ~ p1(X32) ) ) ),
inference(pure_predicate_removal,[],[f6]) ).
fof(f8,plain,
? [X0] :
( ! [X2] :
( ~ r1(X0,X2)
| ( ! [X3] :
( ~ r1(X2,X3)
| ? [X4] :
( r1(X3,X4)
& ? [X5] : r1(X4,X5)
& p2(X4) ) )
& ! [X6] :
( ~ r1(X2,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ( ? [X8] : r1(X7,X8)
& p2(X7) ) )
| ~ p2(X6)
| ! [X9] :
( ~ r1(X6,X9)
| ? [X10] :
( r1(X9,X10)
& ! [X11] :
( ~ r1(X10,X11)
| ~ p2(X11) ) ) ) )
& ( ! [X12] :
( ~ r1(X2,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ? [X14] :
( r1(X13,X14)
& ? [X15] : r1(X14,X15)
& p2(X14) ) ) )
| ? [X16] :
( r1(X2,X16)
& ! [X17] :
( ~ r1(X16,X17)
| ~ p2(X17) ) ) ) ) )
& ! [X18] :
( ~ r1(X0,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) )
| ? [X21] :
( r1(X18,X21)
& ~ p1(X21) ) )
& ? [X22] :
( r1(X0,X22)
& ? [X23] :
( r1(X22,X23)
& ! [X24] :
( ~ r1(X23,X24)
| p1(X24) ) )
& ? [X25] :
( r1(X22,X25)
& ~ p1(X25) ) )
& ? [X26] :
( r1(X0,X26)
& ! [X27] :
( ~ r1(X26,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p2(X28) ) ) )
& ! [X29] :
( ~ r1(X0,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ~ p1(X31) ) )
| ? [X32] :
( r1(X29,X32)
& p1(X32) ) ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f9,plain,
? [X0] :
( ! [X2] :
( ~ r1(X0,X2)
| ( ! [X3] :
( ~ r1(X2,X3)
| ? [X4] :
( r1(X3,X4)
& ? [X5] : r1(X4,X5)
& p2(X4) ) )
& ! [X6] :
( ~ r1(X2,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ( ? [X8] : r1(X7,X8)
& p2(X7) ) )
| ~ p2(X6)
| ! [X9] :
( ~ r1(X6,X9)
| ? [X10] :
( r1(X9,X10)
& ! [X11] :
( ~ r1(X10,X11)
| ~ p2(X11) ) ) ) )
& ( ! [X12] :
( ~ r1(X2,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ? [X14] :
( r1(X13,X14)
& ? [X15] : r1(X14,X15)
& p2(X14) ) ) )
| ? [X16] :
( r1(X2,X16)
& ! [X17] :
( ~ r1(X16,X17)
| ~ p2(X17) ) ) ) ) )
& ! [X18] :
( ~ r1(X0,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) )
| ? [X21] :
( r1(X18,X21)
& ~ p1(X21) ) )
& ? [X22] :
( r1(X0,X22)
& ? [X23] :
( r1(X22,X23)
& ! [X24] :
( ~ r1(X23,X24)
| p1(X24) ) )
& ? [X25] :
( r1(X22,X25)
& ~ p1(X25) ) )
& ? [X26] :
( r1(X0,X26)
& ! [X27] :
( ~ r1(X26,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p2(X28) ) ) )
& ! [X29] :
( ~ r1(X0,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ~ p1(X31) ) )
| ? [X32] :
( r1(X29,X32)
& p1(X32) ) ) ),
inference(flattening,[],[f8]) ).
fof(f10,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f11,plain,
! [X2,X11,X6,X9,X7] :
( ~ r1(sK10(X9),X11)
| ~ p2(X11)
| ~ r1(X6,X9)
| ~ p2(X6)
| p2(X7)
| ~ r1(X6,X7)
| ~ r1(X2,X6)
| ~ r1(sK0,X2) ),
inference(cnf_transformation,[],[f9]) ).
fof(f13,plain,
! [X2,X17,X12,X13] :
( ~ p2(X17)
| ~ r1(sK8(X2),X17)
| p2(sK12(X13))
| ~ r1(X12,X13)
| ~ r1(X2,X12)
| ~ r1(sK0,X2) ),
inference(cnf_transformation,[],[f9]) ).
fof(f15,plain,
! [X2,X17,X12,X13] :
( ~ r1(sK8(X2),X17)
| ~ p2(X17)
| r1(X13,sK12(X13))
| ~ r1(X12,X13)
| ~ r1(X2,X12)
| ~ r1(sK0,X2) ),
inference(cnf_transformation,[],[f9]) ).
fof(f16,plain,
! [X2,X12,X13] :
( ~ r1(sK0,X2)
| p2(sK12(X13))
| ~ r1(X12,X13)
| ~ r1(X2,X12)
| r1(X2,sK8(X2)) ),
inference(cnf_transformation,[],[f9]) ).
fof(f18,plain,
! [X2,X12,X13] :
( ~ r1(sK0,X2)
| r1(X13,sK12(X13))
| ~ r1(X12,X13)
| ~ r1(X2,X12)
| r1(X2,sK8(X2)) ),
inference(cnf_transformation,[],[f9]) ).
fof(f20,plain,
! [X2,X6,X9,X7] :
( ~ p2(X6)
| ~ r1(X6,X9)
| r1(X9,sK10(X9))
| p2(X7)
| ~ r1(X6,X7)
| ~ r1(X2,X6)
| ~ r1(sK0,X2) ),
inference(cnf_transformation,[],[f9]) ).
fof(f21,plain,
! [X2,X3] :
( ~ r1(sK0,X2)
| ~ r1(X2,X3)
| p2(sK9(X3)) ),
inference(cnf_transformation,[],[f9]) ).
fof(f23,plain,
! [X2,X3] :
( ~ r1(sK0,X2)
| ~ r1(X2,X3)
| r1(X3,sK9(X3)) ),
inference(cnf_transformation,[],[f9]) ).
fof(f27,plain,
! [X27] :
( ~ p2(sK7(X27))
| ~ r1(sK1,X27) ),
inference(cnf_transformation,[],[f9]) ).
fof(f28,plain,
! [X27] :
( r1(X27,sK7(X27))
| ~ r1(sK1,X27) ),
inference(cnf_transformation,[],[f9]) ).
fof(f35,plain,
r1(sK0,sK1),
inference(cnf_transformation,[],[f9]) ).
fof(f47,plain,
! [X0] :
( p2(sK9(X0))
| ~ r1(sK1,X0) ),
inference(resolution,[],[f21,f35]) ).
fof(f58,plain,
! [X0] :
( ~ r1(sK1,X0)
| r1(X0,sK9(X0)) ),
inference(resolution,[],[f23,f35]) ).
fof(f99,plain,
! [X0,X1] :
( p2(sK12(X0))
| ~ r1(X1,X0)
| ~ r1(sK1,X1)
| r1(sK1,sK8(sK1)) ),
inference(resolution,[],[f16,f35]) ).
fof(f102,definition,
( spl15_13
<=> r1(sK1,sK8(sK1)) ),
introduced(definition,[new_symbols(definition,[spl15_13])],[avatar_definition]) ).
fof(f104,plain,
( r1(sK1,sK8(sK1))
| ~ spl15_13 ),
inference(avatar_component_clause,[],[f102]) ).
fof(f106,definition,
( spl15_14
<=> ! [X0,X1] :
( p2(sK12(X0))
| ~ r1(sK1,X1)
| ~ r1(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl15_14])],[avatar_definition]) ).
fof(f107,plain,
( ! [X0,X1] :
( ~ r1(sK1,X1)
| p2(sK12(X0))
| ~ r1(X1,X0) )
| ~ spl15_14 ),
inference(avatar_component_clause,[],[f106]) ).
fof(f108,plain,
( spl15_13
| spl15_14 ),
inference(avatar_split_clause,[],[f99,f106,f102]) ).
fof(f118,plain,
! [X0,X1] :
( r1(X0,sK12(X0))
| ~ r1(X1,X0)
| ~ r1(sK1,X1)
| r1(sK1,sK8(sK1)) ),
inference(resolution,[],[f18,f35]) ).
fof(f121,definition,
( spl15_17
<=> ! [X0,X1] :
( r1(X0,sK12(X0))
| ~ r1(sK1,X1)
| ~ r1(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl15_17])],[avatar_definition]) ).
fof(f122,plain,
( ! [X0,X1] :
( ~ r1(sK1,X1)
| r1(X0,sK12(X0))
| ~ r1(X1,X0) )
| ~ spl15_17 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f123,plain,
( spl15_13
| spl15_17 ),
inference(avatar_split_clause,[],[f118,f121,f102]) ).
fof(f132,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK8(X1),sK9(X0))
| ~ r1(sK1,X0)
| p2(sK12(X2))
| ~ r1(X3,X2)
| ~ r1(X1,X3)
| ~ r1(sK0,X1) ),
inference(resolution,[],[f47,f13]) ).
fof(f135,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK1,X0)
| r1(X1,sK10(X1))
| p2(X2)
| ~ r1(sK9(X0),X2)
| ~ r1(X3,sK9(X0))
| ~ r1(sK0,X3)
| ~ r1(sK9(X0),X1) ),
inference(resolution,[],[f20,f47]) ).
fof(f145,plain,
! [X0] :
( p2(sK9(X0))
| ~ r1(sK0,X0) ),
inference(resolution,[],[f10,f21]) ).
fof(f260,plain,
( r1(sK8(sK1),sK9(sK8(sK1)))
| ~ spl15_13 ),
inference(resolution,[],[f58,f104]) ).
fof(f262,plain,
r1(sK1,sK9(sK1)),
inference(resolution,[],[f58,f10]) ).
fof(f386,plain,
( ! [X0,X1] :
( ~ p2(sK9(sK8(sK1)))
| r1(X0,sK12(X0))
| ~ r1(X1,X0)
| ~ r1(sK1,X1)
| ~ r1(sK0,sK1) )
| ~ spl15_13 ),
inference(resolution,[],[f260,f15]) ).
fof(f387,plain,
( ! [X0,X1] :
( ~ p2(sK9(sK8(sK1)))
| r1(X0,sK12(X0))
| ~ r1(X1,X0)
| ~ r1(sK1,X1) )
| ~ spl15_13 ),
inference(forward_subsumption_resolution,[],[f386,f35]) ).
fof(f390,definition,
( spl15_47
<=> p2(sK9(sK8(sK1))) ),
introduced(definition,[new_symbols(definition,[spl15_47])],[avatar_definition]) ).
fof(f392,plain,
( ~ p2(sK9(sK8(sK1)))
| spl15_47 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f393,plain,
( spl15_17
| ~ spl15_47
| ~ spl15_13 ),
inference(avatar_split_clause,[],[f387,f102,f390,f121]) ).
fof(f402,plain,
( ~ r1(sK1,sK8(sK1))
| spl15_47 ),
inference(resolution,[],[f392,f47]) ).
fof(f407,plain,
( ~ spl15_13
| spl15_47 ),
inference(avatar_split_clause,[],[f402,f390,f102]) ).
fof(f409,plain,
( ! [X0] :
( ~ r1(sK9(sK1),X0)
| p2(sK12(X0)) )
| ~ spl15_14 ),
inference(resolution,[],[f107,f262]) ).
fof(f414,plain,
( ! [X0] :
( ~ r1(sK9(sK1),X0)
| r1(X0,sK12(X0)) )
| ~ spl15_17 ),
inference(resolution,[],[f122,f262]) ).
fof(f983,plain,
! [X2,X0,X1] :
( r1(X0,sK10(X0))
| p2(X1)
| ~ r1(sK9(sK1),X1)
| ~ r1(X2,sK9(sK1))
| ~ r1(sK0,X2)
| ~ r1(sK9(sK1),X0) ),
inference(resolution,[],[f135,f10]) ).
fof(f985,definition,
( spl15_99
<=> ! [X2] :
( ~ r1(X2,sK9(sK1))
| ~ r1(sK0,X2) ) ),
introduced(definition,[new_symbols(definition,[spl15_99])],[avatar_definition]) ).
fof(f986,plain,
( ! [X2] :
( ~ r1(X2,sK9(sK1))
| ~ r1(sK0,X2) )
| ~ spl15_99 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f988,definition,
( spl15_100
<=> ! [X1] :
( p2(X1)
| ~ r1(sK9(sK1),X1) ) ),
introduced(definition,[new_symbols(definition,[spl15_100])],[avatar_definition]) ).
fof(f989,plain,
( ! [X1] :
( ~ r1(sK9(sK1),X1)
| p2(X1) )
| ~ spl15_100 ),
inference(avatar_component_clause,[],[f988]) ).
fof(f991,definition,
( spl15_101
<=> ! [X0] :
( r1(X0,sK10(X0))
| ~ r1(sK9(sK1),X0) ) ),
introduced(definition,[new_symbols(definition,[spl15_101])],[avatar_definition]) ).
fof(f992,plain,
( ! [X0] :
( ~ r1(sK9(sK1),X0)
| r1(X0,sK10(X0)) )
| ~ spl15_101 ),
inference(avatar_component_clause,[],[f991]) ).
fof(f993,plain,
( spl15_99
| spl15_100
| spl15_101 ),
inference(avatar_split_clause,[],[f983,f991,f988,f985]) ).
fof(f2152,plain,
( ~ r1(sK0,sK1)
| ~ spl15_99 ),
inference(resolution,[],[f986,f262]) ).
fof(f2153,plain,
( $false
| ~ spl15_99 ),
inference(forward_subsumption_resolution,[],[f2152,f35]) ).
fof(f2154,plain,
~ spl15_99,
inference(avatar_contradiction_clause,[],[f2153]) ).
fof(f2739,plain,
( r1(sK9(sK1),sK10(sK9(sK1)))
| ~ spl15_101 ),
inference(resolution,[],[f992,f10]) ).
fof(f3465,plain,
( r1(sK10(sK9(sK1)),sK12(sK10(sK9(sK1))))
| ~ spl15_17
| ~ spl15_101 ),
inference(resolution,[],[f2739,f414]) ).
fof(f3467,plain,
( p2(sK12(sK10(sK9(sK1))))
| ~ spl15_14
| ~ spl15_101 ),
inference(resolution,[],[f2739,f409]) ).
fof(f6672,definition,
( spl15_898
<=> ! [X2,X0,X1] :
( ~ r1(X0,sK9(sK1))
| ~ r1(sK0,X2)
| ~ r1(X2,X0)
| ~ r1(X0,X1)
| p2(X1)
| ~ p2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl15_898])],[avatar_definition]) ).
fof(f6673,plain,
( ! [X2,X0,X1] :
( ~ r1(X0,sK9(sK1))
| ~ r1(sK0,X2)
| ~ r1(X2,X0)
| ~ r1(X0,X1)
| p2(X1)
| ~ p2(X0) )
| ~ spl15_898 ),
inference(avatar_component_clause,[],[f6672]) ).
fof(f6684,plain,
( ! [X2,X0,X1] :
( ~ p2(sK12(sK10(sK9(sK1))))
| ~ r1(X0,sK9(sK1))
| ~ p2(X0)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| ~ r1(sK0,X2) )
| ~ spl15_17
| ~ spl15_101 ),
inference(resolution,[],[f3465,f11]) ).
fof(f6685,plain,
( ! [X2,X0,X1] :
( ~ r1(X0,sK9(sK1))
| ~ p2(X0)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(X2,X0)
| ~ r1(sK0,X2) )
| ~ spl15_14
| ~ spl15_17
| ~ spl15_101 ),
inference(forward_subsumption_resolution,[],[f6684,f3467]) ).
fof(f6687,plain,
( spl15_898
| ~ spl15_14
| ~ spl15_17
| ~ spl15_101 ),
inference(avatar_split_clause,[],[f6685,f991,f121,f106,f6672]) ).
fof(f13097,plain,
( ! [X0,X1] :
( ~ r1(sK0,X0)
| ~ r1(X0,sK9(sK1))
| ~ r1(sK9(sK1),X1)
| p2(X1)
| ~ p2(sK9(sK1)) )
| ~ spl15_898 ),
inference(resolution,[],[f6673,f10]) ).
fof(f13111,definition,
( spl15_1770
<=> p2(sK9(sK1)) ),
introduced(definition,[new_symbols(definition,[spl15_1770])],[avatar_definition]) ).
fof(f13113,plain,
( ~ p2(sK9(sK1))
| spl15_1770 ),
inference(avatar_component_clause,[],[f13111]) ).
fof(f13114,plain,
( ~ spl15_1770
| spl15_100
| spl15_99
| ~ spl15_898 ),
inference(avatar_split_clause,[],[f13097,f6672,f985,f988,f13111]) ).
fof(f13115,plain,
( ~ r1(sK0,sK1)
| spl15_1770 ),
inference(resolution,[],[f13113,f145]) ).
fof(f13121,plain,
( $false
| spl15_1770 ),
inference(forward_subsumption_resolution,[],[f13115,f35]) ).
fof(f13122,plain,
spl15_1770,
inference(avatar_contradiction_clause,[],[f13121]) ).
fof(f13131,plain,
( p2(sK7(sK9(sK1)))
| ~ r1(sK1,sK9(sK1))
| ~ spl15_100 ),
inference(resolution,[],[f989,f28]) ).
fof(f13134,plain,
( ~ r1(sK1,sK9(sK1))
| ~ spl15_100 ),
inference(forward_subsumption_resolution,[],[f13131,f27]) ).
fof(f13144,plain,
( $false
| ~ spl15_100 ),
inference(forward_subsumption_resolution,[],[f13134,f262]) ).
fof(f13145,plain,
~ spl15_100,
inference(avatar_contradiction_clause,[],[f13144]) ).
fof(f13190,plain,
( ! [X0,X1] :
( ~ r1(sK1,sK8(sK1))
| p2(sK12(X0))
| ~ r1(X1,X0)
| ~ r1(sK1,X1)
| ~ r1(sK0,sK1) )
| ~ spl15_13 ),
inference(resolution,[],[f260,f132]) ).
fof(f13195,plain,
( ! [X0,X1] :
( p2(sK12(X0))
| ~ r1(X1,X0)
| ~ r1(sK1,X1)
| ~ r1(sK0,sK1) )
| ~ spl15_13 ),
inference(forward_subsumption_resolution,[],[f13190,f16]) ).
fof(f13202,plain,
( ! [X0,X1] :
( p2(sK12(X0))
| ~ r1(X1,X0)
| ~ r1(sK1,X1) )
| ~ spl15_13 ),
inference(forward_subsumption_resolution,[],[f13195,f35]) ).
fof(f13208,plain,
( spl15_14
| ~ spl15_13 ),
inference(avatar_split_clause,[],[f13202,f102,f106]) ).
cnf(s8,plain,
( spl15_13
| spl15_14 ),
inference(sat_conversion,[],[f108]) ).
cnf(s10,plain,
( spl15_13
| spl15_17 ),
inference(sat_conversion,[],[f123]) ).
cnf(s43,plain,
( ~ spl15_13
| spl15_17
| ~ spl15_47 ),
inference(sat_conversion,[],[f393]) ).
cnf(s47,plain,
( ~ spl15_13
| spl15_47 ),
inference(sat_conversion,[],[f407]) ).
cnf(s118,plain,
( spl15_99
| spl15_100
| spl15_101 ),
inference(sat_conversion,[],[f993]) ).
cnf(s286,plain,
~ spl15_99,
inference(sat_conversion,[],[f2154]) ).
cnf(s980,plain,
( ~ spl15_14
| ~ spl15_17
| ~ spl15_101
| spl15_898 ),
inference(sat_conversion,[],[f6687]) ).
cnf(s1913,plain,
( spl15_99
| spl15_100
| ~ spl15_898
| ~ spl15_1770 ),
inference(sat_conversion,[],[f13114]) ).
cnf(s1916,plain,
spl15_1770,
inference(sat_conversion,[],[f13122]) ).
cnf(s1921,plain,
~ spl15_100,
inference(sat_conversion,[],[f13145]) ).
cnf(s1936,plain,
( ~ spl15_13
| spl15_14 ),
inference(sat_conversion,[],[f13208]) ).
cnf(s1937,plain,
( spl15_99
| ~ spl15_898 ),
inference(rat,[],[s1913,s1916,s1921]) ).
cnf(s1947,plain,
~ spl15_898,
inference(rat,[],[s1937,s286]) ).
cnf(s1975,plain,
spl15_101,
inference(rat,[],[s118,s1921,s286]) ).
cnf(s1985,plain,
spl15_13,
inference(rat,[],[s980,s8,s10,s1975,s1947]) ).
cnf(s1986,plain,
spl15_14,
inference(rat,[],[s1936,s1985]) ).
cnf(s1987,plain,
spl15_47,
inference(rat,[],[s47,s1985]) ).
cnf(s1988,plain,
~ spl15_17,
inference(rat,[],[s980,s1947,s1975,s1986]) ).
cnf(s1993,plain,
$false,
inference(rat,[],[s43,s1985,s1988,s1987]) ).
fof(f13209,plain,
$false,
inference(avatar_sat_refutation,[],[s1993]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL670+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n002.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 16:30:51 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.86/0.79 % (3719913)Will run a generic schedule for satisfiability detection.
% 1.86/0.79 % (3719928)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3327537186:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.86/0.79 % (3719924)% WARNING: option uhcvi not known.
% 1.86/0.79 % (3719924)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3113091509:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.86/0.79 % (3719927)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1396301084:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.86/0.79 % (3719926)dis+10_1_sil=32000:sp=arity:random_seed=87827521:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.86/0.79 % (3719925)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4137415068:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.86/0.79 % (3719929)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2259518054:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.86/0.79 % (3719923)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=747657774_2999 on theBenchmark for (2999ds/0Mi)
% 1.86/0.79 % TRYING [1]
% 1.86/0.79 % TRYING [2]
% 1.86/0.79 % TRYING [3]
% 1.86/0.79 % TRYING [4]
% 1.86/0.79 % TRYING [5]
% 1.86/0.79 % (3719928)Instruction limit reached!
% 1.86/0.79 % (3719928)------------------------------
% 1.86/0.79 % (3719928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.86/0.79 % (3719928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.86/0.79 % (3719928)CaDiCaL version: 2.1.3
% 1.86/0.79 % (3719928)Termination reason: Instruction limit
% 1.86/0.79 % (3719928)Termination phase: Saturation
% 1.86/0.79 % (3719928)Time elapsed: 0.044 s
% 1.86/0.79 % (3719928)Peak memory usage: 14 MB
% 1.86/0.79 % (3719928)Instructions burned: 134 (million)
% 1.86/0.79 % (3719943)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=491919682:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.86/0.79 % TRYING [1]
% 1.86/0.79 % TRYING [2]
% 1.86/0.79 % TRYING [3]
% 1.86/0.79 % TRYING [4]
% 1.86/0.79 % TRYING [5]
% 1.86/0.79 % (3719927)Instruction limit reached!
% 1.86/0.79 % (3719927)------------------------------
% 1.86/0.79 % (3719927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.86/0.79 % (3719927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.86/0.79 % (3719927)CaDiCaL version: 2.1.3
% 1.86/0.79 % (3719927)Termination reason: Instruction limit
% 1.86/0.79 % (3719927)Termination phase: Saturation
% 1.86/0.79 % (3719927)Time elapsed: 0.061 s
% 1.86/0.79 % (3719927)Peak memory usage: 12 MB
% 1.86/0.79 % (3719927)Instructions burned: 116 (million)
% 1.86/0.79 % (3719926)Instruction limit reached!
% 1.86/0.79 % (3719926)------------------------------
% 1.86/0.79 % (3719926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.86/0.79 % (3719926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.86/0.79 % (3719926)CaDiCaL version: 2.1.3
% 1.86/0.79 % (3719926)Termination reason: Instruction limit
% 1.86/0.79 % (3719926)Termination phase: Saturation
% 1.86/0.79 % (3719926)Time elapsed: 0.065 s
% 1.86/0.79 % (3719926)Peak memory usage: 13 MB
% 1.86/0.79 % (3719926)Instructions burned: 104 (million)
% 1.86/0.79 % TRYING [6]
% 1.86/0.79 % TRYING [6]
% 1.86/0.79 % (3719945)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=573525258:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.86/0.79 % (3719929)Instruction limit reached!
% 1.86/0.79 % (3719929)------------------------------
% 1.86/0.79 % (3719929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.86/0.79 % (3719929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.86/0.79 % (3719929)CaDiCaL version: 2.1.3
% 1.86/0.79 % (3719929)Termination reason: Instruction limit
% 1.86/0.79 % (3719929)Termination phase: Saturation
% 1.86/0.79 % (3719929)Time elapsed: 0.083 s
% 1.86/0.79 % (3719929)Peak memory usage: 12 MB
% 1.86/0.79 % (3719929)Instructions burned: 159 (million)
% 1.86/0.79 % (3719946)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=3493730922:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.86/0.79 % (3719948)ott-21_1_sil=16000:fs=off:random_seed=3120445504:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.86/0.79 % TRYING [7]
% 1.86/0.79 % (3719945)Instruction limit reached!
% 1.86/0.79 % (3719945)------------------------------
% 1.86/0.79 % (3719945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.86/0.79 % (3719945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.86/0.79 % (3719945)CaDiCaL version: 2.1.3
% 1.86/0.79 % (3719945)Termination reason: Instruction limit
% 1.86/0.79 % (3719945)Termination phase: Saturation
% 1.86/0.79 % (3719945)Time elapsed: 0.076 s
% 1.86/0.79 % (3719945)Peak memory usage: 13 MB
% 1.86/0.79 % (3719945)Instructions burned: 132 (million)
% 1.86/0.79 % (3719951)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2293405856:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.86/0.79 % TRYING [7]
% 1.86/0.79 % TRYING [8]
% 1.86/0.79 % (3719948)Instruction limit reached!
% 1.86/0.79 % (3719948)------------------------------
% 1.86/0.79 % (3719948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.86/0.79 % (3719948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.86/0.79 % (3719948)CaDiCaL version: 2.1.3
% 1.86/0.79 % (3719948)Termination reason: Instruction limit
% 1.86/0.79 % (3719948)Termination phase: Saturation
% 1.86/0.79 % (3719948)Time elapsed: 0.093 s
% 1.86/0.79 % (3719948)Peak memory usage: 13 MB
% 1.86/0.79 % (3719948)Instructions burned: 182 (million)
% 1.86/0.79 % (3719953)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3586847836:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.86/0.79 % TRYING [1]
% 1.86/0.79 % TRYING [2]
% 1.86/0.79 % TRYING [3]
% 1.86/0.79 % TRYING [4]
% 1.86/0.79 % TRYING [5]
% 1.86/0.79 % TRYING [6]
% 1.86/0.79 % (3719943)Instruction limit reached!
% 1.86/0.79 % (3719943)------------------------------
% 1.86/0.79 % (3719943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.86/0.79 % (3719943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.86/0.79 % (3719943)CaDiCaL version: 2.1.3
% 1.86/0.79 % (3719943)Termination reason: Instruction limit
% 1.86/0.79 % (3719943)Termination phase: Finite model building SAT solving
% 1.86/0.79 % (3719943)Time elapsed: 0.217 s
% 1.86/0.79 % (3719943)Peak memory usage: 13 MB
% 1.86/0.79 % (3719943)Instructions burned: 717 (million)
% 1.86/0.79 % (3719959)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2293847459:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.86/0.79 % TRYING [7]
% 1.86/0.79 % (3719924) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3719913-3719924"...
% 1.86/0.79 % (3719924)...printing done.
% 1.86/0.79 % (3719924)Refutation found. Thanks to Tanya!
% 1.86/0.79 % SZS status Theorem for theBenchmark
% 1.86/0.79 % SZS output start Proof for theBenchmark
% See solution above
% 1.86/0.80 % (3719924)------------------------------
% 1.86/0.80 % (3719924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.86/0.80 % (3719924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.86/0.80 % (3719924)CaDiCaL version: 2.1.3
% 1.86/0.80 % (3719924)Termination reason: Refutation
% 1.86/0.80 % (3719924)Time elapsed: 0.344 s
% 1.86/0.80 % (3719924)Peak memory usage: 19 MB
% 1.86/0.80 % (3719924)Instructions burned: 602 (million)
% 1.86/0.80 % (3719913)Success in time 0.376 s
% 1.86/0.80 % Vampire exiting
%------------------------------------------------------------------------------