%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR039+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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:44:32 AM UTC 2026
% Result : Theorem 10.71s 4.26s
% Output : Refutation 23.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 31
% Syntax : Number of formulae : 128 ( 85 unt; 0 def)
% Number of atoms : 181 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 102 ( 49 ~; 45 |; 3 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 30 con; 0-2 aty)
% Number of variables : 64 ( 64 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f806,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_806) ).
fof(f1192,axiom,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_1192) ).
fof(f2422,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_2422) ).
fof(f2718,axiom,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_2718) ).
fof(f2922,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_2922) ).
fof(f3246,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_3246) ).
fof(f3989,axiom,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_3989) ).
fof(f5324,axiom,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_5324) ).
fof(f5490,axiom,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_5490) ).
fof(f6009,axiom,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_6009) ).
fof(f8232,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_8232) ).
fof(f9361,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_9361) ).
fof(f10047,axiom,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_10047) ).
fof(f10276,axiom,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_10276) ).
fof(f10406,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_10406) ).
fof(f10474,axiom,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_10474) ).
fof(f13339,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_13339) ).
fof(f13628,axiom,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_13628) ).
fof(f14265,axiom,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_14265) ).
fof(f16825,axiom,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_16825) ).
fof(f17727,axiom,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_17727) ).
fof(f20157,axiom,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_20157) ).
fof(f20317,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_20317) ).
fof(f20749,axiom,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_20749) ).
fof(f21311,axiom,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_21311) ).
fof(f28195,axiom,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_28195) ).
fof(f28510,axiom,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_28510) ).
fof(f41386,axiom,
! [X0,X1] :
( disjointwith(X0,X1)
=> disjointwith(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_41386) ).
fof(f41387,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X1) )
=> disjointwith(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_41387) ).
fof(f41388,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X0) )
=> disjointwith(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_41388) ).
fof(f44217,conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))
=> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query189) ).
fof(f44218,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))
=> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ),
inference(negated_conjecture,[status(cth)],[f44217]) ).
fof(f64063,plain,
! [X0,X1] :
( disjointwith(X1,X0)
| ~ disjointwith(X0,X1) ),
inference(ennf_transformation,[],[f41386]) ).
fof(f64064,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(ennf_transformation,[],[f41387]) ).
fof(f64065,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(flattening,[],[f64064]) ).
fof(f64066,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(ennf_transformation,[],[f41388]) ).
fof(f64067,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(flattening,[],[f64066]) ).
fof(f66315,plain,
( ~ disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664)
& mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7)) ),
inference(ennf_transformation,[],[f44218]) ).
fof(f67111,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(cnf_transformation,[],[f806]) ).
fof(f67491,plain,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
inference(cnf_transformation,[],[f1192]) ).
fof(f68695,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f2422]) ).
fof(f68980,plain,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
inference(cnf_transformation,[],[f2718]) ).
fof(f69180,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[],[f2922]) ).
fof(f69501,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(cnf_transformation,[],[f3246]) ).
fof(f70226,plain,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
inference(cnf_transformation,[],[f3989]) ).
fof(f71532,plain,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
inference(cnf_transformation,[],[f5324]) ).
fof(f71694,plain,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
inference(cnf_transformation,[],[f5490]) ).
fof(f72202,plain,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
inference(cnf_transformation,[],[f6009]) ).
fof(f74384,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f8232]) ).
fof(f75490,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(cnf_transformation,[],[f9361]) ).
fof(f76165,plain,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
inference(cnf_transformation,[],[f10047]) ).
fof(f76389,plain,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
inference(cnf_transformation,[],[f10276]) ).
fof(f76517,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(cnf_transformation,[],[f10406]) ).
fof(f76584,plain,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
inference(cnf_transformation,[],[f10474]) ).
fof(f79396,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[],[f13339]) ).
fof(f79679,plain,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
inference(cnf_transformation,[],[f13628]) ).
fof(f80304,plain,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
inference(cnf_transformation,[],[f14265]) ).
fof(f82824,plain,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
inference(cnf_transformation,[],[f16825]) ).
fof(f83711,plain,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
inference(cnf_transformation,[],[f17727]) ).
fof(f86093,plain,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
inference(cnf_transformation,[],[f20157]) ).
fof(f86251,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(cnf_transformation,[],[f20317]) ).
fof(f86680,plain,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
inference(cnf_transformation,[],[f20749]) ).
fof(f87232,plain,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
inference(cnf_transformation,[],[f21311]) ).
fof(f93972,plain,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
inference(cnf_transformation,[],[f28195]) ).
fof(f94284,plain,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
inference(cnf_transformation,[],[f28510]) ).
fof(f105733,plain,
! [X0,X1] :
( ~ disjointwith(X0,X1)
| disjointwith(X1,X0) ),
inference(cnf_transformation,[],[f64063]) ).
fof(f105734,plain,
! [X2,X0,X1] :
( ~ genls(X2,X1)
| ~ disjointwith(X0,X1)
| disjointwith(X0,X2) ),
inference(cnf_transformation,[],[f64065]) ).
fof(f105735,plain,
! [X2,X0,X1] :
( ~ genls(X2,X0)
| ~ disjointwith(X0,X1)
| disjointwith(X2,X1) ),
inference(cnf_transformation,[],[f64067]) ).
fof(f108042,plain,
~ disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),
inference(cnf_transformation,[],[f66315]) ).
fof(f114027,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(consistent_polarity_flipping,[],[f74384]) ).
fof(f135227,plain,
! [X0,X1] :
( ~ disjointwith(X1,X0)
| disjointwith(X0,X1) ),
inference(consistent_polarity_flipping,[],[f105733]) ).
fof(f135228,plain,
! [X2,X0,X1] :
( ~ disjointwith(X0,X2)
| disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(consistent_polarity_flipping,[],[f105734]) ).
fof(f135229,plain,
! [X2,X0,X1] :
( ~ disjointwith(X2,X1)
| disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(consistent_polarity_flipping,[],[f105735]) ).
fof(f136429,plain,
disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),
inference(consistent_polarity_flipping,[],[f108042]) ).
fof(f192868,plain,
! [X0] :
( ~ genls(c_tptpcol_13_18664,X0)
| disjointwith(c_tptpcol_15_93775,X0) ),
inference(resolution,[],[f135228,f136429]) ).
fof(f192872,plain,
disjointwith(c_tptpcol_15_93775,c_tptpcol_12_18663),
inference(resolution,[],[f192868,f72202]) ).
fof(f192874,plain,
! [X0] :
( ~ genls(c_tptpcol_15_93775,X0)
| disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[],[f192872,f135229]) ).
fof(f192958,plain,
disjointwith(c_tptpcol_14_93774,c_tptpcol_12_18663),
inference(resolution,[],[f192874,f94284]) ).
fof(f192960,plain,
! [X0] :
( ~ genls(c_tptpcol_14_93774,X0)
| disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[],[f192958,f135229]) ).
fof(f193030,plain,
disjointwith(c_tptpcol_13_93766,c_tptpcol_12_18663),
inference(resolution,[],[f192960,f76165]) ).
fof(f193034,plain,
! [X0] :
( ~ genls(c_tptpcol_13_93766,X0)
| disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[],[f193030,f135229]) ).
fof(f193090,plain,
disjointwith(c_tptpcol_12_93765,c_tptpcol_12_18663),
inference(resolution,[],[f193034,f71694]) ).
fof(f193092,plain,
! [X0] :
( ~ genls(c_tptpcol_12_93765,X0)
| disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[],[f193090,f135229]) ).
fof(f193197,plain,
disjointwith(c_tptpcol_11_93764,c_tptpcol_12_18663),
inference(resolution,[],[f193092,f71532]) ).
fof(f193199,plain,
! [X0] :
( ~ genls(c_tptpcol_11_93764,X0)
| disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[],[f193197,f135229]) ).
fof(f193316,plain,
disjointwith(c_tptpcol_10_93700,c_tptpcol_12_18663),
inference(resolution,[],[f193199,f83711]) ).
fof(f193318,plain,
! [X0] :
( ~ genls(c_tptpcol_10_93700,X0)
| disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[],[f193316,f135229]) ).
fof(f193460,plain,
disjointwith(c_tptpcol_9_93699,c_tptpcol_12_18663),
inference(resolution,[],[f193318,f67491]) ).
fof(f193462,plain,
! [X0] :
( ~ genls(c_tptpcol_9_93699,X0)
| disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[],[f193460,f135229]) ).
fof(f193570,plain,
disjointwith(c_tptpcol_8_93698,c_tptpcol_12_18663),
inference(resolution,[],[f193462,f87232]) ).
fof(f193572,plain,
! [X0] :
( ~ genls(c_tptpcol_8_93698,X0)
| disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[],[f193570,f135229]) ).
fof(f193689,plain,
disjointwith(c_tptpcol_7_93186,c_tptpcol_12_18663),
inference(resolution,[],[f193572,f93972]) ).
fof(f193691,plain,
! [X0] :
( ~ genls(c_tptpcol_7_93186,X0)
| disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[],[f193689,f135229]) ).
fof(f193825,plain,
disjointwith(c_tptpcol_6_92162,c_tptpcol_12_18663),
inference(resolution,[],[f193691,f82824]) ).
fof(f193827,plain,
! [X0] :
( ~ genls(c_tptpcol_6_92162,X0)
| disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[],[f193825,f135229]) ).
fof(f194026,plain,
disjointwith(c_tptpcol_5_90114,c_tptpcol_12_18663),
inference(resolution,[],[f193827,f75490]) ).
fof(f194028,plain,
! [X0] :
( ~ genls(c_tptpcol_5_90114,X0)
| disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[],[f194026,f135229]) ).
fof(f194286,plain,
disjointwith(c_tptpcol_4_90113,c_tptpcol_12_18663),
inference(resolution,[],[f194028,f86251]) ).
fof(f194290,plain,
! [X0] :
( ~ genls(c_tptpcol_4_90113,X0)
| disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[],[f194286,f135229]) ).
fof(f194635,plain,
disjointwith(c_tptpcol_3_81921,c_tptpcol_12_18663),
inference(resolution,[],[f194290,f76517]) ).
fof(f194637,plain,
! [X0] :
( ~ genls(c_tptpcol_3_81921,X0)
| disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[],[f194635,f135229]) ).
fof(f194963,plain,
disjointwith(c_tptpcol_2_65537,c_tptpcol_12_18663),
inference(resolution,[],[f194637,f67111]) ).
fof(f194965,plain,
! [X0] :
( ~ genls(c_tptpcol_2_65537,X0)
| disjointwith(X0,c_tptpcol_12_18663) ),
inference(resolution,[],[f194963,f135229]) ).
fof(f195305,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_12_18663),
inference(resolution,[],[f194965,f68695]) ).
fof(f195310,plain,
! [X0] :
( ~ genls(c_tptpcol_12_18663,X0)
| disjointwith(c_tptpcol_1_65536,X0) ),
inference(resolution,[],[f195305,f135228]) ).
fof(f195701,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_11_18631),
inference(resolution,[],[f195310,f80304]) ).
fof(f195707,plain,
! [X0] :
( ~ genls(c_tptpcol_11_18631,X0)
| disjointwith(c_tptpcol_1_65536,X0) ),
inference(resolution,[],[f195701,f135228]) ).
fof(f196089,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_10_18567),
inference(resolution,[],[f195707,f86093]) ).
fof(f196092,plain,
! [X0] :
( ~ genls(c_tptpcol_10_18567,X0)
| disjointwith(c_tptpcol_1_65536,X0) ),
inference(resolution,[],[f196089,f135228]) ).
fof(f196442,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_9_18439),
inference(resolution,[],[f196092,f70226]) ).
fof(f196453,plain,
! [X0] :
( ~ genls(c_tptpcol_9_18439,X0)
| disjointwith(c_tptpcol_1_65536,X0) ),
inference(resolution,[],[f196442,f135228]) ).
fof(f196775,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_8_18438),
inference(resolution,[],[f196453,f79679]) ).
fof(f196780,plain,
! [X0] :
( ~ genls(c_tptpcol_8_18438,X0)
| disjointwith(c_tptpcol_1_65536,X0) ),
inference(resolution,[],[f196775,f135228]) ).
fof(f197072,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_7_18437),
inference(resolution,[],[f196780,f76584]) ).
fof(f197075,plain,
! [X0] :
( ~ genls(c_tptpcol_7_18437,X0)
| disjointwith(c_tptpcol_1_65536,X0) ),
inference(resolution,[],[f197072,f135228]) ).
fof(f197392,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_6_18436),
inference(resolution,[],[f197075,f68980]) ).
fof(f197395,plain,
! [X0] :
( ~ genls(c_tptpcol_6_18436,X0)
| disjointwith(c_tptpcol_1_65536,X0) ),
inference(resolution,[],[f197392,f135228]) ).
fof(f197650,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_5_16388),
inference(resolution,[],[f197395,f76389]) ).
fof(f197654,plain,
! [X0] :
( ~ genls(c_tptpcol_5_16388,X0)
| disjointwith(c_tptpcol_1_65536,X0) ),
inference(resolution,[],[f197650,f135228]) ).
fof(f197907,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_4_16387),
inference(resolution,[],[f197654,f86680]) ).
fof(f197911,plain,
! [X0] :
( ~ genls(c_tptpcol_4_16387,X0)
| disjointwith(c_tptpcol_1_65536,X0) ),
inference(resolution,[],[f197907,f135228]) ).
fof(f198127,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_3_16386),
inference(resolution,[],[f197911,f69501]) ).
fof(f198131,plain,
! [X0] :
( ~ genls(c_tptpcol_3_16386,X0)
| disjointwith(c_tptpcol_1_65536,X0) ),
inference(resolution,[],[f198127,f135228]) ).
fof(f198328,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_2_2),
inference(resolution,[],[f198131,f79396]) ).
fof(f198335,plain,
! [X0] :
( ~ genls(c_tptpcol_2_2,X0)
| disjointwith(c_tptpcol_1_65536,X0) ),
inference(resolution,[],[f198328,f135228]) ).
fof(f198500,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1),
inference(resolution,[],[f198335,f69180]) ).
fof(f198504,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(resolution,[],[f198500,f135227]) ).
fof(f198505,plain,
$false,
inference(forward_subsumption_resolution,[],[f198504,f114027]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR039+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n013.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 22:14:21 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.71/4.26 % (1644135)Will run a generic schedule for satisfiability detection.
% 10.71/4.26 % (1644140)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=76350685_2991 on theBenchmark for (2991ds/0Mi)
% 10.71/4.26 % (1644141)% WARNING: option uhcvi not known.
% 10.71/4.26 % (1644141)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=611398374:i=135531:add=off:rawr=on_2991 on theBenchmark for (2991ds/135531Mi)
% 10.71/4.26 % (1644142)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1906717905:i=88024:add=on:rawr=on_2991 on theBenchmark for (2991ds/88024Mi)
% 10.71/4.26 % (1644143)dis+10_1_sil=32000:sp=arity:random_seed=49443711:i=103:fgj=on_2991 on theBenchmark for (2991ds/103Mi)
% 10.71/4.26 % (1644144)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3549086653:i=116_2991 on theBenchmark for (2991ds/116Mi)
% 10.71/4.26 % (1644145)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2205570059:i=131_2991 on theBenchmark for (2991ds/131Mi)
% 10.71/4.26 % (1644146)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3896219820:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2991 on theBenchmark for (2991ds/159Mi)
% 10.71/4.26 % (1644143)Instruction limit reached!
% 10.71/4.26 % (1644143)------------------------------
% 10.71/4.26 % (1644143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644143)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644143)Termination reason: Instruction limit
% 10.71/4.26 % (1644143)Termination phase: Preprocessing 2
% 10.71/4.26 % (1644143)Time elapsed: 0.089 s
% 10.71/4.26 % (1644143)Peak memory usage: 61 MB
% 10.71/4.26 % (1644143)Instructions burned: 105 (million)
% 10.71/4.26 % (1644144)Instruction limit reached!
% 10.71/4.26 % (1644144)------------------------------
% 10.71/4.26 % (1644144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644144)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644144)Termination reason: Instruction limit
% 10.71/4.26 % (1644144)Termination phase: Preprocessing 2
% 10.71/4.26 % (1644144)Time elapsed: 0.098 s
% 10.71/4.26 % (1644144)Peak memory usage: 61 MB
% 10.71/4.26 % (1644144)Instructions burned: 117 (million)
% 10.71/4.26 % (1644154)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=291670670:i=714:nm=2_2990 on theBenchmark for (2990ds/714Mi)
% 10.71/4.26 % (1644146)Instruction limit reached!
% 10.71/4.26 % (1644146)------------------------------
% 10.71/4.26 % (1644146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644146)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644146)Termination reason: Instruction limit
% 10.71/4.26 % (1644146)Termination phase: Naming
% 10.71/4.26 % (1644146)Time elapsed: 0.116 s
% 10.71/4.26 % (1644146)Peak memory usage: 62 MB
% 10.71/4.26 % (1644146)Instructions burned: 162 (million)
% 10.71/4.26 % (1644145)Instruction limit reached!
% 10.71/4.26 % (1644145)------------------------------
% 10.71/4.26 % (1644145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644145)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644145)Termination reason: Instruction limit
% 10.71/4.26 % (1644145)Termination phase: Preprocessing 2
% 10.71/4.26 % (1644145)Time elapsed: 0.120 s
% 10.71/4.26 % (1644145)Peak memory usage: 61 MB
% 10.71/4.26 % (1644145)Instructions burned: 131 (million)
% 10.71/4.26 % (1644155)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2716379538:i=131:bd=preordered:fsd=on_2990 on theBenchmark for (2990ds/131Mi)
% 10.71/4.26 % (1644158)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=4102610787:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2990 on theBenchmark for (2990ds/684Mi)
% 10.71/4.26 % (1644159)ott-21_1_sil=16000:fs=off:random_seed=1546170905:i=180:av=off:fsr=off_2989 on theBenchmark for (2989ds/180Mi)
% 10.71/4.26 % (1644155)Instruction limit reached!
% 10.71/4.26 % (1644155)------------------------------
% 10.71/4.26 % (1644155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644155)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644155)Termination reason: Instruction limit
% 10.71/4.26 % (1644155)Termination phase: Preprocessing 2
% 10.71/4.26 % (1644155)Time elapsed: 0.105 s
% 10.71/4.26 % (1644155)Peak memory usage: 61 MB
% 10.71/4.26 % (1644155)Instructions burned: 131 (million)
% 10.71/4.26 % (1644162)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2320351418:i=477:bd=all_2988 on theBenchmark for (2988ds/477Mi)
% 10.71/4.26 % (1644159)Instruction limit reached!
% 10.71/4.26 % (1644159)------------------------------
% 10.71/4.26 % (1644159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644159)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644159)Termination reason: Instruction limit
% 10.71/4.26 % (1644159)Termination phase: Preprocessing 3
% 10.71/4.26 % (1644159)Time elapsed: 0.147 s
% 10.71/4.26 % (1644159)Peak memory usage: 62 MB
% 10.71/4.26 % (1644159)Instructions burned: 182 (million)
% 10.71/4.26 % (1644164)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=725008081:fmbsr=1.3:i=865:ins=25_2988 on theBenchmark for (2988ds/865Mi)
% 10.71/4.26 % (1644154)Instruction limit reached!
% 10.71/4.26 % (1644154)------------------------------
% 10.71/4.26 % (1644154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644154)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644154)Termination reason: Instruction limit
% 10.71/4.26 % (1644154)Termination phase: Finite model building preprocessing
% 10.71/4.26 % (1644154)Time elapsed: 0.397 s
% 10.71/4.26 % (1644154)Peak memory usage: 68 MB
% 10.71/4.26 % (1644154)Instructions burned: 715 (million)
% 10.71/4.26 % (1644162)Instruction limit reached!
% 10.71/4.26 % (1644162)------------------------------
% 10.71/4.26 % (1644162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644162)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644162)Termination reason: Instruction limit
% 10.71/4.26 % (1644162)Termination phase: Property scanning
% 10.71/4.26 % (1644162)Time elapsed: 0.280 s
% 10.71/4.26 % (1644162)Peak memory usage: 66 MB
% 10.71/4.26 % (1644162)Instructions burned: 477 (million)
% 10.71/4.26 % (1644166)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1472755651:i=1179_2986 on theBenchmark for (2986ds/1179Mi)
% 10.71/4.26 % (1644168)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3701467077:i=889:ins=1_2985 on theBenchmark for (2985ds/889Mi)
% 10.71/4.26 % (1644158)Instruction limit reached!
% 10.71/4.26 % (1644158)------------------------------
% 10.71/4.26 % (1644158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644158)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644158)Termination reason: Instruction limit
% 10.71/4.26 % (1644158)Termination phase: Property scanning
% 10.71/4.26 % (1644158)Time elapsed: 0.440 s
% 10.71/4.26 % (1644158)Peak memory usage: 73 MB
% 10.71/4.26 % (1644158)Instructions burned: 684 (million)
% 10.71/4.26 % (1644170)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=911803981:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2985 on theBenchmark for (2985ds/692Mi)
% 10.71/4.26 % TRYING [1]
% 10.71/4.26 % TRYING [2]
% 10.71/4.26 % (1644164)Instruction limit reached!
% 10.71/4.26 % (1644164)------------------------------
% 10.71/4.26 % (1644164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644164)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644164)Termination reason: Instruction limit
% 10.71/4.26 % (1644164)Termination phase: Finite model building preprocessing
% 10.71/4.26 % (1644164)Time elapsed: 0.654 s
% 10.71/4.26 % (1644164)Peak memory usage: 86 MB
% 10.71/4.26 % (1644164)Instructions burned: 866 (million)
% 10.71/4.26 % (1644172)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=303556778:i=879:kws=inv_precedence:fsr=off_2981 on theBenchmark for (2981ds/879Mi)
% 10.71/4.26 % (1644170)Instruction limit reached!
% 10.71/4.26 % (1644170)------------------------------
% 10.71/4.26 % (1644170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644170)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644170)Termination reason: Instruction limit
% 10.71/4.26 % (1644170)Termination phase: shuffling
% 10.71/4.26 % (1644170)Time elapsed: 0.469 s
% 10.71/4.26 % (1644170)Peak memory usage: 79 MB
% 10.71/4.26 % (1644170)Instructions burned: 693 (million)
% 10.71/4.26 % (1644168)Instruction limit reached!
% 10.71/4.26 % (1644168)------------------------------
% 10.71/4.26 % (1644168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644168)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644168)Termination reason: Instruction limit
% 10.71/4.26 % (1644168)Termination phase: Finite model building preprocessing
% 10.71/4.26 % (1644168)Time elapsed: 0.525 s
% 10.71/4.26 % (1644168)Peak memory usage: 86 MB
% 10.71/4.26 % (1644168)Instructions burned: 892 (million)
% 10.71/4.26 % (1644174)fmb+10_1_sil=64000:random_seed=2891076322:i=22061:nm=2:gsp=on_2980 on theBenchmark for (2980ds/22061Mi)
% 10.71/4.26 % (1644175)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3665808667:i=9515:nm=5_2980 on theBenchmark for (2980ds/9515Mi)
% 10.71/4.26 % (1644166)Instruction limit reached!
% 10.71/4.26 % (1644166)------------------------------
% 10.71/4.26 % (1644166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644166)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644166)Termination reason: Instruction limit
% 10.71/4.26 % (1644166)Termination phase: Saturation
% 10.71/4.26 % (1644166)Time elapsed: 0.663 s
% 10.71/4.26 % (1644166)Peak memory usage: 81 MB
% 10.71/4.26 % (1644166)Instructions burned: 1179 (million)
% 10.71/4.26 % TRYING [3]
% 10.71/4.26 % (1644178)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=697123859:fmbsr=1.7:i=920_2979 on theBenchmark for (2979ds/920Mi)
% 10.71/4.26 % (1644172)Instruction limit reached!
% 10.71/4.26 % (1644172)------------------------------
% 10.71/4.26 % (1644172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644172)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644172)Termination reason: Instruction limit
% 10.71/4.26 % (1644172)Termination phase: Saturation
% 10.71/4.26 % (1644172)Time elapsed: 0.537 s
% 10.71/4.26 % (1644172)Peak memory usage: 91 MB
% 10.71/4.26 % (1644172)Instructions burned: 880 (million)
% 10.71/4.26 % (1644180)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3664247742:i=5131_2975 on theBenchmark for (2975ds/5131Mi)
% 10.71/4.26 % (1644178)Instruction limit reached!
% 10.71/4.26 % (1644178)------------------------------
% 10.71/4.26 % (1644178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644178)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644178)Termination reason: Instruction limit
% 10.71/4.26 % (1644178)Termination phase: Finite model building preprocessing
% 10.71/4.26 % (1644178)Time elapsed: 0.516 s
% 10.71/4.26 % (1644178)Peak memory usage: 79 MB
% 10.71/4.26 % (1644178)Instructions burned: 921 (million)
% 10.71/4.26 % TRYING [4]
% 10.71/4.26 % (1644182)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1394950019:i=1472:ins=7:fdi=8:gsp=on_2973 on theBenchmark for (2973ds/1472Mi)
% 10.71/4.26 % TRYING [1]
% 10.71/4.26 % (1644182)Instruction limit reached!
% 10.71/4.26 % (1644182)------------------------------
% 10.71/4.26 % (1644182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.71/4.26 % (1644182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/4.26 % (1644182)CaDiCaL version: 2.1.3
% 10.71/4.26 % (1644182)Termination reason: Instruction limit
% 10.71/4.26 % (1644182)Termination phase: Saturation
% 10.71/4.26 % (1644182)Time elapsed: 0.748 s
% 10.71/4.26 % (1644182)Peak memory usage: 82 MB
% 10.71/4.26 % (1644182)Instructions burned: 1472 (million)
% 10.71/4.26 % (1644184)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=831326215:i=6324_2965 on theBenchmark for (2965ds/6324Mi)
% 10.71/4.26 % TRYING [20]
% 10.71/4.26 % TRYING [5]
% 10.71/4.26 % (1644141) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1644135-1644141"...
% 10.71/4.26 % (1644141)...printing done.
% 10.71/4.26 % (1644141)Refutation found. Thanks to Tanya!
% 10.71/4.26 % SZS status Theorem for theBenchmark
% 10.71/4.26 % SZS output start Proof for theBenchmark
% See solution above
% 23.31/4.33 % (1644141)------------------------------
% 23.31/4.33 % (1644141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.31/4.33 % (1644141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.31/4.33 % (1644141)CaDiCaL version: 2.1.3
% 23.31/4.33 % (1644141)Termination reason: Refutation
% 23.31/4.33 % (1644141)Time elapsed: 3.019 s
% 23.31/4.33 % (1644141)Peak memory usage: 123 MB
% 23.31/4.33 % (1644141)Instructions burned: 4567 (million)
% 23.31/4.33 % (1644135)Success in time 4.024 s
% 23.31/4.33 % Vampire exiting
%------------------------------------------------------------------------------