%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR036+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:42:08 AM UTC 2026
% Result : Theorem 8.77s 3.18s
% Output : Refutation 0.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 35
% Syntax : Number of formulae : 139 ( 76 unt; 0 def)
% Number of atoms : 214 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 143 ( 68 ~; 65 |; 4 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 32 con; 0-0 aty)
% Number of variables : 87 ( 87 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f20,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_20) ).
fof(f70,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_70) ).
fof(f176,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_176) ).
fof(f227,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_227) ).
fof(f336,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_336) ).
fof(f460,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_460) ).
fof(f487,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_487) ).
fof(f512,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_512) ).
fof(f587,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_587) ).
fof(f615,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_615) ).
fof(f759,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_759) ).
fof(f783,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_783) ).
fof(f793,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_793) ).
fof(f814,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_814) ).
fof(f853,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_853) ).
fof(f867,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_867) ).
fof(f879,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_879) ).
fof(f940,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_940) ).
fof(f1248,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_1248) ).
fof(f1300,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_1300) ).
fof(f1366,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_1366) ).
fof(f1731,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_1731) ).
fof(f1760,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_1760) ).
fof(f1818,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_1818) ).
fof(f1975,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_1975) ).
fof(f2287,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_2287) ).
fof(f2436,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_2436) ).
fof(f2540,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_2540) ).
fof(f3253,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3253) ).
fof(f3764,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3764) ).
fof(f7584,axiom,
! [X0,X1] :
( disjointwith(X0,X1)
=> disjointwith(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_7584) ).
fof(f7585,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X1) )
=> disjointwith(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_7585) ).
fof(f7586,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X0) )
=> disjointwith(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_7586) ).
fof(f7991,axiom,
! [X0,X1,X2] :
( ( genls(X0,X1)
& genls(X1,X2) )
=> genls(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_7991) ).
fof(f8006,conjecture,
( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query136) ).
fof(f8007,negated_conjecture,
~ ( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(negated_conjecture,[status(cth)],[f8006]) ).
fof(f8008,plain,
( ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)
& mtvisible(c_tptp_member974_mt) ),
inference(ennf_transformation,[],[f8007]) ).
fof(f8011,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(ennf_transformation,[],[f7586]) ).
fof(f8012,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(flattening,[],[f8011]) ).
fof(f8013,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(ennf_transformation,[],[f7585]) ).
fof(f8014,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(flattening,[],[f8013]) ).
fof(f8015,plain,
! [X0,X1] :
( disjointwith(X1,X0)
| ~ disjointwith(X0,X1) ),
inference(ennf_transformation,[],[f7584]) ).
fof(f8032,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ),
inference(ennf_transformation,[],[f7991]) ).
fof(f8033,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ),
inference(flattening,[],[f8032]) ).
fof(f8566,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(cnf_transformation,[],[f8008]) ).
fof(f8568,plain,
! [X2,X0,X1] :
( ~ disjointwith(X0,X1)
| disjointwith(X2,X1)
| ~ genls(X2,X0) ),
inference(cnf_transformation,[],[f8012]) ).
fof(f8569,plain,
! [X2,X0,X1] :
( ~ disjointwith(X0,X1)
| disjointwith(X0,X2)
| ~ genls(X2,X1) ),
inference(cnf_transformation,[],[f8014]) ).
fof(f8570,plain,
! [X0,X1] :
( ~ disjointwith(X0,X1)
| disjointwith(X1,X0) ),
inference(cnf_transformation,[],[f8015]) ).
fof(f8584,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(cnf_transformation,[],[f512]) ).
fof(f8591,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(cnf_transformation,[],[f1300]) ).
fof(f8595,plain,
! [X2,X0,X1] :
( ~ genls(X1,X2)
| ~ genls(X0,X1)
| genls(X0,X2) ),
inference(cnf_transformation,[],[f8033]) ).
fof(f8621,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(cnf_transformation,[],[f2540]) ).
fof(f8631,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(cnf_transformation,[],[f1975]) ).
fof(f8640,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(cnf_transformation,[],[f1760]) ).
fof(f8651,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(cnf_transformation,[],[f1366]) ).
fof(f8660,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(cnf_transformation,[],[f3764]) ).
fof(f8672,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(cnf_transformation,[],[f879]) ).
fof(f8681,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(cnf_transformation,[],[f853]) ).
fof(f8691,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(cnf_transformation,[],[f487]) ).
fof(f8702,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(cnf_transformation,[],[f759]) ).
fof(f8713,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(cnf_transformation,[],[f70]) ).
fof(f8721,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(cnf_transformation,[],[f227]) ).
fof(f8732,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(cnf_transformation,[],[f1731]) ).
fof(f8741,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(cnf_transformation,[],[f615]) ).
fof(f8751,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(cnf_transformation,[],[f336]) ).
fof(f8763,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(cnf_transformation,[],[f940]) ).
fof(f8772,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(cnf_transformation,[],[f2436]) ).
fof(f8783,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(cnf_transformation,[],[f2287]) ).
fof(f8791,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(cnf_transformation,[],[f793]) ).
fof(f8803,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(cnf_transformation,[],[f20]) ).
fof(f8811,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(cnf_transformation,[],[f1818]) ).
fof(f8821,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(cnf_transformation,[],[f814]) ).
fof(f8832,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(cnf_transformation,[],[f783]) ).
fof(f8842,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(cnf_transformation,[],[f176]) ).
fof(f8856,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[],[f460]) ).
fof(f8869,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(cnf_transformation,[],[f587]) ).
fof(f8885,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[],[f3253]) ).
fof(f8907,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f867]) ).
fof(f8946,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f1248]) ).
fof(f9477,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1),
inference(resolution,[],[f8570,f8946]) ).
fof(f9484,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_1_65536)
| disjointwith(X0,c_tptpcol_1_1) ),
inference(resolution,[],[f9477,f8568]) ).
fof(f9517,plain,
! [X0] :
( genls(X0,c_tptpcol_5_69635)
| ~ genls(X0,c_tptpcol_6_71683) ),
inference(resolution,[],[f8595,f8803]) ).
fof(f9518,plain,
! [X0] :
( genls(X0,c_tptpcol_4_65539)
| ~ genls(X0,c_tptpcol_5_69635) ),
inference(resolution,[],[f8595,f8821]) ).
fof(f9519,plain,
! [X0] :
( genls(X0,c_tptpcol_9_22021)
| ~ genls(X0,c_tptpcol_10_22022) ),
inference(resolution,[],[f8595,f8713]) ).
fof(f9520,plain,
! [X0] :
( genls(X0,c_tptpcol_8_22020)
| ~ genls(X0,c_tptpcol_9_22021) ),
inference(resolution,[],[f8595,f8732]) ).
fof(f9528,plain,
! [X0] :
( genls(X0,c_tptpcol_3_65538)
| ~ genls(X0,c_tptpcol_4_65539) ),
inference(resolution,[],[f8595,f8842]) ).
fof(f9529,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_3_65538)
| genls(X0,c_tptpcol_2_65537) ),
inference(resolution,[],[f8595,f8869]) ).
fof(f9531,plain,
! [X0] :
( genls(X0,c_tptpcol_10_72710)
| ~ genls(X0,c_tptpcol_11_72774) ),
inference(resolution,[],[f8595,f8702]) ).
fof(f9532,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_10_72710)
| genls(X0,c_tptpcol_9_72709) ),
inference(resolution,[],[f8595,f8721]) ).
fof(f9533,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_9_72709)
| genls(X0,c_tptpcol_8_72708) ),
inference(resolution,[],[f8595,f8741]) ).
fof(f9538,plain,
! [X0] :
( genls(X0,c_tptpcol_7_21508)
| ~ genls(X0,c_tptpcol_8_22020) ),
inference(resolution,[],[f8595,f8751]) ).
fof(f9539,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_7_21508)
| genls(X0,c_tptpcol_6_20484) ),
inference(resolution,[],[f8595,f8772]) ).
fof(f9540,plain,
! [X0] :
( genls(X0,c_tptpcol_2_2)
| ~ genls(X0,c_tptpcol_3_16386) ),
inference(resolution,[],[f8595,f8856]) ).
fof(f9543,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_11_22023)
| genls(X0,c_tptpcol_10_22022) ),
inference(resolution,[],[f8595,f8691]) ).
fof(f9545,plain,
! [X0] :
( genls(X0,c_tptpcol_14_72792)
| ~ genls(X0,c_tptpcol_15_72793) ),
inference(resolution,[],[f8595,f8621]) ).
fof(f9549,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_12_22055)
| genls(X0,c_tptpcol_11_22023) ),
inference(resolution,[],[f8595,f8672]) ).
fof(f9551,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_2_65537)
| genls(X0,c_tptpcol_1_65536) ),
inference(resolution,[],[f8595,f8907]) ).
fof(f9552,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_8_72708)
| genls(X0,c_tptpcol_7_72707) ),
inference(resolution,[],[f8595,f8763]) ).
fof(f9557,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_6_20484)
| genls(X0,c_tptpcol_5_20483) ),
inference(resolution,[],[f8595,f8791]) ).
fof(f9560,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_12_72775)
| genls(X0,c_tptpcol_11_72774) ),
inference(resolution,[],[f8595,f8681]) ).
fof(f9563,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_7_72707)
| genls(X0,c_tptpcol_6_71683) ),
inference(resolution,[],[f8595,f8783]) ).
fof(f9568,plain,
! [X0] :
( genls(X0,c_tptpcol_13_22071)
| ~ genls(X0,c_tptpcol_14_22072) ),
inference(resolution,[],[f8595,f8631]) ).
fof(f9569,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_13_22071)
| genls(X0,c_tptpcol_12_22055) ),
inference(resolution,[],[f8595,f8651]) ).
fof(f9572,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_13_72791)
| genls(X0,c_tptpcol_12_72775) ),
inference(resolution,[],[f8595,f8660]) ).
fof(f9574,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_14_72792)
| genls(X0,c_tptpcol_13_72791) ),
inference(resolution,[],[f8595,f8640]) ).
fof(f9630,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_14_22072)
| genls(X0,c_tptpcol_12_22055) ),
inference(resolution,[],[f9569,f9568]) ).
fof(f9632,plain,
genls(c_tptpcol_15_22076,c_tptpcol_12_22055),
inference(resolution,[],[f9630,f8591]) ).
fof(f9633,plain,
genls(c_tptpcol_15_22076,c_tptpcol_11_22023),
inference(resolution,[],[f9632,f9549]) ).
fof(f9635,plain,
genls(c_tptpcol_15_22076,c_tptpcol_10_22022),
inference(resolution,[],[f9633,f9543]) ).
fof(f9656,plain,
! [X0] :
( genls(X0,c_tptpcol_6_20484)
| ~ genls(X0,c_tptpcol_8_22020) ),
inference(resolution,[],[f9538,f9539]) ).
fof(f9658,plain,
! [X0] :
( genls(X0,c_tptpcol_5_20483)
| ~ genls(X0,c_tptpcol_8_22020) ),
inference(resolution,[],[f9656,f9557]) ).
fof(f9667,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_4_65539)
| genls(X0,c_tptpcol_2_65537) ),
inference(resolution,[],[f9528,f9529]) ).
fof(f9669,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_5_69635)
| genls(X0,c_tptpcol_2_65537) ),
inference(resolution,[],[f9667,f9518]) ).
fof(f9671,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_6_71683)
| genls(X0,c_tptpcol_2_65537) ),
inference(resolution,[],[f9669,f9517]) ).
fof(f9674,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_15_72793)
| genls(X0,c_tptpcol_13_72791) ),
inference(resolution,[],[f9574,f9545]) ).
fof(f9676,plain,
genls(c_tptpcol_16_72795,c_tptpcol_13_72791),
inference(resolution,[],[f9674,f8584]) ).
fof(f9677,plain,
genls(c_tptpcol_16_72795,c_tptpcol_12_72775),
inference(resolution,[],[f9676,f9572]) ).
fof(f9679,plain,
genls(c_tptpcol_16_72795,c_tptpcol_11_72774),
inference(resolution,[],[f9677,f9560]) ).
fof(f9687,plain,
! [X0] :
( genls(X0,c_tptpcol_9_72709)
| ~ genls(X0,c_tptpcol_11_72774) ),
inference(resolution,[],[f9531,f9532]) ).
fof(f9689,plain,
! [X0] :
( genls(X0,c_tptpcol_8_72708)
| ~ genls(X0,c_tptpcol_11_72774) ),
inference(resolution,[],[f9687,f9533]) ).
fof(f9691,plain,
! [X0] :
( genls(X0,c_tptpcol_7_72707)
| ~ genls(X0,c_tptpcol_11_72774) ),
inference(resolution,[],[f9689,f9552]) ).
fof(f9693,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_11_72774)
| genls(X0,c_tptpcol_6_71683) ),
inference(resolution,[],[f9691,f9563]) ).
fof(f9700,plain,
genls(c_tptpcol_16_72795,c_tptpcol_6_71683),
inference(resolution,[],[f9693,f9679]) ).
fof(f9703,plain,
genls(c_tptpcol_16_72795,c_tptpcol_2_65537),
inference(resolution,[],[f9700,f9671]) ).
fof(f9705,plain,
genls(c_tptpcol_16_72795,c_tptpcol_1_65536),
inference(resolution,[],[f9703,f9551]) ).
fof(f9708,plain,
disjointwith(c_tptpcol_16_72795,c_tptpcol_1_1),
inference(resolution,[],[f9705,f9484]) ).
fof(f9717,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_1_1)
| disjointwith(c_tptpcol_16_72795,X0) ),
inference(resolution,[],[f9708,f8569]) ).
fof(f9722,plain,
disjointwith(c_tptpcol_16_72795,c_tptpcol_2_2),
inference(resolution,[],[f9717,f8885]) ).
fof(f9724,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_2_2)
| disjointwith(c_tptpcol_16_72795,X0) ),
inference(resolution,[],[f9722,f8569]) ).
fof(f9726,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_3_16386)
| disjointwith(c_tptpcol_16_72795,X0) ),
inference(resolution,[],[f9724,f9540]) ).
fof(f9728,plain,
disjointwith(c_tptpcol_16_72795,c_tptpcol_4_16387),
inference(resolution,[],[f9726,f8832]) ).
fof(f9764,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_4_16387)
| disjointwith(c_tptpcol_16_72795,X0) ),
inference(resolution,[],[f9728,f8569]) ).
fof(f9767,plain,
disjointwith(c_tptpcol_16_72795,c_tptpcol_5_20483),
inference(resolution,[],[f9764,f8811]) ).
fof(f9769,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_5_20483)
| disjointwith(c_tptpcol_16_72795,X0) ),
inference(resolution,[],[f9767,f8569]) ).
fof(f9771,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_8_22020)
| disjointwith(c_tptpcol_16_72795,X0) ),
inference(resolution,[],[f9769,f9658]) ).
fof(f9786,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_9_22021)
| disjointwith(c_tptpcol_16_72795,X0) ),
inference(resolution,[],[f9771,f9520]) ).
fof(f9788,plain,
! [X0] :
( disjointwith(c_tptpcol_16_72795,X0)
| ~ genls(X0,c_tptpcol_10_22022) ),
inference(resolution,[],[f9786,f9519]) ).
fof(f9790,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_10_22022)
| disjointwith(X0,c_tptpcol_16_72795) ),
inference(resolution,[],[f9788,f8570]) ).
fof(f9793,plain,
$false,
inference(unit_resulting_resolution,[],[f9790,f8566,f9635]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR036+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 % Computer : n015.cluster.edu
% 0.10/0.23 % Model : x86_64 x86_64
% 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.23 % Memory : 8046.5625MB
% 0.10/0.23 % OS : Linux 6.8.0-71-generic
% 0.10/0.23 % CPULimit : 300
% 0.10/0.23 % WCLimit : 300
% 0.10/0.23 % DateTime : Mon Sep 28 22:17:25 UTC 2026
% 0.10/0.23 % CPUTime :
% 0.10/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.24/0.29 Running first-order theorem proving
% 0.24/0.29 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.77/3.18 % (3088283)Detected formulas, will run a generic FOF schedule.
% 8.77/3.18 % (3088305)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=797834219:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 8.77/3.18 % (3088308)dis-21_1_sil=8000:lcm=predicate:random_seed=3615003447:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 8.77/3.18 % (3088305)Refutation not found, incomplete strategy
% 8.77/3.18 % (3088305)------------------------------
% 8.77/3.18 % (3088305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088305)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088305)Termination reason: Refutation not found, incomplete strategy
% 8.77/3.18 % (3088305)Time elapsed: 0.015 s
% 8.77/3.18 % (3088305)Peak memory usage: 93 MB
% 8.77/3.18 % (3088305)Instructions burned: 24 (million)
% 8.77/3.18 % (3088302)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2736024214:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 8.77/3.18 % (3088308)Instruction limit reached!
% 8.77/3.18 % (3088308)------------------------------
% 8.77/3.18 % (3088308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088308)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088308)Termination reason: Instruction limit
% 8.77/3.18 % (3088308)Termination phase: Saturation
% 8.77/3.18 % (3088308)Time elapsed: 0.085 s
% 8.77/3.18 % (3088308)Peak memory usage: 95 MB
% 8.77/3.18 % (3088308)Instructions burned: 130 (million)
% 8.77/3.18 % (3088306)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1126385040:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 8.77/3.18 % (3088307)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=7689074:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 8.77/3.18 % (3088304)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2582901468:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 8.77/3.18 % (3088303)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3602304612:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 8.77/3.18 % (3088306)Instruction limit reached!
% 8.77/3.18 % (3088306)------------------------------
% 8.77/3.18 % (3088306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088306)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088306)Termination reason: Instruction limit
% 8.77/3.18 % (3088306)Termination phase: Saturation
% 8.77/3.18 % (3088306)Time elapsed: 0.111 s
% 8.77/3.18 % (3088306)Peak memory usage: 93 MB
% 8.77/3.18 % (3088306)Instructions burned: 119 (million)
% 8.77/3.18 % (3088307)Instruction limit reached!
% 8.77/3.18 % (3088307)------------------------------
% 8.77/3.18 % (3088307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088307)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088307)Termination reason: Instruction limit
% 8.77/3.18 % (3088307)Termination phase: Property scanning
% 8.77/3.18 % (3088307)Time elapsed: 0.139 s
% 8.77/3.18 % (3088307)Peak memory usage: 93 MB
% 8.77/3.18 % (3088307)Instructions burned: 140 (million)
% 8.77/3.18 % (3088305)------------------------------
% 8.77/3.18 % (3088305)------------------------------
% 8.77/3.18 % (3088316)lrs+10_1_sil=8000:sp=occurrence:random_seed=466494344:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 8.77/3.18 % (3088316)Refutation not found, incomplete strategy
% 8.77/3.18 % (3088316)------------------------------
% 8.77/3.18 % (3088316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088316)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088316)Termination reason: Refutation not found, incomplete strategy
% 8.77/3.18 % (3088316)Time elapsed: 0.032 s
% 8.77/3.18 % (3088316)Peak memory usage: 94 MB
% 8.77/3.18 % (3088316)Instructions burned: 26 (million)
% 8.77/3.18 % (3088317)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1574527251:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/157Mi)
% 8.77/3.18 % (3088319)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2381547540:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 8.77/3.18 % (3088318)lrs+1011_1_sil=32000:sp=occurrence:random_seed=728285870:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 8.77/3.18 % (3088318)Refutation not found, incomplete strategy
% 8.77/3.18 % (3088318)------------------------------
% 8.77/3.18 % (3088318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088318)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088318)Termination reason: Refutation not found, incomplete strategy
% 8.77/3.18 % (3088318)Time elapsed: 0.024 s
% 8.77/3.18 % (3088318)Peak memory usage: 94 MB
% 8.77/3.18 % (3088318)Instructions burned: 20 (million)
% 8.77/3.18 % (3088317)Refutation not found, incomplete strategy
% 8.77/3.18 % (3088317)------------------------------
% 8.77/3.18 % (3088317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088317)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088317)Termination reason: Refutation not found, incomplete strategy
% 8.77/3.18 % (3088317)Time elapsed: 0.052 s
% 8.77/3.18 % (3088317)Peak memory usage: 94 MB
% 8.77/3.18 % (3088317)Instructions burned: 57 (million)
% 8.77/3.18 % (3088319)Instruction limit reached!
% 8.77/3.18 % (3088319)------------------------------
% 8.77/3.18 % (3088319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088319)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088319)Termination reason: Instruction limit
% 8.77/3.18 % (3088319)Termination phase: Saturation
% 8.77/3.18 % (3088319)Time elapsed: 0.132 s
% 8.77/3.18 % (3088319)Peak memory usage: 98 MB
% 8.77/3.18 % (3088319)Instructions burned: 249 (million)
% 8.77/3.18 % (3088316)------------------------------
% 8.77/3.18 % (3088316)------------------------------
% 8.77/3.18 % (3088326)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3047788454:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi)
% 8.77/3.18 % (3088318)------------------------------
% 8.77/3.18 % (3088318)------------------------------
% 8.77/3.18 % (3088317)------------------------------
% 8.77/3.18 % (3088317)------------------------------
% 8.77/3.18 % (3088326)Instruction limit reached!
% 8.77/3.18 % (3088326)------------------------------
% 8.77/3.18 % (3088326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088326)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088326)Termination reason: Instruction limit
% 8.77/3.18 % (3088326)Termination phase: Saturation
% 8.77/3.18 % (3088326)Time elapsed: 0.128 s
% 8.77/3.18 % (3088326)Peak memory usage: 94 MB
% 8.77/3.18 % (3088326)Instructions burned: 296 (million)
% 8.77/3.18 % (3088327)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4292919478:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 8.77/3.18 % (3088331)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=223572755:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 8.77/3.18 % (3088329)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=975258815:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 8.77/3.18 % (3088330)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3967527750:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 8.77/3.18 % (3088331)Instruction limit reached!
% 8.77/3.18 % (3088331)------------------------------
% 8.77/3.18 % (3088331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088331)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088331)Termination reason: Instruction limit
% 8.77/3.18 % (3088331)Termination phase: Saturation
% 8.77/3.18 % (3088331)Time elapsed: 0.059 s
% 8.77/3.18 % (3088331)Peak memory usage: 94 MB
% 8.77/3.18 % (3088331)Instructions burned: 115 (million)
% 8.77/3.18 % (3088329)Instruction limit reached!
% 8.77/3.18 % (3088329)------------------------------
% 8.77/3.18 % (3088329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088329)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088329)Termination reason: Instruction limit
% 8.77/3.18 % (3088329)Termination phase: Saturation
% 8.77/3.18 % (3088329)Time elapsed: 0.101 s
% 8.77/3.18 % (3088329)Peak memory usage: 94 MB
% 8.77/3.18 % (3088329)Instructions burned: 114 (million)
% 8.77/3.18 % (3088330)Instruction limit reached!
% 8.77/3.18 % (3088330)------------------------------
% 8.77/3.18 % (3088330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088330)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088330)Termination reason: Instruction limit
% 8.77/3.18 % (3088330)Termination phase: Blocked clause elimination
% 8.77/3.18 % (3088330)Time elapsed: 0.138 s
% 8.77/3.18 % (3088330)Peak memory usage: 95 MB
% 8.77/3.18 % (3088330)Instructions burned: 128 (million)
% 8.77/3.18 % (3088336)lrs+10_1_sil=8000:sp=occurrence:random_seed=2613029472:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 8.77/3.18 % (3088303)First to succeed.
% 8.77/3.18 % (3088303)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3088283"
% 8.77/3.18 % (3088337)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1068450672:i=437:sd=1:aac=none:ss=included_2983 on theBenchmark for (2983ds/437Mi)
% 8.77/3.18 % (3088336)Refutation not found, incomplete strategy
% 8.77/3.18 % (3088336)------------------------------
% 8.77/3.18 % (3088336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088336)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088336)Termination reason: Refutation not found, incomplete strategy
% 8.77/3.18 % (3088336)Time elapsed: 0.170 s
% 8.77/3.18 % (3088336)Peak memory usage: 95 MB
% 8.77/3.18 % (3088336)Instructions burned: 173 (million)
% 8.77/3.18 % (3088338)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2015022719:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 8.77/3.18 % (3088337)Instruction limit reached!
% 8.77/3.18 % (3088337)------------------------------
% 8.77/3.18 % (3088337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088337)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088337)Termination reason: Instruction limit
% 8.77/3.18 % (3088337)Termination phase: Saturation
% 8.77/3.18 % (3088337)Time elapsed: 0.154 s
% 8.77/3.18 % (3088337)Peak memory usage: 94 MB
% 8.77/3.18 % (3088337)Instructions burned: 440 (million)
% 8.77/3.18 % (3088342)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4001628808:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 8.77/3.18 % (3088342)Refutation not found, incomplete strategy
% 8.77/3.18 % (3088342)------------------------------
% 8.77/3.18 % (3088342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/3.18 % (3088342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/3.18 % (3088342)CaDiCaL version: 2.1.3
% 8.77/3.18 % (3088342)Termination reason: Refutation not found, incomplete strategy
% 8.77/3.18 % (3088342)Time elapsed: 0.025 s
% 8.77/3.18 % (3088342)Peak memory usage: 94 MB
% 8.77/3.18 % (3088342)Instructions burned: 39 (million)
% 8.77/3.18 % (3088303)Refutation found. Thanks to Tanya!
% 8.77/3.18 % SZS status Theorem for theBenchmark
% 8.77/3.18 % SZS output start Proof for theBenchmark
% See solution above
% 0.26/3.51 % (3088303)------------------------------
% 0.26/3.51 % (3088303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.26/3.51 % (3088303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.26/3.51 % (3088303)CaDiCaL version: 2.1.3
% 0.26/3.51 % (3088303)Termination reason: Refutation
% 0.26/3.51 % (3088303)Time elapsed: 1.393 s
% 0.26/3.51 % (3088303)Peak memory usage: 150 MB
% 0.26/3.51 % (3088303)Instructions burned: 1329 (million)
% 0.26/3.51 % (3088303)------------------------------
% 0.26/3.51 % (3088303)------------------------------
% 0.26/3.51 % (3088283)Success in time 2.291 s
% 0.26/3.51 % Vampire exiting
%------------------------------------------------------------------------------