%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR049+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:19 AM UTC 2026
% Result : Theorem 8.56s 2.79s
% Output : Refutation 10.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 36
% Syntax : Number of formulae : 143 ( 78 unt; 0 def)
% Number of atoms : 228 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 163 ( 78 ~; 75 |; 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 : 33 ( 33 usr; 33 con; 0-0 aty)
% Number of variables : 97 ( 97 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f49,axiom,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_49) ).
fof(f189,axiom,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_189) ).
fof(f520,axiom,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_520) ).
fof(f806,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_806) ).
fof(f1105,axiom,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_1105) ).
fof(f1204,axiom,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_1204) ).
fof(f2422,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_2422) ).
fof(f2922,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_2922) ).
fof(f3272,axiom,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_3272) ).
fof(f3362,axiom,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_3362) ).
fof(f3393,axiom,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_3393) ).
fof(f3909,axiom,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_3909) ).
fof(f4037,axiom,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_4037) ).
fof(f4089,axiom,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_4089) ).
fof(f4455,axiom,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_4455) ).
fof(f4910,axiom,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_4910) ).
fof(f5291,axiom,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_5291) ).
fof(f7779,axiom,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_7779) ).
fof(f8232,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_8232) ).
fof(f8720,axiom,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_8720) ).
fof(f9361,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_9361) ).
fof(f10406,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_10406) ).
fof(f13065,axiom,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_13065) ).
fof(f13339,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_13339) ).
fof(f13777,axiom,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_13777) ).
fof(f14758,axiom,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_14758) ).
fof(f17053,axiom,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_17053) ).
fof(f17208,axiom,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_17208) ).
fof(f20317,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_20317) ).
fof(f25099,axiom,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_25099) ).
fof(f28270,axiom,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_28270) ).
fof(f41386,axiom,
! [X0,X1] :
( disjointwith(X0,X1)
=> disjointwith(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_41386) ).
fof(f41387,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X1) )
=> disjointwith(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_41387) ).
fof(f41388,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X0) )
=> disjointwith(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_41388) ).
fof(f44178,axiom,
! [X0,X1,X2] :
( ( genls(X0,X1)
& genls(X1,X2) )
=> genls(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_44178) ).
fof(f44217,conjecture,
( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query199) ).
fof(f44218,negated_conjecture,
~ ( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
inference(negated_conjecture,[status(cth)],[f44217]) ).
fof(f44219,plain,
( ~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)
& mtvisible(c_unitedstatesgeographypeoplemt) ),
inference(ennf_transformation,[],[f44218]) ).
fof(f44222,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(ennf_transformation,[],[f41388]) ).
fof(f44223,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(flattening,[],[f44222]) ).
fof(f44224,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(ennf_transformation,[],[f41387]) ).
fof(f44225,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(flattening,[],[f44224]) ).
fof(f44226,plain,
! [X0,X1] :
( disjointwith(X1,X0)
| ~ disjointwith(X0,X1) ),
inference(ennf_transformation,[],[f41386]) ).
fof(f44243,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ),
inference(ennf_transformation,[],[f44178]) ).
fof(f44244,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ),
inference(flattening,[],[f44243]) ).
fof(f44903,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),
inference(cnf_transformation,[],[f44219]) ).
fof(f44906,plain,
! [X2,X0,X1] :
( ~ disjointwith(X0,X1)
| disjointwith(X2,X1)
| ~ genls(X2,X0) ),
inference(cnf_transformation,[],[f44223]) ).
fof(f44907,plain,
! [X2,X0,X1] :
( ~ disjointwith(X0,X1)
| disjointwith(X0,X2)
| ~ genls(X2,X1) ),
inference(cnf_transformation,[],[f44225]) ).
fof(f44908,plain,
! [X0,X1] :
( ~ disjointwith(X0,X1)
| disjointwith(X1,X0) ),
inference(cnf_transformation,[],[f44226]) ).
fof(f44926,plain,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
inference(cnf_transformation,[],[f14758]) ).
fof(f44930,plain,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
inference(cnf_transformation,[],[f17053]) ).
fof(f44934,plain,
! [X2,X0,X1] :
( ~ genls(X1,X2)
| ~ genls(X0,X1)
| genls(X0,X2) ),
inference(cnf_transformation,[],[f44244]) ).
fof(f44983,plain,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
inference(cnf_transformation,[],[f520]) ).
fof(f44990,plain,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
inference(cnf_transformation,[],[f1204]) ).
fof(f45065,plain,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
inference(cnf_transformation,[],[f189]) ).
fof(f45074,plain,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
inference(cnf_transformation,[],[f4037]) ).
fof(f45138,plain,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
inference(cnf_transformation,[],[f28270]) ).
fof(f45149,plain,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
inference(cnf_transformation,[],[f13065]) ).
fof(f45177,plain,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
inference(cnf_transformation,[],[f25099]) ).
fof(f45190,plain,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
inference(cnf_transformation,[],[f3362]) ).
fof(f45204,plain,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
inference(cnf_transformation,[],[f8720]) ).
fof(f45214,plain,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
inference(cnf_transformation,[],[f49]) ).
fof(f45224,plain,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
inference(cnf_transformation,[],[f17208]) ).
fof(f45234,plain,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
inference(cnf_transformation,[],[f3393]) ).
fof(f45246,plain,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
inference(cnf_transformation,[],[f3272]) ).
fof(f45255,plain,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
inference(cnf_transformation,[],[f5291]) ).
fof(f45264,plain,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
inference(cnf_transformation,[],[f3909]) ).
fof(f45274,plain,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
inference(cnf_transformation,[],[f1105]) ).
fof(f45286,plain,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
inference(cnf_transformation,[],[f4455]) ).
fof(f45296,plain,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
inference(cnf_transformation,[],[f4089]) ).
fof(f45307,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(cnf_transformation,[],[f9361]) ).
fof(f45318,plain,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
inference(cnf_transformation,[],[f13777]) ).
fof(f45332,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(cnf_transformation,[],[f20317]) ).
fof(f45350,plain,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
inference(cnf_transformation,[],[f7779]) ).
fof(f45369,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(cnf_transformation,[],[f10406]) ).
fof(f45406,plain,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
inference(cnf_transformation,[],[f4910]) ).
fof(f45429,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(cnf_transformation,[],[f806]) ).
fof(f45442,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[],[f13339]) ).
fof(f45464,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f2422]) ).
fof(f45478,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[],[f2922]) ).
fof(f45510,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f8232]) ).
fof(f46129,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1),
inference(resolution,[],[f44908,f45510]) ).
fof(f46135,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_1_65536)
| disjointwith(X0,c_tptpcol_1_1) ),
inference(resolution,[],[f46129,f44906]) ).
fof(f46140,plain,
! [X0] :
( genls(X0,c_tptpcol_10_26886)
| ~ genls(X0,c_tptpcol_11_26887) ),
inference(resolution,[],[f44934,f45214]) ).
fof(f46143,plain,
! [X0] :
( genls(X0,c_tptpcol_12_92262)
| ~ genls(X0,c_tptpcol_13_92263) ),
inference(resolution,[],[f44934,f45138]) ).
fof(f46144,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_15_92268)
| genls(X0,c_tptpcol_14_92264) ),
inference(resolution,[],[f44934,f44983]) ).
fof(f46147,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_3_81921)
| genls(X0,c_tptpcol_2_65537) ),
inference(resolution,[],[f44934,f45429]) ).
fof(f46149,plain,
! [X0] :
( genls(X0,c_tptpcol_14_26921)
| ~ genls(X0,c_tptpcol_15_26925) ),
inference(resolution,[],[f44934,f44990]) ).
fof(f46150,plain,
! [X0] :
( genls(X0,c_tptpcol_13_26920)
| ~ genls(X0,c_tptpcol_14_26921) ),
inference(resolution,[],[f44934,f45074]) ).
fof(f46156,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_2_2)
| genls(X0,c_tptpcol_1_1) ),
inference(resolution,[],[f44934,f45478]) ).
fof(f46161,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_7_92163)
| genls(X0,c_tptpcol_6_92162) ),
inference(resolution,[],[f44934,f45286]) ).
fof(f46162,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_13_26920)
| genls(X0,c_tptpcol_12_26919) ),
inference(resolution,[],[f44934,f45149]) ).
fof(f46165,plain,
! [X0] :
( genls(X0,c_tptpcol_5_90114)
| ~ genls(X0,c_tptpcol_6_92162) ),
inference(resolution,[],[f44934,f45307]) ).
fof(f46171,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_4_90113)
| genls(X0,c_tptpcol_3_81921) ),
inference(resolution,[],[f44934,f45369]) ).
fof(f46172,plain,
! [X0] :
( genls(X0,c_tptpcol_4_24578)
| ~ genls(X0,c_tptpcol_5_24579) ),
inference(resolution,[],[f44934,f45350]) ).
fof(f46173,plain,
! [X0] :
( genls(X0,c_tptpcol_10_92166)
| ~ genls(X0,c_tptpcol_11_92230) ),
inference(resolution,[],[f44934,f45204]) ).
fof(f46174,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_5_90114)
| genls(X0,c_tptpcol_4_90113) ),
inference(resolution,[],[f44934,f45332]) ).
fof(f46177,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_12_92262)
| genls(X0,c_tptpcol_11_92230) ),
inference(resolution,[],[f44934,f45177]) ).
fof(f46180,plain,
genls(c_tptpcol_16_92269,c_tptpcol_14_92264),
inference(resolution,[],[f46144,f44926]) ).
fof(f46185,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_10_92166)
| genls(X0,c_tptpcol_9_92165) ),
inference(resolution,[],[f45224,f44934]) ).
fof(f46187,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_12_26919)
| genls(X0,c_tptpcol_11_26887) ),
inference(resolution,[],[f45190,f44934]) ).
fof(f46196,plain,
! [X0] :
( genls(X0,c_tptpcol_7_26628)
| ~ genls(X0,c_tptpcol_8_26629) ),
inference(resolution,[],[f45274,f44934]) ).
fof(f46216,plain,
disjointwith(c_tptpcol_2_65537,c_tptpcol_1_1),
inference(resolution,[],[f46135,f45464]) ).
fof(f46223,plain,
genls(c_tptpcol_3_16386,c_tptpcol_1_1),
inference(resolution,[],[f46156,f45442]) ).
fof(f46230,plain,
genls(c_tptpcol_8_92164,c_tptpcol_6_92162),
inference(resolution,[],[f46161,f45264]) ).
fof(f46248,plain,
! [X0,X1] :
( ~ genls(X0,c_tptpcol_13_92263)
| ~ genls(X1,X0)
| genls(X1,c_tptpcol_12_92262) ),
inference(resolution,[],[f46143,f44934]) ).
fof(f46260,plain,
! [X0] :
( genls(X0,c_tptpcol_4_90113)
| ~ genls(X0,c_tptpcol_6_92162) ),
inference(resolution,[],[f46174,f46165]) ).
fof(f46262,plain,
! [X0] :
( genls(X0,c_tptpcol_3_81921)
| ~ genls(X0,c_tptpcol_6_92162) ),
inference(resolution,[],[f46260,f46171]) ).
fof(f46264,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_6_92162)
| genls(X0,c_tptpcol_2_65537) ),
inference(resolution,[],[f46262,f46147]) ).
fof(f46276,plain,
! [X0] :
( genls(X0,c_tptpcol_12_26919)
| ~ genls(X0,c_tptpcol_14_26921) ),
inference(resolution,[],[f46150,f46162]) ).
fof(f46360,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_11_92230)
| genls(X0,c_tptpcol_9_92165) ),
inference(resolution,[],[f46185,f46173]) ).
fof(f46381,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_14_26921)
| genls(X0,c_tptpcol_11_26887) ),
inference(resolution,[],[f46187,f46276]) ).
fof(f46484,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_2_65537)
| disjointwith(X0,c_tptpcol_1_1) ),
inference(resolution,[],[f46216,f44906]) ).
fof(f46557,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_15_26925)
| genls(X0,c_tptpcol_11_26887) ),
inference(resolution,[],[f46381,f46149]) ).
fof(f46559,plain,
genls(c_tptpcol_16_26926,c_tptpcol_11_26887),
inference(resolution,[],[f46557,f44930]) ).
fof(f47053,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_8_92164)
| genls(X0,c_tptpcol_6_92162) ),
inference(resolution,[],[f46230,f44934]) ).
fof(f47054,plain,
genls(c_tptpcol_9_92165,c_tptpcol_6_92162),
inference(resolution,[],[f47053,f45246]) ).
fof(f47058,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_9_92165)
| genls(X0,c_tptpcol_6_92162) ),
inference(resolution,[],[f47054,f44934]) ).
fof(f47413,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_14_92264)
| genls(X0,c_tptpcol_12_92262) ),
inference(resolution,[],[f46248,f45065]) ).
fof(f47418,plain,
genls(c_tptpcol_16_92269,c_tptpcol_12_92262),
inference(resolution,[],[f47413,f46180]) ).
fof(f47419,plain,
genls(c_tptpcol_16_92269,c_tptpcol_11_92230),
inference(resolution,[],[f47418,f46177]) ).
fof(f47424,plain,
genls(c_tptpcol_16_92269,c_tptpcol_9_92165),
inference(resolution,[],[f47419,f46360]) ).
fof(f47429,plain,
genls(c_tptpcol_16_92269,c_tptpcol_6_92162),
inference(resolution,[],[f47424,f47058]) ).
fof(f47435,plain,
genls(c_tptpcol_16_92269,c_tptpcol_2_65537),
inference(resolution,[],[f47429,f46264]) ).
fof(f47440,plain,
disjointwith(c_tptpcol_16_92269,c_tptpcol_1_1),
inference(resolution,[],[f47435,f46484]) ).
fof(f47476,plain,
! [X0] :
( disjointwith(c_tptpcol_16_92269,X0)
| ~ genls(X0,c_tptpcol_1_1) ),
inference(resolution,[],[f47440,f44907]) ).
fof(f47503,plain,
! [X0,X1] :
( ~ genls(X0,c_tptpcol_1_1)
| disjointwith(c_tptpcol_16_92269,X1)
| ~ genls(X1,X0) ),
inference(resolution,[],[f47476,f44907]) ).
fof(f47541,plain,
! [X0] :
( disjointwith(c_tptpcol_16_92269,X0)
| ~ genls(X0,c_tptpcol_3_16386) ),
inference(resolution,[],[f47503,f46223]) ).
fof(f47544,plain,
! [X0,X1] :
( ~ genls(X0,c_tptpcol_3_16386)
| disjointwith(c_tptpcol_16_92269,X1)
| ~ genls(X1,X0) ),
inference(resolution,[],[f47541,f44907]) ).
fof(f47646,plain,
! [X0] :
( disjointwith(c_tptpcol_16_92269,X0)
| ~ genls(X0,c_tptpcol_4_24578) ),
inference(resolution,[],[f47544,f45406]) ).
fof(f47652,plain,
! [X0,X1] :
( ~ genls(X0,c_tptpcol_4_24578)
| disjointwith(c_tptpcol_16_92269,X1)
| ~ genls(X1,X0) ),
inference(resolution,[],[f47646,f44907]) ).
fof(f47655,plain,
! [X0,X1] :
( ~ genls(X1,c_tptpcol_5_24579)
| ~ genls(X0,X1)
| disjointwith(c_tptpcol_16_92269,X0) ),
inference(resolution,[],[f47652,f46172]) ).
fof(f47658,plain,
! [X0] :
( disjointwith(c_tptpcol_16_92269,X0)
| ~ genls(X0,c_tptpcol_6_26627) ),
inference(resolution,[],[f47655,f45318]) ).
fof(f47660,plain,
! [X0,X1] :
( ~ genls(X0,c_tptpcol_6_26627)
| disjointwith(c_tptpcol_16_92269,X1)
| ~ genls(X1,X0) ),
inference(resolution,[],[f47658,f44907]) ).
fof(f47663,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_7_26628)
| disjointwith(c_tptpcol_16_92269,X0) ),
inference(resolution,[],[f47660,f45296]) ).
fof(f47665,plain,
! [X0] :
( disjointwith(c_tptpcol_16_92269,X0)
| ~ genls(X0,c_tptpcol_8_26629) ),
inference(resolution,[],[f47663,f46196]) ).
fof(f47668,plain,
! [X0,X1] :
( ~ genls(X0,c_tptpcol_8_26629)
| disjointwith(c_tptpcol_16_92269,X1)
| ~ genls(X1,X0) ),
inference(resolution,[],[f47665,f44907]) ).
fof(f47673,plain,
! [X0] :
( disjointwith(c_tptpcol_16_92269,X0)
| ~ genls(X0,c_tptpcol_9_26885) ),
inference(resolution,[],[f47668,f45255]) ).
fof(f47676,plain,
! [X0,X1] :
( ~ genls(X0,c_tptpcol_9_26885)
| disjointwith(c_tptpcol_16_92269,X1)
| ~ genls(X1,X0) ),
inference(resolution,[],[f47673,f44907]) ).
fof(f47679,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_10_26886)
| disjointwith(c_tptpcol_16_92269,X0) ),
inference(resolution,[],[f47676,f45234]) ).
fof(f47681,plain,
! [X0] :
( ~ genls(X0,c_tptpcol_11_26887)
| disjointwith(c_tptpcol_16_92269,X0) ),
inference(resolution,[],[f47679,f46140]) ).
fof(f47684,plain,
disjointwith(c_tptpcol_16_92269,c_tptpcol_16_26926),
inference(resolution,[],[f47681,f46559]) ).
fof(f47685,plain,
$false,
inference(unit_resulting_resolution,[],[f44908,f44903,f47684]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR049+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.18 % Computer : n005.cluster.edu
% 0.10/0.18 % Model : x86_64 x86_64
% 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.18 % Memory : 8046.5625MB
% 0.10/0.18 % OS : Linux 6.8.0-71-generic
% 0.10/0.18 % CPULimit : 300
% 0.10/0.18 % WCLimit : 300
% 0.10/0.18 % DateTime : Mon Sep 28 22:17:46 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.22 Running first-order theorem proving
% 0.10/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.56/2.79 % (1245411)Detected formulas, will run a generic FOF schedule.
% 8.56/2.79 % (1245694)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=1738106639:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2991 on theBenchmark for (2991ds/134677Mi)
% 8.56/2.79 % (1245693)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=1600774057:i=141193_2991 on theBenchmark for (2991ds/141193Mi)
% 8.56/2.79 % (1245697)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3046343647:i=119:av=off:ss=axioms_2991 on theBenchmark for (2991ds/119Mi)
% 8.56/2.79 % (1245698)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3128430918:s2a=on:i=139:gtg=position_2991 on theBenchmark for (2991ds/139Mi)
% 8.56/2.79 % (1245696)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1312504683:i=109:sd=1:ins=1:gsp=on:ss=axioms_2991 on theBenchmark for (2991ds/109Mi)
% 8.56/2.79 % (1245695)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=146280209:i=141695:sd=1:nm=32:gsp=on:ss=included_2991 on theBenchmark for (2991ds/141695Mi)
% 8.56/2.79 % (1245699)dis-21_1_sil=8000:lcm=predicate:random_seed=4293367065:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2991 on theBenchmark for (2991ds/129Mi)
% 8.56/2.79 % (1245698)Instruction limit reached!
% 8.56/2.79 % (1245698)------------------------------
% 8.56/2.79 % (1245698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.56/2.79 % (1245698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.56/2.79 % (1245698)CaDiCaL version: 2.1.3
% 8.56/2.79 % (1245698)Termination reason: Instruction limit
% 8.56/2.79 % (1245698)Termination phase: Property scanning
% 8.56/2.79 % (1245698)Time elapsed: 0.066 s
% 8.56/2.79 % (1245698)Peak memory usage: 110 MB
% 8.56/2.79 % (1245698)Instructions burned: 141 (million)
% 8.56/2.79 % (1245696)Instruction limit reached!
% 8.56/2.79 % (1245696)------------------------------
% 8.56/2.79 % (1245696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.56/2.79 % (1245696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.56/2.79 % (1245696)CaDiCaL version: 2.1.3
% 8.56/2.79 % (1245696)Termination reason: Instruction limit
% 8.56/2.79 % (1245696)Termination phase: Saturation
% 8.56/2.79 % (1245696)Time elapsed: 0.081 s
% 8.56/2.79 % (1245696)Peak memory usage: 116 MB
% 8.56/2.79 % (1245696)Instructions burned: 112 (million)
% 8.56/2.79 % (1245697)Instruction limit reached!
% 8.56/2.79 % (1245697)------------------------------
% 8.56/2.79 % (1245697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.56/2.79 % (1245697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.56/2.79 % (1245697)CaDiCaL version: 2.1.3
% 8.56/2.79 % (1245697)Termination reason: Instruction limit
% 8.56/2.79 % (1245697)Termination phase: Saturation
% 8.56/2.79 % (1245697)Time elapsed: 0.086 s
% 8.56/2.79 % (1245697)Peak memory usage: 116 MB
% 8.56/2.79 % (1245697)Instructions burned: 122 (million)
% 8.56/2.79 % (1245699)Instruction limit reached!
% 8.56/2.79 % (1245699)------------------------------
% 8.56/2.79 % (1245699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.56/2.79 % (1245699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.56/2.79 % (1245699)CaDiCaL version: 2.1.3
% 8.56/2.79 % (1245699)Termination reason: Instruction limit
% 8.56/2.79 % (1245699)Termination phase: SInE selection
% 8.56/2.79 % (1245699)Time elapsed: 0.078 s
% 8.56/2.79 % (1245699)Peak memory usage: 111 MB
% 8.56/2.79 % (1245699)Instructions burned: 130 (million)
% 8.56/2.79 % (1245707)lrs+10_1_sil=8000:sp=occurrence:random_seed=1167927339:i=285:sd=3:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/285Mi)
% 8.56/2.79 % (1245710)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=1242011044:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 8.56/2.79 % (1245709)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3489840463:i=325:sd=1:ss=axioms:sgt=32_2988 on theBenchmark for (2988ds/325Mi)
% 8.56/2.79 % (1245708)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1529847819:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/157Mi)
% 8.56/2.79 % (1245708)Instruction limit reached!
% 8.56/2.79 % (1245708)------------------------------
% 8.56/2.79 % (1245708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.56/2.79 % (1245708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.56/2.79 % (1245708)CaDiCaL version: 2.1.3
% 8.56/2.79 % (1245708)Termination reason: Instruction limit
% 8.56/2.79 % (1245708)Termination phase: Property scanning
% 8.56/2.79 % (1245708)Time elapsed: 0.071 s
% 8.56/2.79 % (1245708)Peak memory usage: 110 MB
% 8.56/2.79 % (1245708)Instructions burned: 158 (million)
% 8.56/2.79 % (1245707)Refutation not found, incomplete strategy
% 8.56/2.79 % (1245707)------------------------------
% 8.56/2.79 % (1245707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.56/2.79 % (1245707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.56/2.79 % (1245707)CaDiCaL version: 2.1.3
% 8.56/2.79 % (1245707)Termination reason: Refutation not found, incomplete strategy
% 8.56/2.79 % (1245707)Time elapsed: 0.099 s
% 8.56/2.79 % (1245707)Peak memory usage: 119 MB
% 8.56/2.79 % (1245707)Instructions burned: 127 (million)
% 8.56/2.79 % (1245709)Refutation not found, incomplete strategy
% 8.56/2.79 % (1245709)------------------------------
% 8.56/2.79 % (1245709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.56/2.79 % (1245709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.56/2.79 % (1245709)CaDiCaL version: 2.1.3
% 8.56/2.79 % (1245709)Termination reason: Refutation not found, incomplete strategy
% 8.56/2.79 % (1245709)Time elapsed: 0.088 s
% 8.56/2.79 % (1245709)Peak memory usage: 118 MB
% 8.56/2.79 % (1245709)Instructions burned: 112 (million)
% 8.56/2.79 % (1245710)Instruction limit reached!
% 8.56/2.79 % (1245710)------------------------------
% 8.56/2.79 % (1245710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.56/2.79 % (1245710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.56/2.79 % (1245710)CaDiCaL version: 2.1.3
% 8.56/2.79 % (1245710)Termination reason: Instruction limit
% 8.56/2.79 % (1245710)Termination phase: SInE selection
% 8.56/2.79 % (1245710)Time elapsed: 0.121 s
% 8.56/2.79 % (1245710)Peak memory usage: 111 MB
% 8.56/2.79 % (1245710)Instructions burned: 249 (million)
% 8.56/2.79 % (1245715)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2050777849:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2986 on theBenchmark for (2986ds/294Mi)
% 8.56/2.79 % (1245716)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=759161105:i=2350_2985 on theBenchmark for (2985ds/2350Mi)
% 8.56/2.79 % (1245707)------------------------------
% 8.56/2.79 % (1245707)------------------------------
% 8.56/2.79 % (1245709)------------------------------
% 8.56/2.79 % (1245709)------------------------------
% 8.56/2.79 % (1245715)Instruction limit reached!
% 8.56/2.79 % (1245715)------------------------------
% 8.56/2.79 % (1245715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.56/2.79 % (1245715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.56/2.79 % (1245715)CaDiCaL version: 2.1.3
% 8.56/2.79 % (1245715)Termination reason: Instruction limit
% 8.56/2.79 % (1245715)Termination phase: Saturation
% 8.56/2.79 % (1245715)Time elapsed: 0.180 s
% 8.56/2.79 % (1245715)Peak memory usage: 119 MB
% 8.56/2.79 % (1245715)Instructions burned: 296 (million)
% 8.56/2.79 % (1245719)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3525036982:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 8.56/2.79 % (1245720)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1784177294:i=127:av=off:fsr=off:sup=off_2983 on theBenchmark for (2983ds/127Mi)
% 8.56/2.79 % (1245721)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4100512249:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2982 on theBenchmark for (2982ds/114Mi)
% 8.56/2.79 % (1245719)Instruction limit reached!
% 8.56/2.79 % (1245719)------------------------------
% 8.56/2.79 % (1245719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.56/2.79 % (1245719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.56/2.79 % (1245719)CaDiCaL version: 2.1.3
% 8.56/2.79 % (1245719)Termination reason: Instruction limit
% 8.56/2.79 % (1245719)Termination phase: Saturation
% 8.56/2.79 % (1245719)Time elapsed: 0.091 s
% 8.56/2.79 % (1245719)Peak memory usage: 116 MB
% 8.56/2.79 % (1245719)Instructions burned: 114 (million)
% 8.56/2.79 % (1245694)First to succeed.
% 8.56/2.79 % (1245694)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1245411"
% 8.56/2.79 % (1245720)Instruction limit reached!
% 8.56/2.79 % (1245720)------------------------------
% 8.56/2.79 % (1245720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.56/2.79 % (1245720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.56/2.79 % (1245720)CaDiCaL version: 2.1.3
% 8.56/2.79 % (1245720)Termination reason: Instruction limit
% 8.56/2.79 % (1245720)Termination phase: Preprocessing 2
% 8.56/2.79 % (1245720)Time elapsed: 0.110 s
% 8.56/2.79 % (1245720)Peak memory usage: 117 MB
% 8.56/2.79 % (1245720)Instructions burned: 127 (million)
% 8.56/2.79 % (1245721)Instruction limit reached!
% 8.56/2.79 % (1245721)------------------------------
% 8.56/2.79 % (1245721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.56/2.79 % (1245721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.56/2.79 % (1245721)CaDiCaL version: 2.1.3
% 8.56/2.79 % (1245721)Termination reason: Instruction limit
% 8.56/2.79 % (1245721)Termination phase: Property scanning
% 8.56/2.79 % (1245721)Time elapsed: 0.057 s
% 8.56/2.79 % (1245721)Peak memory usage: 110 MB
% 8.56/2.79 % (1245721)Instructions burned: 116 (million)
% 8.56/2.79 % (1245725)lrs+10_1_sil=8000:sp=occurrence:random_seed=804840283:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2980 on theBenchmark for (2980ds/907Mi)
% 8.56/2.79 % (1245694)Refutation found. Thanks to Tanya!
% 8.56/2.79 % SZS status Theorem for theBenchmark
% 8.56/2.79 % SZS output start Proof for theBenchmark
% See solution above
% 10.12/3.00 % (1245694)------------------------------
% 10.12/3.00 % (1245694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.12/3.00 % (1245694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.12/3.00 % (1245694)CaDiCaL version: 2.1.3
% 10.12/3.00 % (1245694)Termination reason: Refutation
% 10.12/3.00 % (1245694)Time elapsed: 0.909 s
% 10.12/3.00 % (1245694)Peak memory usage: 223 MB
% 10.12/3.00 % (1245694)Instructions burned: 2314 (million)
% 10.12/3.00 % (1245694)------------------------------
% 10.12/3.00 % (1245694)------------------------------
% 10.12/3.00 % (1245411)Success in time 2.115 s
% 10.12/3.00 % Vampire exiting
%------------------------------------------------------------------------------