%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : CSR049+1 : TPTP v9.2.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:14:26 PM UTC 2026
% Result : Theorem 1.18s 1.61s
% Output : CNFRefutation 1.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 177
% Syntax : Number of formulae : 1025 ( 199 unt; 0 def)
% Number of atoms : 2041 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 2013 ( 997 ~; 863 |; 16 &)
% ( 0 <=>; 137 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 46 ( 45 usr; 1 prp; 0-2 aty)
% Number of functors : 40 ( 40 usr; 40 con; 0-0 aty)
% Number of variables : 1276 ( 22 sgn 366 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(query49,conjecture,
( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query49) ).
fof(just69,axiom,
! [X1,X2,X3] :
~ ( isa(X1,X2)
& isa(X1,X3)
& disjointwith(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just69) ).
fof(just75,axiom,
! [X10,X11,X12] :
( ( genlpreds(X10,X11)
& genlpreds(X11,X12) )
=> genlpreds(X10,X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just75) ).
fof(just70,axiom,
! [X4,X5,X6] :
( ( genlinverse(X4,X5)
& genlinverse(X5,X6) )
=> genlpreds(X4,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just70) ).
fof(just81,axiom,
! [X7,X13,X14] :
( ( genlinverse(X7,X13)
& genlpreds(X13,X14) )
=> genlinverse(X7,X14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just81) ).
fof(just80,axiom,
! [X13,X9,X14] :
( ( genlinverse(X13,X9)
& genlpreds(X14,X13) )
=> genlinverse(X14,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just80) ).
fof(just166,axiom,
! [X7,X13,X14] :
( ( isa(X7,X13)
& genls(X13,X14) )
=> isa(X7,X14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just166) ).
fof(just85,axiom,
! [X7,X13,X14] :
( ( disjointwith(X7,X13)
& genls(X14,X13) )
=> disjointwith(X7,X14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just85) ).
fof(just86,axiom,
! [X13,X9,X14] :
( ( disjointwith(X13,X9)
& genls(X14,X13) )
=> disjointwith(X14,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just86) ).
fof(just159,axiom,
! [X7,X13,X14] :
( ( genls(X7,X13)
& genls(X13,X14) )
=> genls(X7,X14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just159) ).
fof(just155,axiom,
! [X10,X11,X12] :
( ( genls(X10,X11)
& genls(X11,X12) )
=> genls(X10,X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just155) ).
fof(just158,axiom,
! [X13,X9,X14] :
( ( genls(X13,X9)
& genls(X14,X13) )
=> genls(X14,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just158) ).
fof(just173,axiom,
! [X10,X11,X12] :
( ( genlmt(X10,X11)
& genlmt(X11,X12) )
=> genlmt(X10,X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just173) ).
fof(just84,axiom,
! [X10,X11] :
( disjointwith(X10,X11)
=> disjointwith(X11,X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just84) ).
fof(just168,axiom,
! [X15,X16] :
( ( mtvisible(X15)
& genlmt(X15,X16) )
=> mtvisible(X16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just168) ).
fof(just172,axiom,
! [X8,X9] :
( genlmt(X8,X9)
=> microtheory(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just172) ).
fof(just171,axiom,
! [X8,X9] :
( genlmt(X8,X9)
=> microtheory(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just171) ).
fof(just170,axiom,
! [X7,X8] :
( genlmt(X7,X8)
=> microtheory(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just170) ).
fof(just169,axiom,
! [X7,X8] :
( genlmt(X7,X8)
=> microtheory(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just169) ).
fof(just165,axiom,
! [X8,X9] :
( isa(X8,X9)
=> thing(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just165) ).
fof(just164,axiom,
! [X8,X9] :
( isa(X8,X9)
=> thing(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just164) ).
fof(just83,axiom,
! [X8,X9] :
( disjointwith(X8,X9)
=> collection(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just83) ).
fof(just154,axiom,
! [X8,X9] :
( genls(X8,X9)
=> collection(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just154) ).
fof(just153,axiom,
! [X8,X9] :
( genls(X8,X9)
=> collection(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just153) ).
fof(just163,axiom,
! [X7,X8] :
( isa(X7,X8)
=> collection(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just163) ).
fof(just162,axiom,
! [X7,X8] :
( isa(X7,X8)
=> collection(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just162) ).
fof(just82,axiom,
! [X7,X8] :
( disjointwith(X7,X8)
=> collection(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just82) ).
fof(just152,axiom,
! [X7,X8] :
( genls(X7,X8)
=> collection(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just152) ).
fof(just151,axiom,
! [X7,X8] :
( genls(X7,X8)
=> collection(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just151) ).
fof(just79,axiom,
! [X8,X9] :
( genlinverse(X8,X9)
=> binarypredicate(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just79) ).
fof(just78,axiom,
! [X7,X8] :
( genlinverse(X7,X8)
=> binarypredicate(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just78) ).
fof(just74,axiom,
! [X8,X9] :
( genlpreds(X8,X9)
=> predicate(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just74) ).
fof(just73,axiom,
! [X8,X9] :
( genlpreds(X8,X9)
=> predicate(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just73) ).
fof(just72,axiom,
! [X7,X8] :
( genlpreds(X7,X8)
=> predicate(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just72) ).
fof(just71,axiom,
! [X7,X8] :
( genlpreds(X7,X8)
=> predicate(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just71) ).
fof(just87,axiom,
! [X10] :
( isa(X10,c_tptpcol_16_92269)
=> tptpcol_16_92269(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just87) ).
fof(just89,axiom,
! [X10] :
( isa(X10,c_tptpcol_15_92268)
=> tptpcol_15_92268(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just89) ).
fof(just91,axiom,
! [X10] :
( isa(X10,c_tptpcol_14_92264)
=> tptpcol_14_92264(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just91) ).
fof(just93,axiom,
! [X10] :
( isa(X10,c_tptpcol_13_92263)
=> tptpcol_13_92263(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just93) ).
fof(just95,axiom,
! [X10] :
( isa(X10,c_tptpcol_12_92262)
=> tptpcol_12_92262(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just95) ).
fof(just97,axiom,
! [X10] :
( isa(X10,c_tptpcol_11_92230)
=> tptpcol_11_92230(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just97) ).
fof(just99,axiom,
! [X10] :
( isa(X10,c_tptpcol_10_92166)
=> tptpcol_10_92166(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just99) ).
fof(just101,axiom,
! [X10] :
( isa(X10,c_tptpcol_9_92165)
=> tptpcol_9_92165(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just101) ).
fof(just103,axiom,
! [X10] :
( isa(X10,c_tptpcol_8_92164)
=> tptpcol_8_92164(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just103) ).
fof(just105,axiom,
! [X10] :
( isa(X10,c_tptpcol_7_92163)
=> tptpcol_7_92163(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just105) ).
fof(just107,axiom,
! [X10] :
( isa(X10,c_tptpcol_6_92162)
=> tptpcol_6_92162(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just107) ).
fof(just109,axiom,
! [X10] :
( isa(X10,c_tptpcol_5_90114)
=> tptpcol_5_90114(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just109) ).
fof(just111,axiom,
! [X10] :
( isa(X10,c_tptpcol_4_90113)
=> tptpcol_4_90113(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just111) ).
fof(just113,axiom,
! [X10] :
( isa(X10,c_tptpcol_3_81921)
=> tptpcol_3_81921(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just113) ).
fof(just115,axiom,
! [X10] :
( isa(X10,c_tptpcol_1_65536)
=> tptpcol_1_65536(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just115) ).
fof(just117,axiom,
! [X10] :
( isa(X10,c_tptpcol_2_65537)
=> tptpcol_2_65537(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just117) ).
fof(just119,axiom,
! [X10] :
( isa(X10,c_tptpcol_16_26926)
=> tptpcol_16_26926(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just119) ).
fof(just121,axiom,
! [X10] :
( isa(X10,c_tptpcol_15_26925)
=> tptpcol_15_26925(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just121) ).
fof(just123,axiom,
! [X10] :
( isa(X10,c_tptpcol_14_26921)
=> tptpcol_14_26921(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just123) ).
fof(just125,axiom,
! [X10] :
( isa(X10,c_tptpcol_13_26920)
=> tptpcol_13_26920(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just125) ).
fof(just127,axiom,
! [X10] :
( isa(X10,c_tptpcol_12_26919)
=> tptpcol_12_26919(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just127) ).
fof(just129,axiom,
! [X10] :
( isa(X10,c_tptpcol_11_26887)
=> tptpcol_11_26887(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just129) ).
fof(just131,axiom,
! [X10] :
( isa(X10,c_tptpcol_10_26886)
=> tptpcol_10_26886(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just131) ).
fof(just133,axiom,
! [X10] :
( isa(X10,c_tptpcol_9_26885)
=> tptpcol_9_26885(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just133) ).
fof(just135,axiom,
! [X10] :
( isa(X10,c_tptpcol_8_26629)
=> tptpcol_8_26629(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just135) ).
fof(just137,axiom,
! [X10] :
( isa(X10,c_tptpcol_7_26628)
=> tptpcol_7_26628(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just137) ).
fof(just139,axiom,
! [X10] :
( isa(X10,c_tptpcol_6_26627)
=> tptpcol_6_26627(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just139) ).
fof(just141,axiom,
! [X10] :
( isa(X10,c_tptpcol_5_24579)
=> tptpcol_5_24579(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just141) ).
fof(just143,axiom,
! [X10] :
( isa(X10,c_tptpcol_4_24578)
=> tptpcol_4_24578(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just143) ).
fof(just145,axiom,
! [X10] :
( isa(X10,c_tptpcol_3_16386)
=> tptpcol_3_16386(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just145) ).
fof(just147,axiom,
! [X10] :
( isa(X10,c_tptpcol_1_1)
=> tptpcol_1_1(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just147) ).
fof(just149,axiom,
! [X10] :
( isa(X10,c_tptpcol_2_2)
=> tptpcol_2_2(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just149) ).
fof(just160,axiom,
! [X10] :
( isa(X10,c_transitivebinarypredicate)
=> transitivebinarypredicate(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just160) ).
fof(just77,axiom,
! [X10] :
( predicate(X10)
=> genlpreds(X10,X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just77) ).
fof(just76,axiom,
! [X10] :
( predicate(X10)
=> genlpreds(X10,X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just76) ).
fof(just157,axiom,
! [X10] :
( collection(X10)
=> genls(X10,X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just157) ).
fof(just156,axiom,
! [X10] :
( collection(X10)
=> genls(X10,X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just156) ).
fof(just175,axiom,
! [X10] :
( microtheory(X10)
=> genlmt(X10,X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just175) ).
fof(just174,axiom,
! [X10] :
( microtheory(X10)
=> genlmt(X10,X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just174) ).
fof(just161,axiom,
! [X10] :
( transitivebinarypredicate(X10)
=> isa(X10,c_transitivebinarypredicate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just161) ).
fof(just88,axiom,
! [X10] :
( tptpcol_16_92269(X10)
=> isa(X10,c_tptpcol_16_92269) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just88) ).
fof(just90,axiom,
! [X10] :
( tptpcol_15_92268(X10)
=> isa(X10,c_tptpcol_15_92268) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just90) ).
fof(just92,axiom,
! [X10] :
( tptpcol_14_92264(X10)
=> isa(X10,c_tptpcol_14_92264) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just92) ).
fof(just94,axiom,
! [X10] :
( tptpcol_13_92263(X10)
=> isa(X10,c_tptpcol_13_92263) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just94) ).
fof(just96,axiom,
! [X10] :
( tptpcol_12_92262(X10)
=> isa(X10,c_tptpcol_12_92262) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just96) ).
fof(just98,axiom,
! [X10] :
( tptpcol_11_92230(X10)
=> isa(X10,c_tptpcol_11_92230) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just98) ).
fof(just100,axiom,
! [X10] :
( tptpcol_10_92166(X10)
=> isa(X10,c_tptpcol_10_92166) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just100) ).
fof(just102,axiom,
! [X10] :
( tptpcol_9_92165(X10)
=> isa(X10,c_tptpcol_9_92165) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just102) ).
fof(just104,axiom,
! [X10] :
( tptpcol_8_92164(X10)
=> isa(X10,c_tptpcol_8_92164) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just104) ).
fof(just106,axiom,
! [X10] :
( tptpcol_7_92163(X10)
=> isa(X10,c_tptpcol_7_92163) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just106) ).
fof(just108,axiom,
! [X10] :
( tptpcol_6_92162(X10)
=> isa(X10,c_tptpcol_6_92162) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just108) ).
fof(just110,axiom,
! [X10] :
( tptpcol_5_90114(X10)
=> isa(X10,c_tptpcol_5_90114) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just110) ).
fof(just112,axiom,
! [X10] :
( tptpcol_4_90113(X10)
=> isa(X10,c_tptpcol_4_90113) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just112) ).
fof(just114,axiom,
! [X10] :
( tptpcol_3_81921(X10)
=> isa(X10,c_tptpcol_3_81921) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just114) ).
fof(just116,axiom,
! [X10] :
( tptpcol_1_65536(X10)
=> isa(X10,c_tptpcol_1_65536) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just116) ).
fof(just118,axiom,
! [X10] :
( tptpcol_2_65537(X10)
=> isa(X10,c_tptpcol_2_65537) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just118) ).
fof(just120,axiom,
! [X10] :
( tptpcol_16_26926(X10)
=> isa(X10,c_tptpcol_16_26926) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just120) ).
fof(just122,axiom,
! [X10] :
( tptpcol_15_26925(X10)
=> isa(X10,c_tptpcol_15_26925) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just122) ).
fof(just124,axiom,
! [X10] :
( tptpcol_14_26921(X10)
=> isa(X10,c_tptpcol_14_26921) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just124) ).
fof(just126,axiom,
! [X10] :
( tptpcol_13_26920(X10)
=> isa(X10,c_tptpcol_13_26920) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just126) ).
fof(just128,axiom,
! [X10] :
( tptpcol_12_26919(X10)
=> isa(X10,c_tptpcol_12_26919) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just128) ).
fof(just130,axiom,
! [X10] :
( tptpcol_11_26887(X10)
=> isa(X10,c_tptpcol_11_26887) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just130) ).
fof(just132,axiom,
! [X10] :
( tptpcol_10_26886(X10)
=> isa(X10,c_tptpcol_10_26886) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just132) ).
fof(just134,axiom,
! [X10] :
( tptpcol_9_26885(X10)
=> isa(X10,c_tptpcol_9_26885) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just134) ).
fof(just136,axiom,
! [X10] :
( tptpcol_8_26629(X10)
=> isa(X10,c_tptpcol_8_26629) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just136) ).
fof(just138,axiom,
! [X10] :
( tptpcol_7_26628(X10)
=> isa(X10,c_tptpcol_7_26628) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just138) ).
fof(just140,axiom,
! [X10] :
( tptpcol_6_26627(X10)
=> isa(X10,c_tptpcol_6_26627) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just140) ).
fof(just142,axiom,
! [X10] :
( tptpcol_5_24579(X10)
=> isa(X10,c_tptpcol_5_24579) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just142) ).
fof(just144,axiom,
! [X10] :
( tptpcol_4_24578(X10)
=> isa(X10,c_tptpcol_4_24578) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just144) ).
fof(just146,axiom,
! [X10] :
( tptpcol_3_16386(X10)
=> isa(X10,c_tptpcol_3_16386) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just146) ).
fof(just148,axiom,
! [X10] :
( tptpcol_1_1(X10)
=> isa(X10,c_tptpcol_1_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just148) ).
fof(just150,axiom,
! [X10] :
( tptpcol_2_2(X10)
=> isa(X10,c_tptpcol_2_2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just150) ).
fof(just68,axiom,
! [X1] :
~ ( tptpcol_1_1(X1)
& tptpcol_1_65536(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just68) ).
fof(just66,axiom,
! [X1] :
( tptpcol_16_92269(X1)
=> tptpcol_15_92268(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just66) ).
fof(just64,axiom,
! [X1] :
( tptpcol_15_92268(X1)
=> tptpcol_14_92264(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just64) ).
fof(just62,axiom,
! [X1] :
( tptpcol_14_92264(X1)
=> tptpcol_13_92263(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just62) ).
fof(just60,axiom,
! [X1] :
( tptpcol_13_92263(X1)
=> tptpcol_12_92262(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just60) ).
fof(just58,axiom,
! [X1] :
( tptpcol_12_92262(X1)
=> tptpcol_11_92230(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just58) ).
fof(just56,axiom,
! [X1] :
( tptpcol_11_92230(X1)
=> tptpcol_10_92166(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just56) ).
fof(just54,axiom,
! [X1] :
( tptpcol_10_92166(X1)
=> tptpcol_9_92165(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just54) ).
fof(just52,axiom,
! [X1] :
( tptpcol_9_92165(X1)
=> tptpcol_8_92164(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just52) ).
fof(just50,axiom,
! [X1] :
( tptpcol_8_92164(X1)
=> tptpcol_7_92163(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just50) ).
fof(just48,axiom,
! [X1] :
( tptpcol_7_92163(X1)
=> tptpcol_6_92162(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just48) ).
fof(just46,axiom,
! [X1] :
( tptpcol_6_92162(X1)
=> tptpcol_5_90114(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just46) ).
fof(just44,axiom,
! [X1] :
( tptpcol_5_90114(X1)
=> tptpcol_4_90113(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just44) ).
fof(just42,axiom,
! [X1] :
( tptpcol_4_90113(X1)
=> tptpcol_3_81921(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just42) ).
fof(just38,axiom,
! [X1] :
( tptpcol_2_65537(X1)
=> tptpcol_1_65536(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just38) ).
fof(just40,axiom,
! [X1] :
( tptpcol_3_81921(X1)
=> tptpcol_2_65537(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just40) ).
fof(just36,axiom,
! [X1] :
( tptpcol_16_26926(X1)
=> tptpcol_15_26925(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just36) ).
fof(just34,axiom,
! [X1] :
( tptpcol_15_26925(X1)
=> tptpcol_14_26921(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just34) ).
fof(just32,axiom,
! [X1] :
( tptpcol_14_26921(X1)
=> tptpcol_13_26920(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just32) ).
fof(just30,axiom,
! [X1] :
( tptpcol_13_26920(X1)
=> tptpcol_12_26919(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just30) ).
fof(just28,axiom,
! [X1] :
( tptpcol_12_26919(X1)
=> tptpcol_11_26887(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just28) ).
fof(just26,axiom,
! [X1] :
( tptpcol_11_26887(X1)
=> tptpcol_10_26886(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just26) ).
fof(just24,axiom,
! [X1] :
( tptpcol_10_26886(X1)
=> tptpcol_9_26885(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just24) ).
fof(just22,axiom,
! [X1] :
( tptpcol_9_26885(X1)
=> tptpcol_8_26629(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just22) ).
fof(just20,axiom,
! [X1] :
( tptpcol_8_26629(X1)
=> tptpcol_7_26628(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just20) ).
fof(just18,axiom,
! [X1] :
( tptpcol_7_26628(X1)
=> tptpcol_6_26627(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just18) ).
fof(just16,axiom,
! [X1] :
( tptpcol_6_26627(X1)
=> tptpcol_5_24579(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just16) ).
fof(just14,axiom,
! [X1] :
( tptpcol_5_24579(X1)
=> tptpcol_4_24578(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just14) ).
fof(just12,axiom,
! [X1] :
( tptpcol_4_24578(X1)
=> tptpcol_3_16386(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just12) ).
fof(just8,axiom,
! [X1] :
( tptpcol_2_2(X1)
=> tptpcol_1_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just8) ).
fof(just10,axiom,
! [X1] :
( tptpcol_3_16386(X1)
=> tptpcol_2_2(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just10) ).
fof(just67,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just67) ).
fof(just65,axiom,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just65) ).
fof(just63,axiom,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just63) ).
fof(just61,axiom,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just61) ).
fof(just59,axiom,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just59) ).
fof(just57,axiom,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just57) ).
fof(just55,axiom,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just55) ).
fof(just53,axiom,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just53) ).
fof(just51,axiom,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just51) ).
fof(just49,axiom,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just49) ).
fof(just47,axiom,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just47) ).
fof(just45,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just45) ).
fof(just43,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just43) ).
fof(just41,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just41) ).
fof(just39,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just39) ).
fof(just37,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just37) ).
fof(just35,axiom,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just35) ).
fof(just33,axiom,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just33) ).
fof(just31,axiom,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just31) ).
fof(just29,axiom,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just29) ).
fof(just27,axiom,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just27) ).
fof(just25,axiom,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just25) ).
fof(just23,axiom,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just23) ).
fof(just21,axiom,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just21) ).
fof(just19,axiom,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just19) ).
fof(just17,axiom,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just17) ).
fof(just15,axiom,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just15) ).
fof(just13,axiom,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just13) ).
fof(just11,axiom,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just11) ).
fof(just9,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just9) ).
fof(just7,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just7) ).
fof(just3,axiom,
genlmt(c_unitedstatessociallifemt,c_gregoriancalendarmt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just3) ).
fof(just6,axiom,
genlmt(c_peopledatamt,c_unitedstatessociallifemt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just6) ).
fof(just2,axiom,
genlmt(c_unitedstatesgeographypeoplemt,c_peopledatamt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just2) ).
fof(just5,axiom,
genlmt(c_basekb,c_universalvocabularymt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just5) ).
fof(just1,axiom,
genlmt(c_gregoriancalendarmt,c_basekb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just1) ).
fof(just167,axiom,
mtvisible(c_universalvocabularymt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just167) ).
fof(just176,axiom,
mtvisible(c_basekb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just176) ).
fof(just4,axiom,
transitivebinarypredicate(c_genlmt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just4) ).
fof(i_0_177,negated_conjecture,
~ ( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
inference(assume_negation,[status(cth)],[query49]) ).
fof(i_0_178,plain,
! [X231,X232,X233] :
( ~ isa(X231,X232)
| ~ isa(X231,X233)
| ~ disjointwith(X232,X233) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just69])]) ).
fof(i_0_179,plain,
! [X245,X246,X247] :
( ~ genlpreds(X245,X246)
| ~ genlpreds(X246,X247)
| genlpreds(X245,X247) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just75])]) ).
fof(i_0_180,plain,
! [X234,X235,X236] :
( ~ genlinverse(X234,X235)
| ~ genlinverse(X235,X236)
| genlpreds(X234,X236) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just70])]) ).
fof(i_0_181,plain,
! [X257,X258,X259] :
( ~ genlinverse(X257,X258)
| ~ genlpreds(X258,X259)
| genlinverse(X257,X259) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just81])]) ).
fof(i_0_182,plain,
! [X254,X255,X256] :
( ~ genlinverse(X254,X255)
| ~ genlpreds(X256,X254)
| genlinverse(X256,X255) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just80])]) ).
fof(i_0_183,plain,
! [X365,X366,X367] :
( ~ isa(X365,X366)
| ~ genls(X366,X367)
| isa(X365,X367) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just166])]) ).
fof(i_0_184,plain,
! [X266,X267,X268] :
( ~ disjointwith(X266,X267)
| ~ genls(X268,X267)
| disjointwith(X266,X268) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just85])]) ).
fof(i_0_185,plain,
! [X269,X270,X271] :
( ~ disjointwith(X269,X270)
| ~ genls(X271,X269)
| disjointwith(X271,X270) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just86])]) ).
fof(i_0_186,plain,
! [X352,X353,X354] :
( ~ genls(X352,X353)
| ~ genls(X353,X354)
| genls(X352,X354) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just159])]) ).
fof(i_0_187,plain,
! [X344,X345,X346] :
( ~ genls(X344,X345)
| ~ genls(X345,X346)
| genls(X344,X346) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just155])]) ).
fof(i_0_188,plain,
! [X349,X350,X351] :
( ~ genls(X349,X350)
| ~ genls(X351,X349)
| genls(X351,X350) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just158])]) ).
fof(i_0_189,plain,
! [X378,X379,X380] :
( ~ genlmt(X378,X379)
| ~ genlmt(X379,X380)
| genlmt(X378,X380) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just173])]) ).
fof(i_0_190,plain,
! [X264,X265] :
( ~ disjointwith(X264,X265)
| disjointwith(X265,X264) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just84])]) ).
fof(i_0_191,plain,
! [X368,X369] :
( ~ mtvisible(X368)
| ~ genlmt(X368,X369)
| mtvisible(X369) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just168])]) ).
fof(i_0_192,plain,
! [X376,X377] :
( ~ genlmt(X376,X377)
| microtheory(X376) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just172])]) ).
fof(i_0_193,plain,
! [X374,X375] :
( ~ genlmt(X374,X375)
| microtheory(X374) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just171])]) ).
fof(i_0_194,plain,
! [X372,X373] :
( ~ genlmt(X372,X373)
| microtheory(X373) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just170])]) ).
fof(i_0_195,plain,
! [X370,X371] :
( ~ genlmt(X370,X371)
| microtheory(X371) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just169])]) ).
fof(i_0_196,plain,
! [X363,X364] :
( ~ isa(X363,X364)
| thing(X363) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just165])]) ).
fof(i_0_197,plain,
! [X361,X362] :
( ~ isa(X361,X362)
| thing(X361) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just164])]) ).
fof(i_0_198,plain,
! [X262,X263] :
( ~ disjointwith(X262,X263)
| collection(X262) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just83])]) ).
fof(i_0_199,plain,
! [X342,X343] :
( ~ genls(X342,X343)
| collection(X342) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just154])]) ).
fof(i_0_200,plain,
! [X340,X341] :
( ~ genls(X340,X341)
| collection(X340) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just153])]) ).
fof(i_0_201,plain,
! [X359,X360] :
( ~ isa(X359,X360)
| collection(X360) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just163])]) ).
fof(i_0_202,plain,
! [X357,X358] :
( ~ isa(X357,X358)
| collection(X358) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just162])]) ).
fof(i_0_203,plain,
! [X260,X261] :
( ~ disjointwith(X260,X261)
| collection(X261) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just82])]) ).
fof(i_0_204,plain,
! [X338,X339] :
( ~ genls(X338,X339)
| collection(X339) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just152])]) ).
fof(i_0_205,plain,
! [X336,X337] :
( ~ genls(X336,X337)
| collection(X337) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just151])]) ).
fof(i_0_206,plain,
! [X252,X253] :
( ~ genlinverse(X252,X253)
| binarypredicate(X252) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just79])]) ).
fof(i_0_207,plain,
! [X250,X251] :
( ~ genlinverse(X250,X251)
| binarypredicate(X251) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just78])]) ).
fof(i_0_208,plain,
! [X243,X244] :
( ~ genlpreds(X243,X244)
| predicate(X243) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just74])]) ).
fof(i_0_209,plain,
! [X241,X242] :
( ~ genlpreds(X241,X242)
| predicate(X241) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just73])]) ).
fof(i_0_210,plain,
! [X239,X240] :
( ~ genlpreds(X239,X240)
| predicate(X240) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just72])]) ).
fof(i_0_211,plain,
! [X237,X238] :
( ~ genlpreds(X237,X238)
| predicate(X238) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just71])]) ).
fof(i_0_212,plain,
! [X272] :
( ~ isa(X272,c_tptpcol_16_92269)
| tptpcol_16_92269(X272) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just87])]) ).
fof(i_0_213,plain,
! [X274] :
( ~ isa(X274,c_tptpcol_15_92268)
| tptpcol_15_92268(X274) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just89])]) ).
fof(i_0_214,plain,
! [X276] :
( ~ isa(X276,c_tptpcol_14_92264)
| tptpcol_14_92264(X276) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just91])]) ).
fof(i_0_215,plain,
! [X278] :
( ~ isa(X278,c_tptpcol_13_92263)
| tptpcol_13_92263(X278) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just93])]) ).
fof(i_0_216,plain,
! [X280] :
( ~ isa(X280,c_tptpcol_12_92262)
| tptpcol_12_92262(X280) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just95])]) ).
fof(i_0_217,plain,
! [X282] :
( ~ isa(X282,c_tptpcol_11_92230)
| tptpcol_11_92230(X282) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just97])]) ).
fof(i_0_218,plain,
! [X284] :
( ~ isa(X284,c_tptpcol_10_92166)
| tptpcol_10_92166(X284) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just99])]) ).
fof(i_0_219,plain,
! [X286] :
( ~ isa(X286,c_tptpcol_9_92165)
| tptpcol_9_92165(X286) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just101])]) ).
fof(i_0_220,plain,
! [X288] :
( ~ isa(X288,c_tptpcol_8_92164)
| tptpcol_8_92164(X288) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just103])]) ).
fof(i_0_221,plain,
! [X290] :
( ~ isa(X290,c_tptpcol_7_92163)
| tptpcol_7_92163(X290) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just105])]) ).
fof(i_0_222,plain,
! [X292] :
( ~ isa(X292,c_tptpcol_6_92162)
| tptpcol_6_92162(X292) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just107])]) ).
fof(i_0_223,plain,
! [X294] :
( ~ isa(X294,c_tptpcol_5_90114)
| tptpcol_5_90114(X294) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just109])]) ).
fof(i_0_224,plain,
! [X296] :
( ~ isa(X296,c_tptpcol_4_90113)
| tptpcol_4_90113(X296) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just111])]) ).
fof(i_0_225,plain,
! [X298] :
( ~ isa(X298,c_tptpcol_3_81921)
| tptpcol_3_81921(X298) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just113])]) ).
fof(i_0_226,plain,
! [X300] :
( ~ isa(X300,c_tptpcol_1_65536)
| tptpcol_1_65536(X300) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just115])]) ).
fof(i_0_227,plain,
! [X302] :
( ~ isa(X302,c_tptpcol_2_65537)
| tptpcol_2_65537(X302) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just117])]) ).
fof(i_0_228,plain,
! [X304] :
( ~ isa(X304,c_tptpcol_16_26926)
| tptpcol_16_26926(X304) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just119])]) ).
fof(i_0_229,plain,
! [X306] :
( ~ isa(X306,c_tptpcol_15_26925)
| tptpcol_15_26925(X306) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just121])]) ).
fof(i_0_230,plain,
! [X308] :
( ~ isa(X308,c_tptpcol_14_26921)
| tptpcol_14_26921(X308) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just123])]) ).
fof(i_0_231,plain,
! [X310] :
( ~ isa(X310,c_tptpcol_13_26920)
| tptpcol_13_26920(X310) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just125])]) ).
fof(i_0_232,plain,
! [X312] :
( ~ isa(X312,c_tptpcol_12_26919)
| tptpcol_12_26919(X312) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just127])]) ).
fof(i_0_233,plain,
! [X314] :
( ~ isa(X314,c_tptpcol_11_26887)
| tptpcol_11_26887(X314) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just129])]) ).
fof(i_0_234,plain,
! [X316] :
( ~ isa(X316,c_tptpcol_10_26886)
| tptpcol_10_26886(X316) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just131])]) ).
fof(i_0_235,plain,
! [X318] :
( ~ isa(X318,c_tptpcol_9_26885)
| tptpcol_9_26885(X318) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just133])]) ).
fof(i_0_236,plain,
! [X320] :
( ~ isa(X320,c_tptpcol_8_26629)
| tptpcol_8_26629(X320) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just135])]) ).
fof(i_0_237,plain,
! [X322] :
( ~ isa(X322,c_tptpcol_7_26628)
| tptpcol_7_26628(X322) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just137])]) ).
fof(i_0_238,plain,
! [X324] :
( ~ isa(X324,c_tptpcol_6_26627)
| tptpcol_6_26627(X324) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just139])]) ).
fof(i_0_239,plain,
! [X326] :
( ~ isa(X326,c_tptpcol_5_24579)
| tptpcol_5_24579(X326) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just141])]) ).
fof(i_0_240,plain,
! [X328] :
( ~ isa(X328,c_tptpcol_4_24578)
| tptpcol_4_24578(X328) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just143])]) ).
fof(i_0_241,plain,
! [X330] :
( ~ isa(X330,c_tptpcol_3_16386)
| tptpcol_3_16386(X330) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just145])]) ).
fof(i_0_242,plain,
! [X332] :
( ~ isa(X332,c_tptpcol_1_1)
| tptpcol_1_1(X332) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just147])]) ).
fof(i_0_243,plain,
! [X334] :
( ~ isa(X334,c_tptpcol_2_2)
| tptpcol_2_2(X334) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just149])]) ).
fof(i_0_244,plain,
! [X355] :
( ~ isa(X355,c_transitivebinarypredicate)
| transitivebinarypredicate(X355) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just160])]) ).
fof(i_0_245,plain,
! [X249] :
( ~ predicate(X249)
| genlpreds(X249,X249) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just77])]) ).
fof(i_0_246,plain,
! [X248] :
( ~ predicate(X248)
| genlpreds(X248,X248) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just76])]) ).
fof(i_0_247,plain,
! [X348] :
( ~ collection(X348)
| genls(X348,X348) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just157])]) ).
fof(i_0_248,plain,
! [X347] :
( ~ collection(X347)
| genls(X347,X347) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just156])]) ).
fof(i_0_249,plain,
! [X382] :
( ~ microtheory(X382)
| genlmt(X382,X382) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just175])]) ).
fof(i_0_250,plain,
! [X381] :
( ~ microtheory(X381)
| genlmt(X381,X381) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just174])]) ).
fof(i_0_251,plain,
! [X356] :
( ~ transitivebinarypredicate(X356)
| isa(X356,c_transitivebinarypredicate) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just161])]) ).
fof(i_0_252,plain,
! [X273] :
( ~ tptpcol_16_92269(X273)
| isa(X273,c_tptpcol_16_92269) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just88])]) ).
fof(i_0_253,plain,
! [X275] :
( ~ tptpcol_15_92268(X275)
| isa(X275,c_tptpcol_15_92268) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just90])]) ).
fof(i_0_254,plain,
! [X277] :
( ~ tptpcol_14_92264(X277)
| isa(X277,c_tptpcol_14_92264) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just92])]) ).
fof(i_0_255,plain,
! [X279] :
( ~ tptpcol_13_92263(X279)
| isa(X279,c_tptpcol_13_92263) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just94])]) ).
fof(i_0_256,plain,
! [X281] :
( ~ tptpcol_12_92262(X281)
| isa(X281,c_tptpcol_12_92262) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just96])]) ).
fof(i_0_257,plain,
! [X283] :
( ~ tptpcol_11_92230(X283)
| isa(X283,c_tptpcol_11_92230) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just98])]) ).
fof(i_0_258,plain,
! [X285] :
( ~ tptpcol_10_92166(X285)
| isa(X285,c_tptpcol_10_92166) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just100])]) ).
fof(i_0_259,plain,
! [X287] :
( ~ tptpcol_9_92165(X287)
| isa(X287,c_tptpcol_9_92165) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just102])]) ).
fof(i_0_260,plain,
! [X289] :
( ~ tptpcol_8_92164(X289)
| isa(X289,c_tptpcol_8_92164) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just104])]) ).
fof(i_0_261,plain,
! [X291] :
( ~ tptpcol_7_92163(X291)
| isa(X291,c_tptpcol_7_92163) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just106])]) ).
fof(i_0_262,plain,
! [X293] :
( ~ tptpcol_6_92162(X293)
| isa(X293,c_tptpcol_6_92162) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just108])]) ).
fof(i_0_263,plain,
! [X295] :
( ~ tptpcol_5_90114(X295)
| isa(X295,c_tptpcol_5_90114) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just110])]) ).
fof(i_0_264,plain,
! [X297] :
( ~ tptpcol_4_90113(X297)
| isa(X297,c_tptpcol_4_90113) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just112])]) ).
fof(i_0_265,plain,
! [X299] :
( ~ tptpcol_3_81921(X299)
| isa(X299,c_tptpcol_3_81921) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just114])]) ).
fof(i_0_266,plain,
! [X301] :
( ~ tptpcol_1_65536(X301)
| isa(X301,c_tptpcol_1_65536) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just116])]) ).
fof(i_0_267,plain,
! [X303] :
( ~ tptpcol_2_65537(X303)
| isa(X303,c_tptpcol_2_65537) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just118])]) ).
fof(i_0_268,plain,
! [X305] :
( ~ tptpcol_16_26926(X305)
| isa(X305,c_tptpcol_16_26926) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just120])]) ).
fof(i_0_269,plain,
! [X307] :
( ~ tptpcol_15_26925(X307)
| isa(X307,c_tptpcol_15_26925) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just122])]) ).
fof(i_0_270,plain,
! [X309] :
( ~ tptpcol_14_26921(X309)
| isa(X309,c_tptpcol_14_26921) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just124])]) ).
fof(i_0_271,plain,
! [X311] :
( ~ tptpcol_13_26920(X311)
| isa(X311,c_tptpcol_13_26920) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just126])]) ).
fof(i_0_272,plain,
! [X313] :
( ~ tptpcol_12_26919(X313)
| isa(X313,c_tptpcol_12_26919) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just128])]) ).
fof(i_0_273,plain,
! [X315] :
( ~ tptpcol_11_26887(X315)
| isa(X315,c_tptpcol_11_26887) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just130])]) ).
fof(i_0_274,plain,
! [X317] :
( ~ tptpcol_10_26886(X317)
| isa(X317,c_tptpcol_10_26886) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just132])]) ).
fof(i_0_275,plain,
! [X319] :
( ~ tptpcol_9_26885(X319)
| isa(X319,c_tptpcol_9_26885) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just134])]) ).
fof(i_0_276,plain,
! [X321] :
( ~ tptpcol_8_26629(X321)
| isa(X321,c_tptpcol_8_26629) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just136])]) ).
fof(i_0_277,plain,
! [X323] :
( ~ tptpcol_7_26628(X323)
| isa(X323,c_tptpcol_7_26628) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just138])]) ).
fof(i_0_278,plain,
! [X325] :
( ~ tptpcol_6_26627(X325)
| isa(X325,c_tptpcol_6_26627) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just140])]) ).
fof(i_0_279,plain,
! [X327] :
( ~ tptpcol_5_24579(X327)
| isa(X327,c_tptpcol_5_24579) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just142])]) ).
fof(i_0_280,plain,
! [X329] :
( ~ tptpcol_4_24578(X329)
| isa(X329,c_tptpcol_4_24578) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just144])]) ).
fof(i_0_281,plain,
! [X331] :
( ~ tptpcol_3_16386(X331)
| isa(X331,c_tptpcol_3_16386) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just146])]) ).
fof(i_0_282,plain,
! [X333] :
( ~ tptpcol_1_1(X333)
| isa(X333,c_tptpcol_1_1) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just148])]) ).
fof(i_0_283,plain,
! [X335] :
( ~ tptpcol_2_2(X335)
| isa(X335,c_tptpcol_2_2) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just150])]) ).
fof(i_0_284,negated_conjecture,
( mtvisible(c_unitedstatesgeographypeoplemt)
& ~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
inference(fof_nnf,[status(thm)],[i_0_177]) ).
fof(i_0_285,plain,
! [X230] :
( ~ tptpcol_1_1(X230)
| ~ tptpcol_1_65536(X230) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just68])]) ).
fof(i_0_286,plain,
! [X229] :
( ~ tptpcol_16_92269(X229)
| tptpcol_15_92268(X229) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just66])]) ).
fof(i_0_287,plain,
! [X228] :
( ~ tptpcol_15_92268(X228)
| tptpcol_14_92264(X228) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just64])]) ).
fof(i_0_288,plain,
! [X227] :
( ~ tptpcol_14_92264(X227)
| tptpcol_13_92263(X227) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just62])]) ).
fof(i_0_289,plain,
! [X226] :
( ~ tptpcol_13_92263(X226)
| tptpcol_12_92262(X226) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just60])]) ).
fof(i_0_290,plain,
! [X225] :
( ~ tptpcol_12_92262(X225)
| tptpcol_11_92230(X225) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just58])]) ).
fof(i_0_291,plain,
! [X224] :
( ~ tptpcol_11_92230(X224)
| tptpcol_10_92166(X224) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just56])]) ).
fof(i_0_292,plain,
! [X223] :
( ~ tptpcol_10_92166(X223)
| tptpcol_9_92165(X223) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just54])]) ).
fof(i_0_293,plain,
! [X222] :
( ~ tptpcol_9_92165(X222)
| tptpcol_8_92164(X222) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just52])]) ).
fof(i_0_294,plain,
! [X221] :
( ~ tptpcol_8_92164(X221)
| tptpcol_7_92163(X221) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just50])]) ).
fof(i_0_295,plain,
! [X220] :
( ~ tptpcol_7_92163(X220)
| tptpcol_6_92162(X220) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just48])]) ).
fof(i_0_296,plain,
! [X219] :
( ~ tptpcol_6_92162(X219)
| tptpcol_5_90114(X219) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just46])]) ).
fof(i_0_297,plain,
! [X218] :
( ~ tptpcol_5_90114(X218)
| tptpcol_4_90113(X218) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just44])]) ).
fof(i_0_298,plain,
! [X217] :
( ~ tptpcol_4_90113(X217)
| tptpcol_3_81921(X217) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just42])]) ).
fof(i_0_299,plain,
! [X215] :
( ~ tptpcol_2_65537(X215)
| tptpcol_1_65536(X215) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just38])]) ).
fof(i_0_300,plain,
! [X216] :
( ~ tptpcol_3_81921(X216)
| tptpcol_2_65537(X216) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just40])]) ).
fof(i_0_301,plain,
! [X214] :
( ~ tptpcol_16_26926(X214)
| tptpcol_15_26925(X214) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just36])]) ).
fof(i_0_302,plain,
! [X213] :
( ~ tptpcol_15_26925(X213)
| tptpcol_14_26921(X213) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just34])]) ).
fof(i_0_303,plain,
! [X212] :
( ~ tptpcol_14_26921(X212)
| tptpcol_13_26920(X212) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just32])]) ).
fof(i_0_304,plain,
! [X211] :
( ~ tptpcol_13_26920(X211)
| tptpcol_12_26919(X211) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just30])]) ).
fof(i_0_305,plain,
! [X210] :
( ~ tptpcol_12_26919(X210)
| tptpcol_11_26887(X210) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just28])]) ).
fof(i_0_306,plain,
! [X209] :
( ~ tptpcol_11_26887(X209)
| tptpcol_10_26886(X209) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just26])]) ).
fof(i_0_307,plain,
! [X208] :
( ~ tptpcol_10_26886(X208)
| tptpcol_9_26885(X208) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just24])]) ).
fof(i_0_308,plain,
! [X207] :
( ~ tptpcol_9_26885(X207)
| tptpcol_8_26629(X207) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just22])]) ).
fof(i_0_309,plain,
! [X206] :
( ~ tptpcol_8_26629(X206)
| tptpcol_7_26628(X206) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just20])]) ).
fof(i_0_310,plain,
! [X205] :
( ~ tptpcol_7_26628(X205)
| tptpcol_6_26627(X205) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just18])]) ).
fof(i_0_311,plain,
! [X204] :
( ~ tptpcol_6_26627(X204)
| tptpcol_5_24579(X204) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just16])]) ).
fof(i_0_312,plain,
! [X203] :
( ~ tptpcol_5_24579(X203)
| tptpcol_4_24578(X203) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just14])]) ).
fof(i_0_313,plain,
! [X202] :
( ~ tptpcol_4_24578(X202)
| tptpcol_3_16386(X202) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just12])]) ).
fof(i_0_314,plain,
! [X200] :
( ~ tptpcol_2_2(X200)
| tptpcol_1_1(X200) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just8])]) ).
fof(i_0_315,plain,
! [X201] :
( ~ tptpcol_3_16386(X201)
| tptpcol_2_2(X201) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just10])]) ).
cnf(i_0_316,plain,
( ~ isa(X1,X2)
| ~ isa(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_178]),
[final] ).
cnf(i_0_317,plain,
( genlpreds(X1,X3)
| ~ genlpreds(X1,X2)
| ~ genlpreds(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_179]),
[final] ).
cnf(i_0_318,plain,
( genlpreds(X1,X3)
| ~ genlinverse(X1,X2)
| ~ genlinverse(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_180]),
[final] ).
cnf(i_0_319,plain,
( genlinverse(X1,X3)
| ~ genlinverse(X1,X2)
| ~ genlpreds(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_181]),
[final] ).
cnf(i_0_320,plain,
( genlinverse(X3,X2)
| ~ genlinverse(X1,X2)
| ~ genlpreds(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_182]),
[final] ).
cnf(i_0_321,plain,
( isa(X1,X3)
| ~ isa(X1,X2)
| ~ genls(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_183]),
[final] ).
cnf(i_0_322,plain,
( disjointwith(X1,X3)
| ~ disjointwith(X1,X2)
| ~ genls(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_184]),
[final] ).
cnf(i_0_323,plain,
( disjointwith(X3,X2)
| ~ disjointwith(X1,X2)
| ~ genls(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_185]),
[final] ).
cnf(i_0_324,plain,
( genls(X1,X3)
| ~ genls(X1,X2)
| ~ genls(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_186]),
[final] ).
cnf(i_0_325,plain,
( genls(X1,X3)
| ~ genls(X1,X2)
| ~ genls(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_187]),
[final] ).
cnf(i_0_326,plain,
( genls(X3,X2)
| ~ genls(X1,X2)
| ~ genls(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_188]),
[final] ).
cnf(i_0_327,plain,
( genlmt(X1,X3)
| ~ genlmt(X1,X2)
| ~ genlmt(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_189]),
[final] ).
cnf(i_0_328,plain,
( disjointwith(X2,X1)
| ~ disjointwith(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_190]),
[final] ).
cnf(i_0_329,plain,
( mtvisible(X2)
| ~ mtvisible(X1)
| ~ genlmt(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_191]),
[final] ).
cnf(i_0_330,plain,
( microtheory(X1)
| ~ genlmt(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_192]),
[final] ).
cnf(i_0_331,plain,
( microtheory(X1)
| ~ genlmt(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_193]),
[final] ).
cnf(i_0_332,plain,
( microtheory(X2)
| ~ genlmt(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_194]),
[final] ).
cnf(i_0_333,plain,
( microtheory(X2)
| ~ genlmt(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_195]),
[final] ).
cnf(i_0_334,plain,
( thing(X1)
| ~ isa(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_196]),
[final] ).
cnf(i_0_335,plain,
( thing(X1)
| ~ isa(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_197]),
[final] ).
cnf(i_0_336,plain,
( collection(X1)
| ~ disjointwith(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_198]),
[final] ).
cnf(i_0_337,plain,
( collection(X1)
| ~ genls(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_199]),
[final] ).
cnf(i_0_338,plain,
( collection(X1)
| ~ genls(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_200]),
[final] ).
cnf(i_0_339,plain,
( collection(X2)
| ~ isa(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_201]),
[final] ).
cnf(i_0_340,plain,
( collection(X2)
| ~ isa(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_202]),
[final] ).
cnf(i_0_341,plain,
( collection(X2)
| ~ disjointwith(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_203]),
[final] ).
cnf(i_0_342,plain,
( collection(X2)
| ~ genls(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_204]),
[final] ).
cnf(i_0_343,plain,
( collection(X2)
| ~ genls(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_205]),
[final] ).
cnf(i_0_344,plain,
( binarypredicate(X1)
| ~ genlinverse(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_206]),
[final] ).
cnf(i_0_345,plain,
( binarypredicate(X2)
| ~ genlinverse(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_207]),
[final] ).
cnf(i_0_346,plain,
( predicate(X1)
| ~ genlpreds(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_208]),
[final] ).
cnf(i_0_347,plain,
( predicate(X1)
| ~ genlpreds(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_209]),
[final] ).
cnf(i_0_348,plain,
( predicate(X2)
| ~ genlpreds(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_210]),
[final] ).
cnf(i_0_349,plain,
( predicate(X2)
| ~ genlpreds(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_211]),
[final] ).
cnf(i_0_350,plain,
( tptpcol_16_92269(X1)
| ~ isa(X1,c_tptpcol_16_92269) ),
inference(split_conjunct,[status(thm)],[i_0_212]),
[final] ).
cnf(i_0_351,plain,
( tptpcol_15_92268(X1)
| ~ isa(X1,c_tptpcol_15_92268) ),
inference(split_conjunct,[status(thm)],[i_0_213]),
[final] ).
cnf(i_0_352,plain,
( tptpcol_14_92264(X1)
| ~ isa(X1,c_tptpcol_14_92264) ),
inference(split_conjunct,[status(thm)],[i_0_214]),
[final] ).
cnf(i_0_353,plain,
( tptpcol_13_92263(X1)
| ~ isa(X1,c_tptpcol_13_92263) ),
inference(split_conjunct,[status(thm)],[i_0_215]),
[final] ).
cnf(i_0_354,plain,
( tptpcol_12_92262(X1)
| ~ isa(X1,c_tptpcol_12_92262) ),
inference(split_conjunct,[status(thm)],[i_0_216]),
[final] ).
cnf(i_0_355,plain,
( tptpcol_11_92230(X1)
| ~ isa(X1,c_tptpcol_11_92230) ),
inference(split_conjunct,[status(thm)],[i_0_217]),
[final] ).
cnf(i_0_356,plain,
( tptpcol_10_92166(X1)
| ~ isa(X1,c_tptpcol_10_92166) ),
inference(split_conjunct,[status(thm)],[i_0_218]),
[final] ).
cnf(i_0_357,plain,
( tptpcol_9_92165(X1)
| ~ isa(X1,c_tptpcol_9_92165) ),
inference(split_conjunct,[status(thm)],[i_0_219]),
[final] ).
cnf(i_0_358,plain,
( tptpcol_8_92164(X1)
| ~ isa(X1,c_tptpcol_8_92164) ),
inference(split_conjunct,[status(thm)],[i_0_220]),
[final] ).
cnf(i_0_359,plain,
( tptpcol_7_92163(X1)
| ~ isa(X1,c_tptpcol_7_92163) ),
inference(split_conjunct,[status(thm)],[i_0_221]),
[final] ).
cnf(i_0_360,plain,
( tptpcol_6_92162(X1)
| ~ isa(X1,c_tptpcol_6_92162) ),
inference(split_conjunct,[status(thm)],[i_0_222]),
[final] ).
cnf(i_0_361,plain,
( tptpcol_5_90114(X1)
| ~ isa(X1,c_tptpcol_5_90114) ),
inference(split_conjunct,[status(thm)],[i_0_223]),
[final] ).
cnf(i_0_362,plain,
( tptpcol_4_90113(X1)
| ~ isa(X1,c_tptpcol_4_90113) ),
inference(split_conjunct,[status(thm)],[i_0_224]),
[final] ).
cnf(i_0_363,plain,
( tptpcol_3_81921(X1)
| ~ isa(X1,c_tptpcol_3_81921) ),
inference(split_conjunct,[status(thm)],[i_0_225]),
[final] ).
cnf(i_0_364,plain,
( tptpcol_1_65536(X1)
| ~ isa(X1,c_tptpcol_1_65536) ),
inference(split_conjunct,[status(thm)],[i_0_226]),
[final] ).
cnf(i_0_365,plain,
( tptpcol_2_65537(X1)
| ~ isa(X1,c_tptpcol_2_65537) ),
inference(split_conjunct,[status(thm)],[i_0_227]),
[final] ).
cnf(i_0_366,plain,
( tptpcol_16_26926(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(split_conjunct,[status(thm)],[i_0_228]),
[final] ).
cnf(i_0_367,plain,
( tptpcol_15_26925(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(split_conjunct,[status(thm)],[i_0_229]),
[final] ).
cnf(i_0_368,plain,
( tptpcol_14_26921(X1)
| ~ isa(X1,c_tptpcol_14_26921) ),
inference(split_conjunct,[status(thm)],[i_0_230]),
[final] ).
cnf(i_0_369,plain,
( tptpcol_13_26920(X1)
| ~ isa(X1,c_tptpcol_13_26920) ),
inference(split_conjunct,[status(thm)],[i_0_231]),
[final] ).
cnf(i_0_370,plain,
( tptpcol_12_26919(X1)
| ~ isa(X1,c_tptpcol_12_26919) ),
inference(split_conjunct,[status(thm)],[i_0_232]),
[final] ).
cnf(i_0_371,plain,
( tptpcol_11_26887(X1)
| ~ isa(X1,c_tptpcol_11_26887) ),
inference(split_conjunct,[status(thm)],[i_0_233]),
[final] ).
cnf(i_0_372,plain,
( tptpcol_10_26886(X1)
| ~ isa(X1,c_tptpcol_10_26886) ),
inference(split_conjunct,[status(thm)],[i_0_234]),
[final] ).
cnf(i_0_373,plain,
( tptpcol_9_26885(X1)
| ~ isa(X1,c_tptpcol_9_26885) ),
inference(split_conjunct,[status(thm)],[i_0_235]),
[final] ).
cnf(i_0_374,plain,
( tptpcol_8_26629(X1)
| ~ isa(X1,c_tptpcol_8_26629) ),
inference(split_conjunct,[status(thm)],[i_0_236]),
[final] ).
cnf(i_0_375,plain,
( tptpcol_7_26628(X1)
| ~ isa(X1,c_tptpcol_7_26628) ),
inference(split_conjunct,[status(thm)],[i_0_237]),
[final] ).
cnf(i_0_376,plain,
( tptpcol_6_26627(X1)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(split_conjunct,[status(thm)],[i_0_238]),
[final] ).
cnf(i_0_377,plain,
( tptpcol_5_24579(X1)
| ~ isa(X1,c_tptpcol_5_24579) ),
inference(split_conjunct,[status(thm)],[i_0_239]),
[final] ).
cnf(i_0_378,plain,
( tptpcol_4_24578(X1)
| ~ isa(X1,c_tptpcol_4_24578) ),
inference(split_conjunct,[status(thm)],[i_0_240]),
[final] ).
cnf(i_0_379,plain,
( tptpcol_3_16386(X1)
| ~ isa(X1,c_tptpcol_3_16386) ),
inference(split_conjunct,[status(thm)],[i_0_241]),
[final] ).
cnf(i_0_380,plain,
( tptpcol_1_1(X1)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(split_conjunct,[status(thm)],[i_0_242]),
[final] ).
cnf(i_0_381,plain,
( tptpcol_2_2(X1)
| ~ isa(X1,c_tptpcol_2_2) ),
inference(split_conjunct,[status(thm)],[i_0_243]),
[final] ).
cnf(i_0_382,plain,
( transitivebinarypredicate(X1)
| ~ isa(X1,c_transitivebinarypredicate) ),
inference(split_conjunct,[status(thm)],[i_0_244]),
[final] ).
cnf(i_0_383,plain,
( genlpreds(X1,X1)
| ~ predicate(X1) ),
inference(split_conjunct,[status(thm)],[i_0_245]),
[final] ).
cnf(i_0_384,plain,
( genlpreds(X1,X1)
| ~ predicate(X1) ),
inference(split_conjunct,[status(thm)],[i_0_246]),
[final] ).
cnf(i_0_385,plain,
( genls(X1,X1)
| ~ collection(X1) ),
inference(split_conjunct,[status(thm)],[i_0_247]),
[final] ).
cnf(i_0_386,plain,
( genls(X1,X1)
| ~ collection(X1) ),
inference(split_conjunct,[status(thm)],[i_0_248]),
[final] ).
cnf(i_0_387,plain,
( genlmt(X1,X1)
| ~ microtheory(X1) ),
inference(split_conjunct,[status(thm)],[i_0_249]),
[final] ).
cnf(i_0_388,plain,
( genlmt(X1,X1)
| ~ microtheory(X1) ),
inference(split_conjunct,[status(thm)],[i_0_250]),
[final] ).
cnf(i_0_389,plain,
( isa(X1,c_transitivebinarypredicate)
| ~ transitivebinarypredicate(X1) ),
inference(split_conjunct,[status(thm)],[i_0_251]),
[final] ).
cnf(i_0_390,plain,
( isa(X1,c_tptpcol_16_92269)
| ~ tptpcol_16_92269(X1) ),
inference(split_conjunct,[status(thm)],[i_0_252]),
[final] ).
cnf(i_0_391,plain,
( isa(X1,c_tptpcol_15_92268)
| ~ tptpcol_15_92268(X1) ),
inference(split_conjunct,[status(thm)],[i_0_253]),
[final] ).
cnf(i_0_392,plain,
( isa(X1,c_tptpcol_14_92264)
| ~ tptpcol_14_92264(X1) ),
inference(split_conjunct,[status(thm)],[i_0_254]),
[final] ).
cnf(i_0_393,plain,
( isa(X1,c_tptpcol_13_92263)
| ~ tptpcol_13_92263(X1) ),
inference(split_conjunct,[status(thm)],[i_0_255]),
[final] ).
cnf(i_0_394,plain,
( isa(X1,c_tptpcol_12_92262)
| ~ tptpcol_12_92262(X1) ),
inference(split_conjunct,[status(thm)],[i_0_256]),
[final] ).
cnf(i_0_395,plain,
( isa(X1,c_tptpcol_11_92230)
| ~ tptpcol_11_92230(X1) ),
inference(split_conjunct,[status(thm)],[i_0_257]),
[final] ).
cnf(i_0_396,plain,
( isa(X1,c_tptpcol_10_92166)
| ~ tptpcol_10_92166(X1) ),
inference(split_conjunct,[status(thm)],[i_0_258]),
[final] ).
cnf(i_0_397,plain,
( isa(X1,c_tptpcol_9_92165)
| ~ tptpcol_9_92165(X1) ),
inference(split_conjunct,[status(thm)],[i_0_259]),
[final] ).
cnf(i_0_398,plain,
( isa(X1,c_tptpcol_8_92164)
| ~ tptpcol_8_92164(X1) ),
inference(split_conjunct,[status(thm)],[i_0_260]),
[final] ).
cnf(i_0_399,plain,
( isa(X1,c_tptpcol_7_92163)
| ~ tptpcol_7_92163(X1) ),
inference(split_conjunct,[status(thm)],[i_0_261]),
[final] ).
cnf(i_0_400,plain,
( isa(X1,c_tptpcol_6_92162)
| ~ tptpcol_6_92162(X1) ),
inference(split_conjunct,[status(thm)],[i_0_262]),
[final] ).
cnf(i_0_401,plain,
( isa(X1,c_tptpcol_5_90114)
| ~ tptpcol_5_90114(X1) ),
inference(split_conjunct,[status(thm)],[i_0_263]),
[final] ).
cnf(i_0_402,plain,
( isa(X1,c_tptpcol_4_90113)
| ~ tptpcol_4_90113(X1) ),
inference(split_conjunct,[status(thm)],[i_0_264]),
[final] ).
cnf(i_0_403,plain,
( isa(X1,c_tptpcol_3_81921)
| ~ tptpcol_3_81921(X1) ),
inference(split_conjunct,[status(thm)],[i_0_265]),
[final] ).
cnf(i_0_404,plain,
( isa(X1,c_tptpcol_1_65536)
| ~ tptpcol_1_65536(X1) ),
inference(split_conjunct,[status(thm)],[i_0_266]),
[final] ).
cnf(i_0_405,plain,
( isa(X1,c_tptpcol_2_65537)
| ~ tptpcol_2_65537(X1) ),
inference(split_conjunct,[status(thm)],[i_0_267]),
[final] ).
cnf(i_0_406,plain,
( isa(X1,c_tptpcol_16_26926)
| ~ tptpcol_16_26926(X1) ),
inference(split_conjunct,[status(thm)],[i_0_268]),
[final] ).
cnf(i_0_407,plain,
( isa(X1,c_tptpcol_15_26925)
| ~ tptpcol_15_26925(X1) ),
inference(split_conjunct,[status(thm)],[i_0_269]),
[final] ).
cnf(i_0_408,plain,
( isa(X1,c_tptpcol_14_26921)
| ~ tptpcol_14_26921(X1) ),
inference(split_conjunct,[status(thm)],[i_0_270]),
[final] ).
cnf(i_0_409,plain,
( isa(X1,c_tptpcol_13_26920)
| ~ tptpcol_13_26920(X1) ),
inference(split_conjunct,[status(thm)],[i_0_271]),
[final] ).
cnf(i_0_410,plain,
( isa(X1,c_tptpcol_12_26919)
| ~ tptpcol_12_26919(X1) ),
inference(split_conjunct,[status(thm)],[i_0_272]),
[final] ).
cnf(i_0_411,plain,
( isa(X1,c_tptpcol_11_26887)
| ~ tptpcol_11_26887(X1) ),
inference(split_conjunct,[status(thm)],[i_0_273]),
[final] ).
cnf(i_0_412,plain,
( isa(X1,c_tptpcol_10_26886)
| ~ tptpcol_10_26886(X1) ),
inference(split_conjunct,[status(thm)],[i_0_274]),
[final] ).
cnf(i_0_413,plain,
( isa(X1,c_tptpcol_9_26885)
| ~ tptpcol_9_26885(X1) ),
inference(split_conjunct,[status(thm)],[i_0_275]),
[final] ).
cnf(i_0_414,plain,
( isa(X1,c_tptpcol_8_26629)
| ~ tptpcol_8_26629(X1) ),
inference(split_conjunct,[status(thm)],[i_0_276]),
[final] ).
cnf(i_0_415,plain,
( isa(X1,c_tptpcol_7_26628)
| ~ tptpcol_7_26628(X1) ),
inference(split_conjunct,[status(thm)],[i_0_277]),
[final] ).
cnf(i_0_416,plain,
( isa(X1,c_tptpcol_6_26627)
| ~ tptpcol_6_26627(X1) ),
inference(split_conjunct,[status(thm)],[i_0_278]),
[final] ).
cnf(i_0_417,plain,
( isa(X1,c_tptpcol_5_24579)
| ~ tptpcol_5_24579(X1) ),
inference(split_conjunct,[status(thm)],[i_0_279]),
[final] ).
cnf(i_0_418,plain,
( isa(X1,c_tptpcol_4_24578)
| ~ tptpcol_4_24578(X1) ),
inference(split_conjunct,[status(thm)],[i_0_280]),
[final] ).
cnf(i_0_419,plain,
( isa(X1,c_tptpcol_3_16386)
| ~ tptpcol_3_16386(X1) ),
inference(split_conjunct,[status(thm)],[i_0_281]),
[final] ).
cnf(i_0_420,plain,
( isa(X1,c_tptpcol_1_1)
| ~ tptpcol_1_1(X1) ),
inference(split_conjunct,[status(thm)],[i_0_282]),
[final] ).
cnf(i_0_421,plain,
( isa(X1,c_tptpcol_2_2)
| ~ tptpcol_2_2(X1) ),
inference(split_conjunct,[status(thm)],[i_0_283]),
[final] ).
cnf(i_0_422,negated_conjecture,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),
inference(split_conjunct,[status(thm)],[i_0_284]),
[final] ).
cnf(i_0_423,plain,
( ~ tptpcol_1_1(X1)
| ~ tptpcol_1_65536(X1) ),
inference(split_conjunct,[status(thm)],[i_0_285]),
[final] ).
cnf(i_0_424,plain,
( tptpcol_15_92268(X1)
| ~ tptpcol_16_92269(X1) ),
inference(split_conjunct,[status(thm)],[i_0_286]),
[final] ).
cnf(i_0_425,plain,
( tptpcol_14_92264(X1)
| ~ tptpcol_15_92268(X1) ),
inference(split_conjunct,[status(thm)],[i_0_287]),
[final] ).
cnf(i_0_426,plain,
( tptpcol_13_92263(X1)
| ~ tptpcol_14_92264(X1) ),
inference(split_conjunct,[status(thm)],[i_0_288]),
[final] ).
cnf(i_0_427,plain,
( tptpcol_12_92262(X1)
| ~ tptpcol_13_92263(X1) ),
inference(split_conjunct,[status(thm)],[i_0_289]),
[final] ).
cnf(i_0_428,plain,
( tptpcol_11_92230(X1)
| ~ tptpcol_12_92262(X1) ),
inference(split_conjunct,[status(thm)],[i_0_290]),
[final] ).
cnf(i_0_429,plain,
( tptpcol_10_92166(X1)
| ~ tptpcol_11_92230(X1) ),
inference(split_conjunct,[status(thm)],[i_0_291]),
[final] ).
cnf(i_0_430,plain,
( tptpcol_9_92165(X1)
| ~ tptpcol_10_92166(X1) ),
inference(split_conjunct,[status(thm)],[i_0_292]),
[final] ).
cnf(i_0_431,plain,
( tptpcol_8_92164(X1)
| ~ tptpcol_9_92165(X1) ),
inference(split_conjunct,[status(thm)],[i_0_293]),
[final] ).
cnf(i_0_432,plain,
( tptpcol_7_92163(X1)
| ~ tptpcol_8_92164(X1) ),
inference(split_conjunct,[status(thm)],[i_0_294]),
[final] ).
cnf(i_0_433,plain,
( tptpcol_6_92162(X1)
| ~ tptpcol_7_92163(X1) ),
inference(split_conjunct,[status(thm)],[i_0_295]),
[final] ).
cnf(i_0_434,plain,
( tptpcol_5_90114(X1)
| ~ tptpcol_6_92162(X1) ),
inference(split_conjunct,[status(thm)],[i_0_296]),
[final] ).
cnf(i_0_435,plain,
( tptpcol_4_90113(X1)
| ~ tptpcol_5_90114(X1) ),
inference(split_conjunct,[status(thm)],[i_0_297]),
[final] ).
cnf(i_0_436,plain,
( tptpcol_3_81921(X1)
| ~ tptpcol_4_90113(X1) ),
inference(split_conjunct,[status(thm)],[i_0_298]),
[final] ).
cnf(i_0_437,plain,
( tptpcol_1_65536(X1)
| ~ tptpcol_2_65537(X1) ),
inference(split_conjunct,[status(thm)],[i_0_299]),
[final] ).
cnf(i_0_438,plain,
( tptpcol_2_65537(X1)
| ~ tptpcol_3_81921(X1) ),
inference(split_conjunct,[status(thm)],[i_0_300]),
[final] ).
cnf(i_0_439,plain,
( tptpcol_15_26925(X1)
| ~ tptpcol_16_26926(X1) ),
inference(split_conjunct,[status(thm)],[i_0_301]),
[final] ).
cnf(i_0_440,plain,
( tptpcol_14_26921(X1)
| ~ tptpcol_15_26925(X1) ),
inference(split_conjunct,[status(thm)],[i_0_302]),
[final] ).
cnf(i_0_441,plain,
( tptpcol_13_26920(X1)
| ~ tptpcol_14_26921(X1) ),
inference(split_conjunct,[status(thm)],[i_0_303]),
[final] ).
cnf(i_0_442,plain,
( tptpcol_12_26919(X1)
| ~ tptpcol_13_26920(X1) ),
inference(split_conjunct,[status(thm)],[i_0_304]),
[final] ).
cnf(i_0_443,plain,
( tptpcol_11_26887(X1)
| ~ tptpcol_12_26919(X1) ),
inference(split_conjunct,[status(thm)],[i_0_305]),
[final] ).
cnf(i_0_444,plain,
( tptpcol_10_26886(X1)
| ~ tptpcol_11_26887(X1) ),
inference(split_conjunct,[status(thm)],[i_0_306]),
[final] ).
cnf(i_0_445,plain,
( tptpcol_9_26885(X1)
| ~ tptpcol_10_26886(X1) ),
inference(split_conjunct,[status(thm)],[i_0_307]),
[final] ).
cnf(i_0_446,plain,
( tptpcol_8_26629(X1)
| ~ tptpcol_9_26885(X1) ),
inference(split_conjunct,[status(thm)],[i_0_308]),
[final] ).
cnf(i_0_447,plain,
( tptpcol_7_26628(X1)
| ~ tptpcol_8_26629(X1) ),
inference(split_conjunct,[status(thm)],[i_0_309]),
[final] ).
cnf(i_0_448,plain,
( tptpcol_6_26627(X1)
| ~ tptpcol_7_26628(X1) ),
inference(split_conjunct,[status(thm)],[i_0_310]),
[final] ).
cnf(i_0_449,plain,
( tptpcol_5_24579(X1)
| ~ tptpcol_6_26627(X1) ),
inference(split_conjunct,[status(thm)],[i_0_311]),
[final] ).
cnf(i_0_450,plain,
( tptpcol_4_24578(X1)
| ~ tptpcol_5_24579(X1) ),
inference(split_conjunct,[status(thm)],[i_0_312]),
[final] ).
cnf(i_0_451,plain,
( tptpcol_3_16386(X1)
| ~ tptpcol_4_24578(X1) ),
inference(split_conjunct,[status(thm)],[i_0_313]),
[final] ).
cnf(i_0_452,plain,
( tptpcol_1_1(X1)
| ~ tptpcol_2_2(X1) ),
inference(split_conjunct,[status(thm)],[i_0_314]),
[final] ).
cnf(i_0_453,plain,
( tptpcol_2_2(X1)
| ~ tptpcol_3_16386(X1) ),
inference(split_conjunct,[status(thm)],[i_0_315]),
[final] ).
cnf(i_0_454,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(split_conjunct,[status(thm)],[just67]),
[final] ).
cnf(i_0_455,plain,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
inference(split_conjunct,[status(thm)],[just65]),
[final] ).
cnf(i_0_456,plain,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
inference(split_conjunct,[status(thm)],[just63]),
[final] ).
cnf(i_0_457,plain,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
inference(split_conjunct,[status(thm)],[just61]),
[final] ).
cnf(i_0_458,plain,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
inference(split_conjunct,[status(thm)],[just59]),
[final] ).
cnf(i_0_459,plain,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
inference(split_conjunct,[status(thm)],[just57]),
[final] ).
cnf(i_0_460,plain,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
inference(split_conjunct,[status(thm)],[just55]),
[final] ).
cnf(i_0_461,plain,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
inference(split_conjunct,[status(thm)],[just53]),
[final] ).
cnf(i_0_462,plain,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
inference(split_conjunct,[status(thm)],[just51]),
[final] ).
cnf(i_0_463,plain,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
inference(split_conjunct,[status(thm)],[just49]),
[final] ).
cnf(i_0_464,plain,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
inference(split_conjunct,[status(thm)],[just47]),
[final] ).
cnf(i_0_465,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(split_conjunct,[status(thm)],[just45]),
[final] ).
cnf(i_0_466,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(split_conjunct,[status(thm)],[just43]),
[final] ).
cnf(i_0_467,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(split_conjunct,[status(thm)],[just41]),
[final] ).
cnf(i_0_468,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(split_conjunct,[status(thm)],[just39]),
[final] ).
cnf(i_0_469,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(split_conjunct,[status(thm)],[just37]),
[final] ).
cnf(i_0_470,plain,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
inference(split_conjunct,[status(thm)],[just35]),
[final] ).
cnf(i_0_471,plain,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
inference(split_conjunct,[status(thm)],[just33]),
[final] ).
cnf(i_0_472,plain,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
inference(split_conjunct,[status(thm)],[just31]),
[final] ).
cnf(i_0_473,plain,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
inference(split_conjunct,[status(thm)],[just29]),
[final] ).
cnf(i_0_474,plain,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
inference(split_conjunct,[status(thm)],[just27]),
[final] ).
cnf(i_0_475,plain,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
inference(split_conjunct,[status(thm)],[just25]),
[final] ).
cnf(i_0_476,plain,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
inference(split_conjunct,[status(thm)],[just23]),
[final] ).
cnf(i_0_477,plain,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
inference(split_conjunct,[status(thm)],[just21]),
[final] ).
cnf(i_0_478,plain,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
inference(split_conjunct,[status(thm)],[just19]),
[final] ).
cnf(i_0_479,plain,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
inference(split_conjunct,[status(thm)],[just17]),
[final] ).
cnf(i_0_480,plain,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
inference(split_conjunct,[status(thm)],[just15]),
[final] ).
cnf(i_0_481,plain,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
inference(split_conjunct,[status(thm)],[just13]),
[final] ).
cnf(i_0_482,plain,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
inference(split_conjunct,[status(thm)],[just11]),
[final] ).
cnf(i_0_483,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(split_conjunct,[status(thm)],[just9]),
[final] ).
cnf(i_0_484,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(split_conjunct,[status(thm)],[just7]),
[final] ).
cnf(i_0_485,plain,
genlmt(c_unitedstatessociallifemt,c_gregoriancalendarmt),
inference(split_conjunct,[status(thm)],[just3]),
[final] ).
cnf(i_0_486,plain,
genlmt(c_peopledatamt,c_unitedstatessociallifemt),
inference(split_conjunct,[status(thm)],[just6]),
[final] ).
cnf(i_0_487,plain,
genlmt(c_unitedstatesgeographypeoplemt,c_peopledatamt),
inference(split_conjunct,[status(thm)],[just2]),
[final] ).
cnf(i_0_488,plain,
genlmt(c_basekb,c_universalvocabularymt),
inference(split_conjunct,[status(thm)],[just5]),
[final] ).
cnf(i_0_489,plain,
genlmt(c_gregoriancalendarmt,c_basekb),
inference(split_conjunct,[status(thm)],[just1]),
[final] ).
cnf(i_0_490,plain,
mtvisible(c_universalvocabularymt),
inference(split_conjunct,[status(thm)],[just167]),
[final] ).
cnf(i_0_491,negated_conjecture,
mtvisible(c_unitedstatesgeographypeoplemt),
inference(split_conjunct,[status(thm)],[i_0_284]),
[final] ).
cnf(i_0_492,plain,
mtvisible(c_basekb),
inference(split_conjunct,[status(thm)],[just176]),
[final] ).
cnf(i_0_493,plain,
transitivebinarypredicate(c_genlmt),
inference(split_conjunct,[status(thm)],[just4]),
[final] ).
cnf(i_0_494,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_454,i_0_328]) ).
cnf(i_0_495,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_496,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_15_92268),
inference(scs_inference,[],[i_0_422,i_0_454,i_0_455,i_0_328,i_0_322]) ).
cnf(i_0_497,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_498,plain,
disjointwith(c_tptpcol_2_65537,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_422,i_0_454,i_0_455,i_0_469,i_0_328,i_0_322,i_0_323]) ).
cnf(i_0_499,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_500,plain,
mtvisible(c_peopledatamt),
inference(scs_inference,[],[i_0_422,i_0_491,i_0_454,i_0_455,i_0_469,i_0_487,i_0_328,i_0_322,i_0_323,i_0_329]) ).
cnf(i_0_501,plain,
( ~ genlmt(X1,X2)
| mtvisible(X2)
| ~ mtvisible(X1) ),
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_502,plain,
genls(c_tptpcol_16_92269,c_tptpcol_14_92264),
inference(scs_inference,[],[i_0_422,i_0_491,i_0_454,i_0_455,i_0_456,i_0_469,i_0_487,i_0_328,i_0_322,i_0_323,i_0_329,i_0_326]) ).
cnf(i_0_503,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_504,plain,
genlmt(c_peopledatamt,c_gregoriancalendarmt),
inference(scs_inference,[],[i_0_422,i_0_491,i_0_454,i_0_455,i_0_456,i_0_469,i_0_485,i_0_486,i_0_487,i_0_328,i_0_322,i_0_323,i_0_329,i_0_326,i_0_327]) ).
cnf(i_0_505,plain,
( ~ genlmt(X1,X2)
| genlmt(X3,X2)
| ~ genlmt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_506,plain,
( ~ isa(X1,c_tptpcol_1_1)
| ~ isa(X1,c_tptpcol_1_65536) ),
inference(scs_inference,[],[i_0_422,i_0_491,i_0_454,i_0_455,i_0_456,i_0_469,i_0_485,i_0_486,i_0_487,i_0_328,i_0_322,i_0_323,i_0_329,i_0_326,i_0_327,i_0_316]) ).
cnf(i_0_507,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_508,plain,
( ~ isa(X1,c_tptpcol_2_2)
| ~ isa(X1,c_tptpcol_1_65536) ),
inference(scs_inference,[],[i_0_422,i_0_491,i_0_454,i_0_455,i_0_456,i_0_469,i_0_484,i_0_485,i_0_486,i_0_487,i_0_328,i_0_322,i_0_323,i_0_329,i_0_326,i_0_327,i_0_316,i_0_321]) ).
cnf(i_0_509,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_510,plain,
( ~ tptpcol_1_1(X1)
| ~ isa(X1,c_tptpcol_1_65536) ),
inference(scs_inference,[],[i_0_422,i_0_491,i_0_454,i_0_455,i_0_456,i_0_469,i_0_484,i_0_485,i_0_486,i_0_487,i_0_328,i_0_322,i_0_323,i_0_329,i_0_326,i_0_327,i_0_316,i_0_321,i_0_420]) ).
cnf(i_0_511,plain,
( isa(X1,c_tptpcol_1_1)
| ~ tptpcol_1_1(X1) ),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_512,plain,
( ~ tptpcol_2_2(X1)
| ~ isa(X1,c_tptpcol_1_65536) ),
inference(scs_inference,[],[i_0_422,i_0_491,i_0_454,i_0_455,i_0_456,i_0_469,i_0_484,i_0_485,i_0_486,i_0_487,i_0_328,i_0_322,i_0_323,i_0_329,i_0_326,i_0_327,i_0_316,i_0_321,i_0_420,i_0_421]) ).
cnf(i_0_513,plain,
( isa(X1,c_tptpcol_2_2)
| ~ tptpcol_2_2(X1) ),
inference(rename_variables,[],[i_0_421]) ).
cnf(i_0_514,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_2_65537),
inference(scs_inference,[],[i_0_498,i_0_328]) ).
cnf(i_0_515,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_516,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_3_81921),
inference(scs_inference,[],[i_0_498,i_0_468,i_0_328,i_0_322]) ).
cnf(i_0_517,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_518,plain,
disjointwith(c_tptpcol_3_81921,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_498,i_0_468,i_0_328,i_0_322,i_0_323]) ).
cnf(i_0_519,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_520,plain,
mtvisible(c_gregoriancalendarmt),
inference(scs_inference,[],[i_0_498,i_0_500,i_0_468,i_0_504,i_0_328,i_0_322,i_0_323,i_0_329]) ).
cnf(i_0_521,plain,
( ~ genlmt(X1,X2)
| mtvisible(X2)
| ~ mtvisible(X1) ),
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_522,plain,
genls(c_tptpcol_14_92264,c_tptpcol_12_92262),
inference(scs_inference,[],[i_0_498,i_0_500,i_0_457,i_0_458,i_0_468,i_0_504,i_0_328,i_0_322,i_0_323,i_0_329,i_0_326]) ).
cnf(i_0_523,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_524,plain,
genlmt(c_gregoriancalendarmt,c_universalvocabularymt),
inference(scs_inference,[],[i_0_498,i_0_500,i_0_457,i_0_458,i_0_468,i_0_488,i_0_489,i_0_504,i_0_328,i_0_322,i_0_323,i_0_329,i_0_326,i_0_327]) ).
cnf(i_0_525,plain,
( ~ genlmt(X1,X2)
| genlmt(X3,X2)
| ~ genlmt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_526,plain,
( ~ isa(X1,c_tptpcol_2_65537)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_498,i_0_500,i_0_457,i_0_458,i_0_468,i_0_488,i_0_489,i_0_504,i_0_328,i_0_322,i_0_323,i_0_329,i_0_326,i_0_327,i_0_316]) ).
cnf(i_0_527,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_528,plain,
( ~ isa(X1,c_tptpcol_3_81921)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_498,i_0_500,i_0_457,i_0_458,i_0_468,i_0_488,i_0_489,i_0_504,i_0_328,i_0_322,i_0_323,i_0_329,i_0_326,i_0_327,i_0_316,i_0_321]) ).
cnf(i_0_529,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_530,plain,
( ~ tptpcol_3_81921(X1)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_498,i_0_500,i_0_457,i_0_458,i_0_468,i_0_488,i_0_489,i_0_504,i_0_328,i_0_322,i_0_323,i_0_329,i_0_326,i_0_327,i_0_316,i_0_321,i_0_403]) ).
cnf(i_0_531,plain,
( isa(X1,c_tptpcol_3_81921)
| ~ tptpcol_3_81921(X1) ),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_532,plain,
( ~ tptpcol_2_65537(X1)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_498,i_0_500,i_0_457,i_0_458,i_0_468,i_0_488,i_0_489,i_0_504,i_0_328,i_0_322,i_0_323,i_0_329,i_0_326,i_0_327,i_0_316,i_0_321,i_0_403,i_0_405]) ).
cnf(i_0_533,plain,
( isa(X1,c_tptpcol_2_65537)
| ~ tptpcol_2_65537(X1) ),
inference(rename_variables,[],[i_0_405]) ).
cnf(i_0_534,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_4_90113),
inference(scs_inference,[],[i_0_516,i_0_467,i_0_322]) ).
cnf(i_0_535,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_536,plain,
disjointwith(c_tptpcol_4_90113,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_516,i_0_518,i_0_467,i_0_322,i_0_323]) ).
cnf(i_0_537,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_538,plain,
genls(c_tptpcol_12_92262,c_tptpcol_10_92166),
inference(scs_inference,[],[i_0_516,i_0_518,i_0_459,i_0_460,i_0_467,i_0_322,i_0_323,i_0_326]) ).
cnf(i_0_539,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_540,plain,
genlmt(c_unitedstatessociallifemt,c_universalvocabularymt),
inference(scs_inference,[],[i_0_516,i_0_518,i_0_459,i_0_460,i_0_467,i_0_524,i_0_485,i_0_322,i_0_323,i_0_326,i_0_327]) ).
cnf(i_0_541,plain,
( ~ genlmt(X1,X2)
| genlmt(X3,X2)
| ~ genlmt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_542,plain,
mtvisible(c_unitedstatessociallifemt),
inference(scs_inference,[],[i_0_516,i_0_518,i_0_500,i_0_459,i_0_460,i_0_467,i_0_524,i_0_485,i_0_486,i_0_322,i_0_323,i_0_326,i_0_327,i_0_329]) ).
cnf(i_0_543,plain,
( ~ genlmt(X1,X2)
| mtvisible(X2)
| ~ mtvisible(X1) ),
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_544,plain,
( ~ isa(X1,c_tptpcol_1_1)
| ~ isa(X1,c_tptpcol_4_90113) ),
inference(scs_inference,[],[i_0_516,i_0_518,i_0_500,i_0_459,i_0_460,i_0_467,i_0_524,i_0_485,i_0_486,i_0_322,i_0_323,i_0_326,i_0_327,i_0_329,i_0_316]) ).
cnf(i_0_545,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_546,plain,
( ~ isa(X1,c_tptpcol_2_2)
| ~ isa(X1,c_tptpcol_4_90113) ),
inference(scs_inference,[],[i_0_516,i_0_518,i_0_500,i_0_459,i_0_460,i_0_467,i_0_524,i_0_484,i_0_485,i_0_486,i_0_322,i_0_323,i_0_326,i_0_327,i_0_329,i_0_316,i_0_321]) ).
cnf(i_0_547,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_548,plain,
( ~ tptpcol_1_1(X1)
| ~ isa(X1,c_tptpcol_4_90113) ),
inference(scs_inference,[],[i_0_516,i_0_518,i_0_500,i_0_459,i_0_460,i_0_467,i_0_524,i_0_484,i_0_485,i_0_486,i_0_322,i_0_323,i_0_326,i_0_327,i_0_329,i_0_316,i_0_321,i_0_420]) ).
cnf(i_0_549,plain,
( isa(X1,c_tptpcol_1_1)
| ~ tptpcol_1_1(X1) ),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_550,plain,
( ~ tptpcol_2_2(X1)
| ~ isa(X1,c_tptpcol_4_90113) ),
inference(scs_inference,[],[i_0_516,i_0_518,i_0_500,i_0_459,i_0_460,i_0_467,i_0_524,i_0_484,i_0_485,i_0_486,i_0_322,i_0_323,i_0_326,i_0_327,i_0_329,i_0_316,i_0_321,i_0_420,i_0_421]) ).
cnf(i_0_551,plain,
( isa(X1,c_tptpcol_2_2)
| ~ tptpcol_2_2(X1) ),
inference(rename_variables,[],[i_0_421]) ).
cnf(i_0_552,plain,
genls(c_tptpcol_10_92166,c_tptpcol_8_92164),
inference(scs_inference,[],[i_0_461,i_0_462,i_0_326]) ).
cnf(i_0_553,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_554,plain,
genlmt(c_peopledatamt,c_universalvocabularymt),
inference(scs_inference,[],[i_0_461,i_0_462,i_0_540,i_0_486,i_0_326,i_0_327]) ).
cnf(i_0_555,plain,
( ~ genlmt(X1,X2)
| genlmt(X3,X2)
| ~ genlmt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_556,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_5_90114),
inference(scs_inference,[],[i_0_534,i_0_461,i_0_462,i_0_466,i_0_540,i_0_486,i_0_326,i_0_327,i_0_322]) ).
cnf(i_0_557,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_558,plain,
disjointwith(c_tptpcol_5_90114,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_534,i_0_536,i_0_461,i_0_462,i_0_466,i_0_540,i_0_486,i_0_326,i_0_327,i_0_322,i_0_323]) ).
cnf(i_0_559,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_560,plain,
( ~ isa(X1,c_tptpcol_1_1)
| ~ isa(X1,c_tptpcol_5_90114) ),
inference(scs_inference,[],[i_0_534,i_0_536,i_0_461,i_0_462,i_0_466,i_0_540,i_0_486,i_0_326,i_0_327,i_0_322,i_0_323,i_0_316]) ).
cnf(i_0_561,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_562,plain,
( ~ isa(X1,c_tptpcol_2_2)
| ~ isa(X1,c_tptpcol_5_90114) ),
inference(scs_inference,[],[i_0_534,i_0_536,i_0_461,i_0_462,i_0_466,i_0_540,i_0_484,i_0_486,i_0_326,i_0_327,i_0_322,i_0_323,i_0_316,i_0_321]) ).
cnf(i_0_563,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_564,plain,
( ~ tptpcol_1_1(X1)
| ~ isa(X1,c_tptpcol_5_90114) ),
inference(scs_inference,[],[i_0_534,i_0_536,i_0_461,i_0_462,i_0_466,i_0_540,i_0_484,i_0_486,i_0_326,i_0_327,i_0_322,i_0_323,i_0_316,i_0_321,i_0_420]) ).
cnf(i_0_565,plain,
( isa(X1,c_tptpcol_1_1)
| ~ tptpcol_1_1(X1) ),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_566,plain,
( ~ tptpcol_2_2(X1)
| ~ isa(X1,c_tptpcol_5_90114) ),
inference(scs_inference,[],[i_0_534,i_0_536,i_0_461,i_0_462,i_0_466,i_0_540,i_0_484,i_0_486,i_0_326,i_0_327,i_0_322,i_0_323,i_0_316,i_0_321,i_0_420,i_0_421]) ).
cnf(i_0_567,plain,
( isa(X1,c_tptpcol_2_2)
| ~ tptpcol_2_2(X1) ),
inference(rename_variables,[],[i_0_421]) ).
cnf(i_0_568,plain,
genls(c_tptpcol_8_92164,c_tptpcol_6_92162),
inference(scs_inference,[],[i_0_463,i_0_464,i_0_326]) ).
cnf(i_0_569,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_570,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_6_92162),
inference(scs_inference,[],[i_0_556,i_0_463,i_0_464,i_0_465,i_0_326,i_0_322]) ).
cnf(i_0_571,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_572,plain,
disjointwith(c_tptpcol_6_92162,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_556,i_0_558,i_0_463,i_0_464,i_0_465,i_0_326,i_0_322,i_0_323]) ).
cnf(i_0_573,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_574,plain,
genlmt(c_peopledatamt,c_basekb),
inference(scs_inference,[],[i_0_556,i_0_558,i_0_489,i_0_504,i_0_463,i_0_464,i_0_465,i_0_326,i_0_322,i_0_323,i_0_327]) ).
cnf(i_0_575,plain,
( ~ genlmt(X1,X2)
| genlmt(X3,X2)
| ~ genlmt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_576,plain,
( ~ isa(X1,c_tptpcol_1_1)
| ~ isa(X1,c_tptpcol_6_92162) ),
inference(scs_inference,[],[i_0_556,i_0_558,i_0_489,i_0_504,i_0_463,i_0_464,i_0_465,i_0_326,i_0_322,i_0_323,i_0_327,i_0_316]) ).
cnf(i_0_577,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_578,plain,
( ~ isa(X1,c_tptpcol_2_2)
| ~ isa(X1,c_tptpcol_6_92162) ),
inference(scs_inference,[],[i_0_556,i_0_558,i_0_489,i_0_504,i_0_463,i_0_464,i_0_465,i_0_484,i_0_326,i_0_322,i_0_323,i_0_327,i_0_316,i_0_321]) ).
cnf(i_0_579,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_580,plain,
( ~ tptpcol_1_1(X1)
| ~ isa(X1,c_tptpcol_6_92162) ),
inference(scs_inference,[],[i_0_556,i_0_558,i_0_489,i_0_504,i_0_463,i_0_464,i_0_465,i_0_484,i_0_326,i_0_322,i_0_323,i_0_327,i_0_316,i_0_321,i_0_420]) ).
cnf(i_0_581,plain,
( isa(X1,c_tptpcol_1_1)
| ~ tptpcol_1_1(X1) ),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_582,plain,
( ~ tptpcol_2_2(X1)
| ~ isa(X1,c_tptpcol_6_92162) ),
inference(scs_inference,[],[i_0_556,i_0_558,i_0_489,i_0_504,i_0_463,i_0_464,i_0_465,i_0_484,i_0_326,i_0_322,i_0_323,i_0_327,i_0_316,i_0_321,i_0_420,i_0_421]) ).
cnf(i_0_583,plain,
( isa(X1,c_tptpcol_2_2)
| ~ tptpcol_2_2(X1) ),
inference(rename_variables,[],[i_0_421]) ).
cnf(i_0_584,plain,
genls(c_tptpcol_16_26926,c_tptpcol_14_26921),
inference(scs_inference,[],[i_0_470,i_0_471,i_0_326]) ).
cnf(i_0_585,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_586,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_14_92264),
inference(scs_inference,[],[i_0_422,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322]) ).
cnf(i_0_587,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_588,plain,
~ disjointwith(c_tptpcol_15_26925,c_tptpcol_16_92269),
inference(scs_inference,[],[i_0_422,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323]) ).
cnf(i_0_589,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_590,plain,
genlmt(c_unitedstatessociallifemt,c_basekb),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327]) ).
cnf(i_0_591,plain,
( ~ genlmt(X1,X2)
| genlmt(X3,X2)
| ~ genlmt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_592,plain,
( isa(X1,c_tptpcol_15_26925)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321]) ).
cnf(i_0_593,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_594,plain,
( tptpcol_15_26925(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_367]) ).
cnf(i_0_595,plain,
( ~ isa(X1,c_tptpcol_15_26925)
| tptpcol_15_26925(X1) ),
inference(rename_variables,[],[i_0_367]) ).
cnf(i_0_596,plain,
( tptpcol_14_26921(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_367,i_0_440]) ).
cnf(i_0_597,plain,
( ~ tptpcol_15_26925(X1)
| tptpcol_14_26921(X1) ),
inference(rename_variables,[],[i_0_440]) ).
cnf(i_0_598,plain,
( tptpcol_13_26920(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_367,i_0_440,i_0_441]) ).
cnf(i_0_599,plain,
( ~ tptpcol_14_26921(X1)
| tptpcol_13_26920(X1) ),
inference(rename_variables,[],[i_0_441]) ).
cnf(i_0_600,plain,
( tptpcol_12_26919(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_367,i_0_440,i_0_441,i_0_442]) ).
cnf(i_0_601,plain,
( ~ tptpcol_13_26920(X1)
| tptpcol_12_26919(X1) ),
inference(rename_variables,[],[i_0_442]) ).
cnf(i_0_602,plain,
( tptpcol_11_26887(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_367,i_0_440,i_0_441,i_0_442,i_0_443]) ).
cnf(i_0_603,plain,
( ~ tptpcol_12_26919(X1)
| tptpcol_11_26887(X1) ),
inference(rename_variables,[],[i_0_443]) ).
cnf(i_0_604,plain,
( tptpcol_10_26886(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_367,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444]) ).
cnf(i_0_605,plain,
( ~ tptpcol_11_26887(X1)
| tptpcol_10_26886(X1) ),
inference(rename_variables,[],[i_0_444]) ).
cnf(i_0_606,plain,
( tptpcol_9_26885(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_367,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445]) ).
cnf(i_0_607,plain,
( ~ tptpcol_10_26886(X1)
| tptpcol_9_26885(X1) ),
inference(rename_variables,[],[i_0_445]) ).
cnf(i_0_608,plain,
( tptpcol_8_26629(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_367,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_446]) ).
cnf(i_0_609,plain,
( ~ tptpcol_9_26885(X1)
| tptpcol_8_26629(X1) ),
inference(rename_variables,[],[i_0_446]) ).
cnf(i_0_610,plain,
( tptpcol_7_26628(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_367,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_446,i_0_447]) ).
cnf(i_0_611,plain,
( ~ tptpcol_8_26629(X1)
| tptpcol_7_26628(X1) ),
inference(rename_variables,[],[i_0_447]) ).
cnf(i_0_612,plain,
( tptpcol_6_26627(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_367,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_446,i_0_447,i_0_448]) ).
cnf(i_0_613,plain,
( ~ tptpcol_7_26628(X1)
| tptpcol_6_26627(X1) ),
inference(rename_variables,[],[i_0_448]) ).
cnf(i_0_614,plain,
( tptpcol_5_24579(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_367,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_446,i_0_447,i_0_448,i_0_449]) ).
cnf(i_0_615,plain,
( ~ tptpcol_6_26627(X1)
| tptpcol_5_24579(X1) ),
inference(rename_variables,[],[i_0_449]) ).
cnf(i_0_616,plain,
( tptpcol_4_24578(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_367,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_446,i_0_447,i_0_448,i_0_449,i_0_450]) ).
cnf(i_0_617,plain,
( ~ tptpcol_5_24579(X1)
| tptpcol_4_24578(X1) ),
inference(rename_variables,[],[i_0_450]) ).
cnf(i_0_618,plain,
( tptpcol_3_16386(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_367,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_446,i_0_447,i_0_448,i_0_449,i_0_450,i_0_451]) ).
cnf(i_0_619,plain,
( ~ tptpcol_4_24578(X1)
| tptpcol_3_16386(X1) ),
inference(rename_variables,[],[i_0_451]) ).
cnf(i_0_620,plain,
( tptpcol_2_2(X1)
| ~ isa(X1,c_tptpcol_16_26926) ),
inference(scs_inference,[],[i_0_422,i_0_485,i_0_489,i_0_470,i_0_471,i_0_502,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_367,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_446,i_0_447,i_0_448,i_0_449,i_0_450,i_0_451,i_0_453]) ).
cnf(i_0_621,plain,
( ~ tptpcol_3_16386(X1)
| tptpcol_2_2(X1) ),
inference(rename_variables,[],[i_0_453]) ).
cnf(i_0_623,plain,
genls(c_tptpcol_14_26921,c_tptpcol_12_26919),
inference(scs_inference,[],[i_0_472,i_0_473,i_0_326]) ).
cnf(i_0_624,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_625,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_12_92262),
inference(scs_inference,[],[i_0_586,i_0_472,i_0_473,i_0_522,i_0_326,i_0_322]) ).
cnf(i_0_626,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_627,plain,
disjointwith(c_tptpcol_8_92164,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_572,i_0_586,i_0_472,i_0_473,i_0_522,i_0_568,i_0_326,i_0_322,i_0_323]) ).
cnf(i_0_628,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_629,plain,
genlmt(c_unitedstatesgeographypeoplemt,c_gregoriancalendarmt),
inference(scs_inference,[],[i_0_572,i_0_586,i_0_487,i_0_504,i_0_472,i_0_473,i_0_522,i_0_568,i_0_326,i_0_322,i_0_323,i_0_327]) ).
cnf(i_0_630,plain,
( ~ genlmt(X1,X2)
| genlmt(X3,X2)
| ~ genlmt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_631,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_8_92164),
inference(scs_inference,[],[i_0_572,i_0_586,i_0_487,i_0_504,i_0_472,i_0_473,i_0_522,i_0_568,i_0_326,i_0_322,i_0_323,i_0_327,i_0_328]) ).
cnf(i_0_632,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_633,plain,
( ~ isa(X1,c_tptpcol_8_92164)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_572,i_0_586,i_0_487,i_0_504,i_0_472,i_0_473,i_0_522,i_0_568,i_0_326,i_0_322,i_0_323,i_0_327,i_0_328,i_0_316]) ).
cnf(i_0_634,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_635,plain,
( ~ isa(X1,c_tptpcol_10_92166)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_572,i_0_586,i_0_487,i_0_504,i_0_472,i_0_473,i_0_522,i_0_552,i_0_568,i_0_326,i_0_322,i_0_323,i_0_327,i_0_328,i_0_316,i_0_321]) ).
cnf(i_0_636,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_637,plain,
( ~ tptpcol_10_92166(X1)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_572,i_0_586,i_0_487,i_0_504,i_0_472,i_0_473,i_0_522,i_0_552,i_0_568,i_0_326,i_0_322,i_0_323,i_0_327,i_0_328,i_0_316,i_0_321,i_0_396]) ).
cnf(i_0_638,plain,
( isa(X1,c_tptpcol_10_92166)
| ~ tptpcol_10_92166(X1) ),
inference(rename_variables,[],[i_0_396]) ).
cnf(i_0_639,plain,
( ~ tptpcol_8_92164(X1)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_572,i_0_586,i_0_487,i_0_504,i_0_472,i_0_473,i_0_522,i_0_552,i_0_568,i_0_326,i_0_322,i_0_323,i_0_327,i_0_328,i_0_316,i_0_321,i_0_396,i_0_398]) ).
cnf(i_0_640,plain,
( isa(X1,c_tptpcol_8_92164)
| ~ tptpcol_8_92164(X1) ),
inference(rename_variables,[],[i_0_398]) ).
cnf(i_0_641,plain,
genls(c_tptpcol_12_26919,c_tptpcol_10_26886),
inference(scs_inference,[],[i_0_474,i_0_475,i_0_326]) ).
cnf(i_0_642,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_643,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_10_92166),
inference(scs_inference,[],[i_0_625,i_0_474,i_0_475,i_0_538,i_0_326,i_0_322]) ).
cnf(i_0_644,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_645,plain,
~ disjointwith(c_tptpcol_14_26921,c_tptpcol_16_92269),
inference(scs_inference,[],[i_0_422,i_0_625,i_0_474,i_0_475,i_0_538,i_0_584,i_0_326,i_0_322,i_0_323]) ).
cnf(i_0_646,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_647,plain,
genlmt(c_unitedstatesgeographypeoplemt,c_unitedstatessociallifemt),
inference(scs_inference,[],[i_0_422,i_0_625,i_0_487,i_0_486,i_0_474,i_0_475,i_0_538,i_0_584,i_0_326,i_0_322,i_0_323,i_0_327]) ).
cnf(i_0_648,plain,
( ~ genlmt(X1,X2)
| genlmt(X3,X2)
| ~ genlmt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_649,plain,
( isa(X1,c_tptpcol_11_26887)
| ~ isa(X1,c_tptpcol_12_26919) ),
inference(scs_inference,[],[i_0_422,i_0_625,i_0_487,i_0_486,i_0_474,i_0_475,i_0_538,i_0_584,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321]) ).
cnf(i_0_650,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_651,plain,
( tptpcol_11_26887(X1)
| ~ isa(X1,c_tptpcol_12_26919) ),
inference(scs_inference,[],[i_0_422,i_0_625,i_0_487,i_0_486,i_0_474,i_0_475,i_0_538,i_0_584,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_371]) ).
cnf(i_0_652,plain,
( ~ isa(X1,c_tptpcol_11_26887)
| tptpcol_11_26887(X1) ),
inference(rename_variables,[],[i_0_371]) ).
cnf(i_0_653,plain,
( tptpcol_10_26886(X1)
| ~ isa(X1,c_tptpcol_12_26919) ),
inference(scs_inference,[],[i_0_422,i_0_625,i_0_487,i_0_486,i_0_474,i_0_475,i_0_538,i_0_584,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_371,i_0_444]) ).
cnf(i_0_654,plain,
( ~ tptpcol_11_26887(X1)
| tptpcol_10_26886(X1) ),
inference(rename_variables,[],[i_0_444]) ).
cnf(i_0_655,plain,
( tptpcol_9_26885(X1)
| ~ isa(X1,c_tptpcol_12_26919) ),
inference(scs_inference,[],[i_0_422,i_0_625,i_0_487,i_0_486,i_0_474,i_0_475,i_0_538,i_0_584,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_371,i_0_444,i_0_445]) ).
cnf(i_0_656,plain,
( ~ tptpcol_10_26886(X1)
| tptpcol_9_26885(X1) ),
inference(rename_variables,[],[i_0_445]) ).
cnf(i_0_657,plain,
( tptpcol_8_26629(X1)
| ~ isa(X1,c_tptpcol_12_26919) ),
inference(scs_inference,[],[i_0_422,i_0_625,i_0_487,i_0_486,i_0_474,i_0_475,i_0_538,i_0_584,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_371,i_0_444,i_0_445,i_0_446]) ).
cnf(i_0_658,plain,
( ~ tptpcol_9_26885(X1)
| tptpcol_8_26629(X1) ),
inference(rename_variables,[],[i_0_446]) ).
cnf(i_0_659,plain,
( tptpcol_7_26628(X1)
| ~ isa(X1,c_tptpcol_12_26919) ),
inference(scs_inference,[],[i_0_422,i_0_625,i_0_487,i_0_486,i_0_474,i_0_475,i_0_538,i_0_584,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_371,i_0_444,i_0_445,i_0_446,i_0_447]) ).
cnf(i_0_660,plain,
( ~ tptpcol_8_26629(X1)
| tptpcol_7_26628(X1) ),
inference(rename_variables,[],[i_0_447]) ).
cnf(i_0_661,plain,
( tptpcol_6_26627(X1)
| ~ isa(X1,c_tptpcol_12_26919) ),
inference(scs_inference,[],[i_0_422,i_0_625,i_0_487,i_0_486,i_0_474,i_0_475,i_0_538,i_0_584,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_371,i_0_444,i_0_445,i_0_446,i_0_447,i_0_448]) ).
cnf(i_0_662,plain,
( ~ tptpcol_7_26628(X1)
| tptpcol_6_26627(X1) ),
inference(rename_variables,[],[i_0_448]) ).
cnf(i_0_663,plain,
( tptpcol_5_24579(X1)
| ~ isa(X1,c_tptpcol_12_26919) ),
inference(scs_inference,[],[i_0_422,i_0_625,i_0_487,i_0_486,i_0_474,i_0_475,i_0_538,i_0_584,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_371,i_0_444,i_0_445,i_0_446,i_0_447,i_0_448,i_0_449]) ).
cnf(i_0_664,plain,
( ~ tptpcol_6_26627(X1)
| tptpcol_5_24579(X1) ),
inference(rename_variables,[],[i_0_449]) ).
cnf(i_0_665,plain,
( tptpcol_4_24578(X1)
| ~ isa(X1,c_tptpcol_12_26919) ),
inference(scs_inference,[],[i_0_422,i_0_625,i_0_487,i_0_486,i_0_474,i_0_475,i_0_538,i_0_584,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_371,i_0_444,i_0_445,i_0_446,i_0_447,i_0_448,i_0_449,i_0_450]) ).
cnf(i_0_666,plain,
( ~ tptpcol_5_24579(X1)
| tptpcol_4_24578(X1) ),
inference(rename_variables,[],[i_0_450]) ).
cnf(i_0_667,plain,
( tptpcol_3_16386(X1)
| ~ isa(X1,c_tptpcol_12_26919) ),
inference(scs_inference,[],[i_0_422,i_0_625,i_0_487,i_0_486,i_0_474,i_0_475,i_0_538,i_0_584,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_371,i_0_444,i_0_445,i_0_446,i_0_447,i_0_448,i_0_449,i_0_450,i_0_451]) ).
cnf(i_0_668,plain,
( ~ tptpcol_4_24578(X1)
| tptpcol_3_16386(X1) ),
inference(rename_variables,[],[i_0_451]) ).
cnf(i_0_669,plain,
( tptpcol_2_2(X1)
| ~ isa(X1,c_tptpcol_12_26919) ),
inference(scs_inference,[],[i_0_422,i_0_625,i_0_487,i_0_486,i_0_474,i_0_475,i_0_538,i_0_584,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_371,i_0_444,i_0_445,i_0_446,i_0_447,i_0_448,i_0_449,i_0_450,i_0_451,i_0_453]) ).
cnf(i_0_670,plain,
( ~ tptpcol_3_16386(X1)
| tptpcol_2_2(X1) ),
inference(rename_variables,[],[i_0_453]) ).
cnf(i_0_672,plain,
genls(c_tptpcol_10_26886,c_tptpcol_8_26629),
inference(scs_inference,[],[i_0_476,i_0_477,i_0_326]) ).
cnf(i_0_673,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_674,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_13_92263),
inference(scs_inference,[],[i_0_586,i_0_476,i_0_477,i_0_457,i_0_326,i_0_322]) ).
cnf(i_0_675,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_676,plain,
~ disjointwith(c_tptpcol_12_26919,c_tptpcol_16_92269),
inference(scs_inference,[],[i_0_645,i_0_586,i_0_476,i_0_477,i_0_623,i_0_457,i_0_326,i_0_322,i_0_323]) ).
cnf(i_0_677,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_678,plain,
genlmt(c_unitedstatesgeographypeoplemt,c_universalvocabularymt),
inference(scs_inference,[],[i_0_645,i_0_586,i_0_487,i_0_554,i_0_476,i_0_477,i_0_623,i_0_457,i_0_326,i_0_322,i_0_323,i_0_327]) ).
cnf(i_0_679,plain,
( ~ genlmt(X1,X2)
| genlmt(X3,X2)
| ~ genlmt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_680,plain,
( isa(X1,c_tptpcol_9_26885)
| ~ isa(X1,c_tptpcol_10_26886) ),
inference(scs_inference,[],[i_0_645,i_0_586,i_0_487,i_0_554,i_0_476,i_0_477,i_0_623,i_0_457,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321]) ).
cnf(i_0_681,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_682,plain,
( tptpcol_9_26885(X1)
| ~ isa(X1,c_tptpcol_10_26886) ),
inference(scs_inference,[],[i_0_645,i_0_586,i_0_487,i_0_554,i_0_476,i_0_477,i_0_623,i_0_457,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_373]) ).
cnf(i_0_683,plain,
( ~ isa(X1,c_tptpcol_9_26885)
| tptpcol_9_26885(X1) ),
inference(rename_variables,[],[i_0_373]) ).
cnf(i_0_684,plain,
( tptpcol_8_26629(X1)
| ~ isa(X1,c_tptpcol_10_26886) ),
inference(scs_inference,[],[i_0_645,i_0_586,i_0_487,i_0_554,i_0_476,i_0_477,i_0_623,i_0_457,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_373,i_0_446]) ).
cnf(i_0_685,plain,
( ~ tptpcol_9_26885(X1)
| tptpcol_8_26629(X1) ),
inference(rename_variables,[],[i_0_446]) ).
cnf(i_0_686,plain,
( tptpcol_7_26628(X1)
| ~ isa(X1,c_tptpcol_10_26886) ),
inference(scs_inference,[],[i_0_645,i_0_586,i_0_487,i_0_554,i_0_476,i_0_477,i_0_623,i_0_457,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_373,i_0_446,i_0_447]) ).
cnf(i_0_687,plain,
( ~ tptpcol_8_26629(X1)
| tptpcol_7_26628(X1) ),
inference(rename_variables,[],[i_0_447]) ).
cnf(i_0_688,plain,
( tptpcol_6_26627(X1)
| ~ isa(X1,c_tptpcol_10_26886) ),
inference(scs_inference,[],[i_0_645,i_0_586,i_0_487,i_0_554,i_0_476,i_0_477,i_0_623,i_0_457,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_373,i_0_446,i_0_447,i_0_448]) ).
cnf(i_0_689,plain,
( ~ tptpcol_7_26628(X1)
| tptpcol_6_26627(X1) ),
inference(rename_variables,[],[i_0_448]) ).
cnf(i_0_690,plain,
( tptpcol_5_24579(X1)
| ~ isa(X1,c_tptpcol_10_26886) ),
inference(scs_inference,[],[i_0_645,i_0_586,i_0_487,i_0_554,i_0_476,i_0_477,i_0_623,i_0_457,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_373,i_0_446,i_0_447,i_0_448,i_0_449]) ).
cnf(i_0_691,plain,
( ~ tptpcol_6_26627(X1)
| tptpcol_5_24579(X1) ),
inference(rename_variables,[],[i_0_449]) ).
cnf(i_0_692,plain,
( tptpcol_4_24578(X1)
| ~ isa(X1,c_tptpcol_10_26886) ),
inference(scs_inference,[],[i_0_645,i_0_586,i_0_487,i_0_554,i_0_476,i_0_477,i_0_623,i_0_457,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_373,i_0_446,i_0_447,i_0_448,i_0_449,i_0_450]) ).
cnf(i_0_693,plain,
( ~ tptpcol_5_24579(X1)
| tptpcol_4_24578(X1) ),
inference(rename_variables,[],[i_0_450]) ).
cnf(i_0_694,plain,
( tptpcol_3_16386(X1)
| ~ isa(X1,c_tptpcol_10_26886) ),
inference(scs_inference,[],[i_0_645,i_0_586,i_0_487,i_0_554,i_0_476,i_0_477,i_0_623,i_0_457,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_373,i_0_446,i_0_447,i_0_448,i_0_449,i_0_450,i_0_451]) ).
cnf(i_0_695,plain,
( ~ tptpcol_4_24578(X1)
| tptpcol_3_16386(X1) ),
inference(rename_variables,[],[i_0_451]) ).
cnf(i_0_696,plain,
( tptpcol_2_2(X1)
| ~ isa(X1,c_tptpcol_10_26886) ),
inference(scs_inference,[],[i_0_645,i_0_586,i_0_487,i_0_554,i_0_476,i_0_477,i_0_623,i_0_457,i_0_326,i_0_322,i_0_323,i_0_327,i_0_321,i_0_373,i_0_446,i_0_447,i_0_448,i_0_449,i_0_450,i_0_451,i_0_453]) ).
cnf(i_0_697,plain,
( ~ tptpcol_3_16386(X1)
| tptpcol_2_2(X1) ),
inference(rename_variables,[],[i_0_453]) ).
cnf(i_0_699,plain,
genls(c_tptpcol_8_26629,c_tptpcol_6_26627),
inference(scs_inference,[],[i_0_478,i_0_479,i_0_326]) ).
cnf(i_0_700,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_701,plain,
~ disjointwith(c_tptpcol_10_26886,c_tptpcol_16_92269),
inference(scs_inference,[],[i_0_676,i_0_478,i_0_479,i_0_641,i_0_326,i_0_323]) ).
cnf(i_0_702,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_703,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_11_92230),
inference(scs_inference,[],[i_0_676,i_0_625,i_0_478,i_0_479,i_0_641,i_0_459,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_704,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_705,plain,
genlmt(c_unitedstatesgeographypeoplemt,c_basekb),
inference(scs_inference,[],[i_0_676,i_0_625,i_0_487,i_0_574,i_0_478,i_0_479,i_0_641,i_0_459,i_0_326,i_0_323,i_0_322,i_0_327]) ).
cnf(i_0_706,plain,
( ~ genlmt(X1,X2)
| genlmt(X3,X2)
| ~ genlmt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_707,plain,
( isa(X1,c_tptpcol_7_26628)
| ~ isa(X1,c_tptpcol_8_26629) ),
inference(scs_inference,[],[i_0_676,i_0_625,i_0_487,i_0_574,i_0_478,i_0_479,i_0_641,i_0_459,i_0_326,i_0_323,i_0_322,i_0_327,i_0_321]) ).
cnf(i_0_708,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_709,plain,
( tptpcol_7_26628(X1)
| ~ isa(X1,c_tptpcol_8_26629) ),
inference(scs_inference,[],[i_0_676,i_0_625,i_0_487,i_0_574,i_0_478,i_0_479,i_0_641,i_0_459,i_0_326,i_0_323,i_0_322,i_0_327,i_0_321,i_0_375]) ).
cnf(i_0_710,plain,
( ~ isa(X1,c_tptpcol_7_26628)
| tptpcol_7_26628(X1) ),
inference(rename_variables,[],[i_0_375]) ).
cnf(i_0_711,plain,
( tptpcol_6_26627(X1)
| ~ isa(X1,c_tptpcol_8_26629) ),
inference(scs_inference,[],[i_0_676,i_0_625,i_0_487,i_0_574,i_0_478,i_0_479,i_0_641,i_0_459,i_0_326,i_0_323,i_0_322,i_0_327,i_0_321,i_0_375,i_0_448]) ).
cnf(i_0_712,plain,
( ~ tptpcol_7_26628(X1)
| tptpcol_6_26627(X1) ),
inference(rename_variables,[],[i_0_448]) ).
cnf(i_0_713,plain,
( tptpcol_5_24579(X1)
| ~ isa(X1,c_tptpcol_8_26629) ),
inference(scs_inference,[],[i_0_676,i_0_625,i_0_487,i_0_574,i_0_478,i_0_479,i_0_641,i_0_459,i_0_326,i_0_323,i_0_322,i_0_327,i_0_321,i_0_375,i_0_448,i_0_449]) ).
cnf(i_0_714,plain,
( ~ tptpcol_6_26627(X1)
| tptpcol_5_24579(X1) ),
inference(rename_variables,[],[i_0_449]) ).
cnf(i_0_715,plain,
( tptpcol_4_24578(X1)
| ~ isa(X1,c_tptpcol_8_26629) ),
inference(scs_inference,[],[i_0_676,i_0_625,i_0_487,i_0_574,i_0_478,i_0_479,i_0_641,i_0_459,i_0_326,i_0_323,i_0_322,i_0_327,i_0_321,i_0_375,i_0_448,i_0_449,i_0_450]) ).
cnf(i_0_716,plain,
( ~ tptpcol_5_24579(X1)
| tptpcol_4_24578(X1) ),
inference(rename_variables,[],[i_0_450]) ).
cnf(i_0_717,plain,
( tptpcol_3_16386(X1)
| ~ isa(X1,c_tptpcol_8_26629) ),
inference(scs_inference,[],[i_0_676,i_0_625,i_0_487,i_0_574,i_0_478,i_0_479,i_0_641,i_0_459,i_0_326,i_0_323,i_0_322,i_0_327,i_0_321,i_0_375,i_0_448,i_0_449,i_0_450,i_0_451]) ).
cnf(i_0_718,plain,
( ~ tptpcol_4_24578(X1)
| tptpcol_3_16386(X1) ),
inference(rename_variables,[],[i_0_451]) ).
cnf(i_0_719,plain,
( tptpcol_2_2(X1)
| ~ isa(X1,c_tptpcol_8_26629) ),
inference(scs_inference,[],[i_0_676,i_0_625,i_0_487,i_0_574,i_0_478,i_0_479,i_0_641,i_0_459,i_0_326,i_0_323,i_0_322,i_0_327,i_0_321,i_0_375,i_0_448,i_0_449,i_0_450,i_0_451,i_0_453]) ).
cnf(i_0_720,plain,
( ~ tptpcol_3_16386(X1)
| tptpcol_2_2(X1) ),
inference(rename_variables,[],[i_0_453]) ).
cnf(i_0_722,plain,
genls(c_tptpcol_6_26627,c_tptpcol_4_24578),
inference(scs_inference,[],[i_0_480,i_0_481,i_0_326]) ).
cnf(i_0_723,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_724,plain,
~ disjointwith(c_tptpcol_8_26629,c_tptpcol_16_92269),
inference(scs_inference,[],[i_0_701,i_0_480,i_0_481,i_0_672,i_0_326,i_0_323]) ).
cnf(i_0_725,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_726,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_9_92165),
inference(scs_inference,[],[i_0_643,i_0_701,i_0_480,i_0_481,i_0_672,i_0_461,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_727,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_728,plain,
( isa(X1,c_tptpcol_5_24579)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_643,i_0_701,i_0_480,i_0_481,i_0_672,i_0_461,i_0_326,i_0_323,i_0_322,i_0_321]) ).
cnf(i_0_729,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_730,plain,
( tptpcol_5_24579(X1)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_643,i_0_701,i_0_480,i_0_481,i_0_672,i_0_461,i_0_326,i_0_323,i_0_322,i_0_321,i_0_377]) ).
cnf(i_0_731,plain,
( ~ isa(X1,c_tptpcol_5_24579)
| tptpcol_5_24579(X1) ),
inference(rename_variables,[],[i_0_377]) ).
cnf(i_0_732,plain,
( tptpcol_4_24578(X1)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_643,i_0_701,i_0_480,i_0_481,i_0_672,i_0_461,i_0_326,i_0_323,i_0_322,i_0_321,i_0_377,i_0_450]) ).
cnf(i_0_733,plain,
( ~ tptpcol_5_24579(X1)
| tptpcol_4_24578(X1) ),
inference(rename_variables,[],[i_0_450]) ).
cnf(i_0_734,plain,
( tptpcol_3_16386(X1)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_643,i_0_701,i_0_480,i_0_481,i_0_672,i_0_461,i_0_326,i_0_323,i_0_322,i_0_321,i_0_377,i_0_450,i_0_451]) ).
cnf(i_0_735,plain,
( ~ tptpcol_4_24578(X1)
| tptpcol_3_16386(X1) ),
inference(rename_variables,[],[i_0_451]) ).
cnf(i_0_736,plain,
( tptpcol_2_2(X1)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_643,i_0_701,i_0_480,i_0_481,i_0_672,i_0_461,i_0_326,i_0_323,i_0_322,i_0_321,i_0_377,i_0_450,i_0_451,i_0_453]) ).
cnf(i_0_737,plain,
( ~ tptpcol_3_16386(X1)
| tptpcol_2_2(X1) ),
inference(rename_variables,[],[i_0_453]) ).
cnf(i_0_738,plain,
( genlmt(X1,c_peopledatamt)
| ~ isa(X2,c_tptpcol_6_26627)
| ~ genlmt(X1,c_unitedstatesgeographypeoplemt) ),
inference(scs_inference,[],[i_0_516,i_0_643,i_0_701,i_0_487,i_0_480,i_0_481,i_0_672,i_0_461,i_0_326,i_0_323,i_0_322,i_0_321,i_0_377,i_0_450,i_0_451,i_0_453,i_0_327]) ).
cnf(i_0_739,plain,
genls(c_tptpcol_4_24578,c_tptpcol_2_2),
inference(scs_inference,[],[i_0_482,i_0_483,i_0_326]) ).
cnf(i_0_740,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_741,plain,
~ disjointwith(c_tptpcol_6_26627,c_tptpcol_16_92269),
inference(scs_inference,[],[i_0_724,i_0_482,i_0_483,i_0_699,i_0_326,i_0_323]) ).
cnf(i_0_742,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_743,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_8_92164),
inference(scs_inference,[],[i_0_724,i_0_726,i_0_482,i_0_483,i_0_699,i_0_462,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_744,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_745,plain,
( isa(X1,c_tptpcol_3_16386)
| ~ isa(X1,c_tptpcol_4_24578) ),
inference(scs_inference,[],[i_0_724,i_0_726,i_0_482,i_0_483,i_0_699,i_0_462,i_0_326,i_0_323,i_0_322,i_0_321]) ).
cnf(i_0_746,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_747,plain,
( tptpcol_3_16386(X1)
| ~ isa(X1,c_tptpcol_4_24578) ),
inference(scs_inference,[],[i_0_724,i_0_726,i_0_482,i_0_483,i_0_699,i_0_462,i_0_326,i_0_323,i_0_322,i_0_321,i_0_379]) ).
cnf(i_0_748,plain,
( ~ isa(X1,c_tptpcol_3_16386)
| tptpcol_3_16386(X1) ),
inference(rename_variables,[],[i_0_379]) ).
cnf(i_0_749,plain,
( tptpcol_2_2(X1)
| ~ isa(X1,c_tptpcol_4_24578) ),
inference(scs_inference,[],[i_0_724,i_0_726,i_0_482,i_0_483,i_0_699,i_0_462,i_0_326,i_0_323,i_0_322,i_0_321,i_0_379,i_0_453]) ).
cnf(i_0_750,plain,
( ~ tptpcol_3_16386(X1)
| tptpcol_2_2(X1) ),
inference(rename_variables,[],[i_0_453]) ).
cnf(i_0_751,plain,
( genlmt(X1,c_peopledatamt)
| ~ isa(X2,c_tptpcol_4_24578)
| ~ genlmt(X1,c_unitedstatesgeographypeoplemt) ),
inference(scs_inference,[],[i_0_516,i_0_724,i_0_726,i_0_487,i_0_482,i_0_483,i_0_699,i_0_462,i_0_326,i_0_323,i_0_322,i_0_321,i_0_379,i_0_453,i_0_327]) ).
cnf(i_0_752,plain,
genls(c_tptpcol_6_26627,c_tptpcol_2_2),
inference(scs_inference,[],[i_0_722,i_0_739,i_0_326]) ).
cnf(i_0_753,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_754,plain,
~ disjointwith(c_tptpcol_4_24578,c_tptpcol_16_92269),
inference(scs_inference,[],[i_0_741,i_0_722,i_0_739,i_0_326,i_0_323]) ).
cnf(i_0_755,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_756,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_7_92163),
inference(scs_inference,[],[i_0_741,i_0_743,i_0_722,i_0_739,i_0_463,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_757,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_758,plain,
( isa(X1,c_tptpcol_4_24578)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_741,i_0_743,i_0_722,i_0_739,i_0_463,i_0_326,i_0_323,i_0_322,i_0_321]) ).
cnf(i_0_759,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_760,plain,
( ~ isa(X1,c_tptpcol_6_26627)
| isa(X1,c_tptpcol_3_16386) ),
inference(scs_inference,[],[i_0_741,i_0_743,i_0_722,i_0_739,i_0_463,i_0_326,i_0_323,i_0_322,i_0_321,i_0_745]) ).
cnf(i_0_761,plain,
( ~ isa(X1,c_tptpcol_4_24578)
| isa(X1,c_tptpcol_3_16386) ),
inference(rename_variables,[],[i_0_745]) ).
cnf(i_0_763,plain,
genls(c_tptpcol_6_26627,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_752,i_0_484,i_0_326]) ).
cnf(i_0_764,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_765,plain,
~ disjointwith(c_tptpcol_2_2,c_tptpcol_16_92269),
inference(scs_inference,[],[i_0_741,i_0_752,i_0_484,i_0_326,i_0_323]) ).
cnf(i_0_766,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_767,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_6_92162),
inference(scs_inference,[],[i_0_756,i_0_741,i_0_752,i_0_464,i_0_484,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_768,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_769,plain,
( isa(X1,c_tptpcol_2_2)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_756,i_0_741,i_0_752,i_0_464,i_0_484,i_0_326,i_0_323,i_0_322,i_0_321]) ).
cnf(i_0_770,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_771,plain,
( genlmt(X1,c_peopledatamt)
| ~ genlmt(X1,c_unitedstatesgeographypeoplemt) ),
inference(scs_inference,[],[i_0_756,i_0_741,i_0_487,i_0_752,i_0_464,i_0_484,i_0_326,i_0_323,i_0_322,i_0_321,i_0_327]) ).
cnf(i_0_772,plain,
( ~ genlmt(X1,X2)
| genlmt(X3,X2)
| ~ genlmt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_773,plain,
genls(c_tptpcol_15_92268,c_tptpcol_12_92262),
inference(scs_inference,[],[i_0_456,i_0_522,i_0_326]) ).
cnf(i_0_774,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_775,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_16_92269),
inference(scs_inference,[],[i_0_741,i_0_763,i_0_456,i_0_522,i_0_326,i_0_323]) ).
cnf(i_0_776,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_777,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_6_26627),
inference(scs_inference,[],[i_0_494,i_0_741,i_0_763,i_0_456,i_0_522,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_778,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_779,plain,
disjointwith(c_tptpcol_6_26627,c_tptpcol_1_65536),
inference(scs_inference,[],[i_0_494,i_0_741,i_0_763,i_0_456,i_0_522,i_0_326,i_0_323,i_0_322,i_0_328]) ).
cnf(i_0_780,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_781,plain,
( ~ isa(X1,c_tptpcol_1_65536)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_494,i_0_741,i_0_763,i_0_456,i_0_522,i_0_326,i_0_323,i_0_322,i_0_328,i_0_316]) ).
cnf(i_0_782,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_783,plain,
( ~ isa(X1,c_tptpcol_2_65537)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_494,i_0_741,i_0_763,i_0_456,i_0_469,i_0_522,i_0_326,i_0_323,i_0_322,i_0_328,i_0_316,i_0_321]) ).
cnf(i_0_784,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_785,plain,
( ~ tptpcol_1_65536(X1)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_494,i_0_741,i_0_763,i_0_456,i_0_469,i_0_522,i_0_326,i_0_323,i_0_322,i_0_328,i_0_316,i_0_321,i_0_404]) ).
cnf(i_0_786,plain,
( isa(X1,c_tptpcol_1_65536)
| ~ tptpcol_1_65536(X1) ),
inference(rename_variables,[],[i_0_404]) ).
cnf(i_0_787,plain,
( ~ tptpcol_2_65537(X1)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_494,i_0_741,i_0_763,i_0_456,i_0_469,i_0_522,i_0_326,i_0_323,i_0_322,i_0_328,i_0_316,i_0_321,i_0_404,i_0_405]) ).
cnf(i_0_788,plain,
( isa(X1,c_tptpcol_2_65537)
| ~ tptpcol_2_65537(X1) ),
inference(rename_variables,[],[i_0_405]) ).
cnf(i_0_790,plain,
genls(c_tptpcol_15_92268,c_tptpcol_10_92166),
inference(scs_inference,[],[i_0_773,i_0_538,i_0_326]) ).
cnf(i_0_791,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_792,plain,
~ disjointwith(c_tptpcol_13_26920,c_tptpcol_16_92269),
inference(scs_inference,[],[i_0_645,i_0_773,i_0_472,i_0_538,i_0_326,i_0_323]) ).
cnf(i_0_793,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_794,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_7_26628),
inference(scs_inference,[],[i_0_777,i_0_645,i_0_773,i_0_472,i_0_479,i_0_538,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_795,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_796,plain,
disjointwith(c_tptpcol_7_26628,c_tptpcol_1_65536),
inference(scs_inference,[],[i_0_777,i_0_645,i_0_773,i_0_472,i_0_479,i_0_538,i_0_326,i_0_323,i_0_322,i_0_328]) ).
cnf(i_0_797,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_798,plain,
( ~ isa(X1,c_tptpcol_1_65536)
| ~ isa(X1,c_tptpcol_7_26628) ),
inference(scs_inference,[],[i_0_777,i_0_645,i_0_773,i_0_472,i_0_479,i_0_538,i_0_326,i_0_323,i_0_322,i_0_328,i_0_316]) ).
cnf(i_0_799,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_800,plain,
( ~ isa(X1,c_tptpcol_2_65537)
| ~ isa(X1,c_tptpcol_7_26628) ),
inference(scs_inference,[],[i_0_777,i_0_645,i_0_773,i_0_472,i_0_479,i_0_538,i_0_469,i_0_326,i_0_323,i_0_322,i_0_328,i_0_316,i_0_321]) ).
cnf(i_0_801,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_802,plain,
( ~ tptpcol_1_65536(X1)
| ~ isa(X1,c_tptpcol_7_26628) ),
inference(scs_inference,[],[i_0_777,i_0_645,i_0_773,i_0_472,i_0_479,i_0_538,i_0_469,i_0_326,i_0_323,i_0_322,i_0_328,i_0_316,i_0_321,i_0_404]) ).
cnf(i_0_803,plain,
( isa(X1,c_tptpcol_1_65536)
| ~ tptpcol_1_65536(X1) ),
inference(rename_variables,[],[i_0_404]) ).
cnf(i_0_804,plain,
( ~ tptpcol_2_65537(X1)
| ~ isa(X1,c_tptpcol_7_26628) ),
inference(scs_inference,[],[i_0_777,i_0_645,i_0_773,i_0_472,i_0_479,i_0_538,i_0_469,i_0_326,i_0_323,i_0_322,i_0_328,i_0_316,i_0_321,i_0_404,i_0_405]) ).
cnf(i_0_805,plain,
( isa(X1,c_tptpcol_2_65537)
| ~ tptpcol_2_65537(X1) ),
inference(rename_variables,[],[i_0_405]) ).
cnf(i_0_807,plain,
genls(c_tptpcol_15_92268,c_tptpcol_8_92164),
inference(scs_inference,[],[i_0_790,i_0_552,i_0_326]) ).
cnf(i_0_808,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_809,plain,
disjointwith(c_tptpcol_10_92166,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_627,i_0_790,i_0_552,i_0_326,i_0_323]) ).
cnf(i_0_810,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_811,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_8_26629),
inference(scs_inference,[],[i_0_777,i_0_627,i_0_790,i_0_552,i_0_699,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_812,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_813,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_10_92166),
inference(scs_inference,[],[i_0_777,i_0_627,i_0_790,i_0_552,i_0_699,i_0_326,i_0_323,i_0_322,i_0_328]) ).
cnf(i_0_814,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_815,plain,
( ~ isa(X1,c_tptpcol_1_65536)
| ~ isa(X1,c_tptpcol_8_26629) ),
inference(scs_inference,[],[i_0_777,i_0_627,i_0_790,i_0_552,i_0_699,i_0_326,i_0_323,i_0_322,i_0_328,i_0_316]) ).
cnf(i_0_816,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_817,plain,
( ~ isa(X1,c_tptpcol_2_65537)
| ~ isa(X1,c_tptpcol_8_26629) ),
inference(scs_inference,[],[i_0_777,i_0_627,i_0_790,i_0_552,i_0_699,i_0_469,i_0_326,i_0_323,i_0_322,i_0_328,i_0_316,i_0_321]) ).
cnf(i_0_818,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_819,plain,
( ~ tptpcol_1_65536(X1)
| ~ isa(X1,c_tptpcol_8_26629) ),
inference(scs_inference,[],[i_0_777,i_0_627,i_0_790,i_0_552,i_0_699,i_0_469,i_0_326,i_0_323,i_0_322,i_0_328,i_0_316,i_0_321,i_0_404]) ).
cnf(i_0_820,plain,
( isa(X1,c_tptpcol_1_65536)
| ~ tptpcol_1_65536(X1) ),
inference(rename_variables,[],[i_0_404]) ).
cnf(i_0_821,plain,
( ~ tptpcol_2_65537(X1)
| ~ isa(X1,c_tptpcol_8_26629) ),
inference(scs_inference,[],[i_0_777,i_0_627,i_0_790,i_0_552,i_0_699,i_0_469,i_0_326,i_0_323,i_0_322,i_0_328,i_0_316,i_0_321,i_0_404,i_0_405]) ).
cnf(i_0_822,plain,
( isa(X1,c_tptpcol_2_65537)
| ~ tptpcol_2_65537(X1) ),
inference(rename_variables,[],[i_0_405]) ).
cnf(i_0_824,plain,
disjointwith(c_tptpcol_8_26629,c_tptpcol_1_65536),
inference(scs_inference,[],[i_0_811,i_0_328]) ).
cnf(i_0_825,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_826,plain,
genls(c_tptpcol_15_92268,c_tptpcol_6_92162),
inference(scs_inference,[],[i_0_811,i_0_807,i_0_568,i_0_328,i_0_326]) ).
cnf(i_0_827,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_828,plain,
disjointwith(c_tptpcol_15_92268,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_811,i_0_627,i_0_807,i_0_568,i_0_328,i_0_326,i_0_323]) ).
cnf(i_0_829,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_830,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_9_26885),
inference(scs_inference,[],[i_0_811,i_0_627,i_0_807,i_0_477,i_0_568,i_0_328,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_831,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_832,plain,
( ~ isa(X1,c_tptpcol_15_92268)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_811,i_0_627,i_0_807,i_0_477,i_0_568,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316]) ).
cnf(i_0_833,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_834,plain,
( ~ isa(X1,c_tptpcol_16_92269)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_811,i_0_627,i_0_807,i_0_477,i_0_568,i_0_455,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321]) ).
cnf(i_0_835,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_836,plain,
( ~ tptpcol_16_92269(X1)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_811,i_0_627,i_0_807,i_0_477,i_0_568,i_0_455,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321,i_0_390]) ).
cnf(i_0_837,plain,
( isa(X1,c_tptpcol_16_92269)
| ~ tptpcol_16_92269(X1) ),
inference(rename_variables,[],[i_0_390]) ).
cnf(i_0_838,plain,
( ~ tptpcol_15_92268(X1)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_811,i_0_627,i_0_807,i_0_477,i_0_568,i_0_455,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321,i_0_390,i_0_391]) ).
cnf(i_0_839,plain,
( isa(X1,c_tptpcol_15_92268)
| ~ tptpcol_15_92268(X1) ),
inference(rename_variables,[],[i_0_391]) ).
cnf(i_0_841,plain,
disjointwith(c_tptpcol_9_26885,c_tptpcol_1_65536),
inference(scs_inference,[],[i_0_830,i_0_328]) ).
cnf(i_0_842,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_843,plain,
genls(c_tptpcol_15_92268,c_tptpcol_5_90114),
inference(scs_inference,[],[i_0_830,i_0_826,i_0_465,i_0_328,i_0_326]) ).
cnf(i_0_844,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_845,plain,
disjointwith(c_tptpcol_11_92230,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_830,i_0_809,i_0_826,i_0_460,i_0_465,i_0_328,i_0_326,i_0_323]) ).
cnf(i_0_846,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_847,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_10_26886),
inference(scs_inference,[],[i_0_811,i_0_830,i_0_809,i_0_826,i_0_460,i_0_672,i_0_465,i_0_328,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_848,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_849,plain,
( ~ isa(X1,c_tptpcol_1_65536)
| ~ isa(X1,c_tptpcol_9_26885) ),
inference(scs_inference,[],[i_0_811,i_0_830,i_0_809,i_0_826,i_0_460,i_0_672,i_0_465,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316]) ).
cnf(i_0_850,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_851,plain,
( ~ isa(X1,c_tptpcol_2_65537)
| ~ isa(X1,c_tptpcol_9_26885) ),
inference(scs_inference,[],[i_0_811,i_0_830,i_0_809,i_0_826,i_0_460,i_0_672,i_0_465,i_0_469,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321]) ).
cnf(i_0_852,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_853,plain,
( ~ tptpcol_1_65536(X1)
| ~ isa(X1,c_tptpcol_9_26885) ),
inference(scs_inference,[],[i_0_811,i_0_830,i_0_809,i_0_826,i_0_460,i_0_672,i_0_465,i_0_469,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321,i_0_404]) ).
cnf(i_0_854,plain,
( isa(X1,c_tptpcol_1_65536)
| ~ tptpcol_1_65536(X1) ),
inference(rename_variables,[],[i_0_404]) ).
cnf(i_0_855,plain,
( ~ tptpcol_2_65537(X1)
| ~ isa(X1,c_tptpcol_9_26885) ),
inference(scs_inference,[],[i_0_811,i_0_830,i_0_809,i_0_826,i_0_460,i_0_672,i_0_465,i_0_469,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321,i_0_404,i_0_405]) ).
cnf(i_0_856,plain,
( isa(X1,c_tptpcol_2_65537)
| ~ tptpcol_2_65537(X1) ),
inference(rename_variables,[],[i_0_405]) ).
cnf(i_0_858,plain,
disjointwith(c_tptpcol_10_26886,c_tptpcol_1_65536),
inference(scs_inference,[],[i_0_847,i_0_328]) ).
cnf(i_0_859,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_860,plain,
genls(c_tptpcol_15_92268,c_tptpcol_4_90113),
inference(scs_inference,[],[i_0_847,i_0_843,i_0_466,i_0_328,i_0_326]) ).
cnf(i_0_861,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_862,plain,
disjointwith(c_tptpcol_11_26887,c_tptpcol_1_65536),
inference(scs_inference,[],[i_0_847,i_0_843,i_0_475,i_0_466,i_0_328,i_0_326,i_0_323]) ).
cnf(i_0_863,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_864,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_5_90114),
inference(scs_inference,[],[i_0_847,i_0_496,i_0_843,i_0_475,i_0_466,i_0_328,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_865,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_866,plain,
( ~ isa(X1,c_tptpcol_1_65536)
| ~ isa(X1,c_tptpcol_10_26886) ),
inference(scs_inference,[],[i_0_847,i_0_496,i_0_843,i_0_475,i_0_466,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316]) ).
cnf(i_0_867,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_868,plain,
( ~ isa(X1,c_tptpcol_2_65537)
| ~ isa(X1,c_tptpcol_10_26886) ),
inference(scs_inference,[],[i_0_847,i_0_496,i_0_843,i_0_475,i_0_466,i_0_469,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321]) ).
cnf(i_0_869,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_870,plain,
( ~ tptpcol_1_65536(X1)
| ~ isa(X1,c_tptpcol_10_26886) ),
inference(scs_inference,[],[i_0_847,i_0_496,i_0_843,i_0_475,i_0_466,i_0_469,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321,i_0_404]) ).
cnf(i_0_871,plain,
( isa(X1,c_tptpcol_1_65536)
| ~ tptpcol_1_65536(X1) ),
inference(rename_variables,[],[i_0_404]) ).
cnf(i_0_872,plain,
( ~ tptpcol_2_65537(X1)
| ~ isa(X1,c_tptpcol_10_26886) ),
inference(scs_inference,[],[i_0_847,i_0_496,i_0_843,i_0_475,i_0_466,i_0_469,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321,i_0_404,i_0_405]) ).
cnf(i_0_873,plain,
( isa(X1,c_tptpcol_2_65537)
| ~ tptpcol_2_65537(X1) ),
inference(rename_variables,[],[i_0_405]) ).
cnf(i_0_875,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_15_92268),
inference(scs_inference,[],[i_0_828,i_0_328]) ).
cnf(i_0_876,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_877,plain,
genls(c_tptpcol_15_92268,c_tptpcol_3_81921),
inference(scs_inference,[],[i_0_828,i_0_860,i_0_467,i_0_328,i_0_326]) ).
cnf(i_0_878,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_879,plain,
disjointwith(c_tptpcol_12_92262,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_828,i_0_845,i_0_860,i_0_459,i_0_467,i_0_328,i_0_326,i_0_323]) ).
cnf(i_0_880,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_881,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_4_90113),
inference(scs_inference,[],[i_0_828,i_0_845,i_0_496,i_0_860,i_0_459,i_0_467,i_0_328,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_882,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_883,plain,
( ~ isa(X1,c_tptpcol_11_92230)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_828,i_0_845,i_0_496,i_0_860,i_0_459,i_0_467,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316]) ).
cnf(i_0_884,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_885,plain,
( ~ isa(X1,c_tptpcol_12_92262)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_828,i_0_845,i_0_496,i_0_860,i_0_459,i_0_467,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321]) ).
cnf(i_0_886,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_887,plain,
( ~ tptpcol_12_92262(X1)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_828,i_0_845,i_0_496,i_0_860,i_0_459,i_0_467,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321,i_0_394]) ).
cnf(i_0_888,plain,
( isa(X1,c_tptpcol_12_92262)
| ~ tptpcol_12_92262(X1) ),
inference(rename_variables,[],[i_0_394]) ).
cnf(i_0_889,plain,
( ~ tptpcol_11_92230(X1)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_828,i_0_845,i_0_496,i_0_860,i_0_459,i_0_467,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321,i_0_394,i_0_395]) ).
cnf(i_0_890,plain,
( isa(X1,c_tptpcol_11_92230)
| ~ tptpcol_11_92230(X1) ),
inference(rename_variables,[],[i_0_395]) ).
cnf(i_0_892,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_11_26887),
inference(scs_inference,[],[i_0_862,i_0_328]) ).
cnf(i_0_893,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_894,plain,
genls(c_tptpcol_15_92268,c_tptpcol_2_65537),
inference(scs_inference,[],[i_0_862,i_0_877,i_0_468,i_0_328,i_0_326]) ).
cnf(i_0_895,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_896,plain,
disjointwith(c_tptpcol_13_92263,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_862,i_0_879,i_0_877,i_0_458,i_0_468,i_0_328,i_0_326,i_0_323]) ).
cnf(i_0_897,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_898,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_3_81921),
inference(scs_inference,[],[i_0_862,i_0_879,i_0_496,i_0_877,i_0_458,i_0_468,i_0_328,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_899,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_900,plain,
( ~ isa(X1,c_tptpcol_11_26887)
| ~ isa(X1,c_tptpcol_1_65536) ),
inference(scs_inference,[],[i_0_862,i_0_879,i_0_496,i_0_877,i_0_458,i_0_468,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316]) ).
cnf(i_0_901,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_902,plain,
( ~ isa(X1,c_tptpcol_12_26919)
| ~ isa(X1,c_tptpcol_1_65536) ),
inference(scs_inference,[],[i_0_862,i_0_879,i_0_496,i_0_877,i_0_458,i_0_474,i_0_468,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321]) ).
cnf(i_0_903,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_904,plain,
( ~ tptpcol_12_26919(X1)
| ~ isa(X1,c_tptpcol_1_65536) ),
inference(scs_inference,[],[i_0_862,i_0_879,i_0_496,i_0_877,i_0_458,i_0_474,i_0_468,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321,i_0_410]) ).
cnf(i_0_905,plain,
( isa(X1,c_tptpcol_12_26919)
| ~ tptpcol_12_26919(X1) ),
inference(rename_variables,[],[i_0_410]) ).
cnf(i_0_906,plain,
( ~ tptpcol_11_26887(X1)
| ~ isa(X1,c_tptpcol_1_65536) ),
inference(scs_inference,[],[i_0_862,i_0_879,i_0_496,i_0_877,i_0_458,i_0_474,i_0_468,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321,i_0_410,i_0_411]) ).
cnf(i_0_907,plain,
( isa(X1,c_tptpcol_11_26887)
| ~ tptpcol_11_26887(X1) ),
inference(rename_variables,[],[i_0_411]) ).
cnf(i_0_909,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_13_92263),
inference(scs_inference,[],[i_0_896,i_0_328]) ).
cnf(i_0_910,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_911,plain,
genls(c_tptpcol_15_92268,c_tptpcol_1_65536),
inference(scs_inference,[],[i_0_896,i_0_894,i_0_469,i_0_328,i_0_326]) ).
cnf(i_0_912,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_913,plain,
disjointwith(c_tptpcol_14_92264,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_896,i_0_894,i_0_457,i_0_469,i_0_328,i_0_326,i_0_323]) ).
cnf(i_0_914,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_915,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_2_65537),
inference(scs_inference,[],[i_0_896,i_0_496,i_0_894,i_0_457,i_0_469,i_0_328,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_916,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_917,plain,
( ~ isa(X1,c_tptpcol_13_92263)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_896,i_0_496,i_0_894,i_0_457,i_0_469,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316]) ).
cnf(i_0_918,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_919,plain,
( ~ isa(X1,c_tptpcol_14_92264)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_896,i_0_496,i_0_894,i_0_457,i_0_469,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321]) ).
cnf(i_0_920,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_921,plain,
( ~ tptpcol_14_92264(X1)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_896,i_0_496,i_0_894,i_0_457,i_0_469,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321,i_0_392]) ).
cnf(i_0_922,plain,
( isa(X1,c_tptpcol_14_92264)
| ~ tptpcol_14_92264(X1) ),
inference(rename_variables,[],[i_0_392]) ).
cnf(i_0_923,plain,
( ~ tptpcol_13_92263(X1)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_896,i_0_496,i_0_894,i_0_457,i_0_469,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321,i_0_392,i_0_393]) ).
cnf(i_0_924,plain,
( isa(X1,c_tptpcol_13_92263)
| ~ tptpcol_13_92263(X1) ),
inference(rename_variables,[],[i_0_393]) ).
cnf(i_0_926,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_14_92264),
inference(scs_inference,[],[i_0_913,i_0_328]) ).
cnf(i_0_927,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_928,plain,
genls(c_tptpcol_15_26925,c_tptpcol_12_26919),
inference(scs_inference,[],[i_0_913,i_0_471,i_0_623,i_0_328,i_0_326]) ).
cnf(i_0_929,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_930,plain,
disjointwith(c_tptpcol_15_92268,c_tptpcol_6_26627),
inference(scs_inference,[],[i_0_777,i_0_913,i_0_911,i_0_471,i_0_623,i_0_328,i_0_326,i_0_323]) ).
cnf(i_0_931,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_932,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_1_65536),
inference(scs_inference,[],[i_0_777,i_0_913,i_0_496,i_0_911,i_0_471,i_0_623,i_0_328,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_933,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_934,plain,
( ~ isa(X1,c_tptpcol_15_92268)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_777,i_0_913,i_0_496,i_0_911,i_0_471,i_0_623,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316]) ).
cnf(i_0_935,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_936,plain,
( ~ isa(X1,c_tptpcol_16_92269)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_777,i_0_913,i_0_496,i_0_911,i_0_471,i_0_623,i_0_455,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321]) ).
cnf(i_0_937,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_938,plain,
( ~ tptpcol_16_92269(X1)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_777,i_0_913,i_0_496,i_0_911,i_0_471,i_0_623,i_0_455,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321,i_0_390]) ).
cnf(i_0_939,plain,
( isa(X1,c_tptpcol_16_92269)
| ~ tptpcol_16_92269(X1) ),
inference(rename_variables,[],[i_0_390]) ).
cnf(i_0_940,plain,
( ~ tptpcol_15_92268(X1)
| ~ isa(X1,c_tptpcol_6_26627) ),
inference(scs_inference,[],[i_0_777,i_0_913,i_0_496,i_0_911,i_0_471,i_0_623,i_0_455,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_321,i_0_390,i_0_391]) ).
cnf(i_0_941,plain,
( isa(X1,c_tptpcol_15_92268)
| ~ tptpcol_15_92268(X1) ),
inference(rename_variables,[],[i_0_391]) ).
cnf(i_0_943,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_12_92262),
inference(scs_inference,[],[i_0_879,i_0_328]) ).
cnf(i_0_944,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_945,plain,
genls(c_tptpcol_15_26925,c_tptpcol_10_26886),
inference(scs_inference,[],[i_0_879,i_0_928,i_0_641,i_0_328,i_0_326]) ).
cnf(i_0_946,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_947,plain,
disjointwith(c_tptpcol_16_92269,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323]) ).
cnf(i_0_948,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_949,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_12_26919),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_950,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_951,plain,
( isa(X1,c_tptpcol_12_26919)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322,i_0_321]) ).
cnf(i_0_952,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_953,plain,
( ~ isa(X1,c_tptpcol_15_26925)
| isa(X1,c_tptpcol_11_26887) ),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322,i_0_321,i_0_649]) ).
cnf(i_0_954,plain,
( ~ isa(X1,c_tptpcol_12_26919)
| isa(X1,c_tptpcol_11_26887) ),
inference(rename_variables,[],[i_0_649]) ).
cnf(i_0_955,plain,
( tptpcol_11_26887(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322,i_0_321,i_0_649,i_0_651]) ).
cnf(i_0_956,plain,
( ~ isa(X1,c_tptpcol_12_26919)
| tptpcol_11_26887(X1) ),
inference(rename_variables,[],[i_0_651]) ).
cnf(i_0_957,plain,
( tptpcol_10_26886(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322,i_0_321,i_0_649,i_0_651,i_0_653]) ).
cnf(i_0_958,plain,
( ~ isa(X1,c_tptpcol_12_26919)
| tptpcol_10_26886(X1) ),
inference(rename_variables,[],[i_0_653]) ).
cnf(i_0_959,plain,
( tptpcol_9_26885(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322,i_0_321,i_0_649,i_0_651,i_0_653,i_0_655]) ).
cnf(i_0_960,plain,
( ~ isa(X1,c_tptpcol_12_26919)
| tptpcol_9_26885(X1) ),
inference(rename_variables,[],[i_0_655]) ).
cnf(i_0_961,plain,
( tptpcol_8_26629(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322,i_0_321,i_0_649,i_0_651,i_0_653,i_0_655,i_0_657]) ).
cnf(i_0_962,plain,
( ~ isa(X1,c_tptpcol_12_26919)
| tptpcol_8_26629(X1) ),
inference(rename_variables,[],[i_0_657]) ).
cnf(i_0_963,plain,
( tptpcol_7_26628(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322,i_0_321,i_0_649,i_0_651,i_0_653,i_0_655,i_0_657,i_0_659]) ).
cnf(i_0_964,plain,
( ~ isa(X1,c_tptpcol_12_26919)
| tptpcol_7_26628(X1) ),
inference(rename_variables,[],[i_0_659]) ).
cnf(i_0_965,plain,
( tptpcol_6_26627(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322,i_0_321,i_0_649,i_0_651,i_0_653,i_0_655,i_0_657,i_0_659,i_0_661]) ).
cnf(i_0_966,plain,
( ~ isa(X1,c_tptpcol_12_26919)
| tptpcol_6_26627(X1) ),
inference(rename_variables,[],[i_0_661]) ).
cnf(i_0_967,plain,
( tptpcol_5_24579(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322,i_0_321,i_0_649,i_0_651,i_0_653,i_0_655,i_0_657,i_0_659,i_0_661,i_0_663]) ).
cnf(i_0_968,plain,
( ~ isa(X1,c_tptpcol_12_26919)
| tptpcol_5_24579(X1) ),
inference(rename_variables,[],[i_0_663]) ).
cnf(i_0_969,plain,
( tptpcol_4_24578(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322,i_0_321,i_0_649,i_0_651,i_0_653,i_0_655,i_0_657,i_0_659,i_0_661,i_0_663,i_0_665]) ).
cnf(i_0_970,plain,
( ~ isa(X1,c_tptpcol_12_26919)
| tptpcol_4_24578(X1) ),
inference(rename_variables,[],[i_0_665]) ).
cnf(i_0_971,plain,
( tptpcol_3_16386(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322,i_0_321,i_0_649,i_0_651,i_0_653,i_0_655,i_0_657,i_0_659,i_0_661,i_0_663,i_0_665,i_0_667]) ).
cnf(i_0_972,plain,
( ~ isa(X1,c_tptpcol_12_26919)
| tptpcol_3_16386(X1) ),
inference(rename_variables,[],[i_0_667]) ).
cnf(i_0_973,plain,
( tptpcol_2_2(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322,i_0_321,i_0_649,i_0_651,i_0_653,i_0_655,i_0_657,i_0_659,i_0_661,i_0_663,i_0_665,i_0_667,i_0_669]) ).
cnf(i_0_974,plain,
( ~ isa(X1,c_tptpcol_12_26919)
| tptpcol_2_2(X1) ),
inference(rename_variables,[],[i_0_669]) ).
cnf(i_0_975,plain,
( tptpcol_12_26919(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322,i_0_321,i_0_649,i_0_651,i_0_653,i_0_655,i_0_657,i_0_659,i_0_661,i_0_663,i_0_665,i_0_667,i_0_669,i_0_370]) ).
cnf(i_0_976,plain,
( ~ isa(X1,c_tptpcol_12_26919)
| tptpcol_12_26919(X1) ),
inference(rename_variables,[],[i_0_370]) ).
cnf(i_0_977,plain,
( tptpcol_1_1(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_847,i_0_879,i_0_913,i_0_928,i_0_502,i_0_641,i_0_328,i_0_326,i_0_323,i_0_322,i_0_321,i_0_649,i_0_651,i_0_653,i_0_655,i_0_657,i_0_659,i_0_661,i_0_663,i_0_665,i_0_667,i_0_669,i_0_370,i_0_452]) ).
cnf(i_0_978,plain,
( ~ tptpcol_2_2(X1)
| tptpcol_1_1(X1) ),
inference(rename_variables,[],[i_0_452]) ).
cnf(i_0_980,plain,
disjointwith(c_tptpcol_12_26919,c_tptpcol_1_65536),
inference(scs_inference,[],[i_0_949,i_0_328]) ).
cnf(i_0_981,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_982,plain,
genls(c_tptpcol_15_26925,c_tptpcol_9_26885),
inference(scs_inference,[],[i_0_949,i_0_945,i_0_476,i_0_328,i_0_326]) ).
cnf(i_0_983,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_984,plain,
disjointwith(c_tptpcol_9_92165,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_949,i_0_627,i_0_945,i_0_462,i_0_476,i_0_328,i_0_326,i_0_323]) ).
cnf(i_0_985,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_986,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_15_26925),
inference(scs_inference,[],[i_0_847,i_0_949,i_0_627,i_0_945,i_0_462,i_0_476,i_0_328,i_0_326,i_0_323,i_0_322]) ).
cnf(i_0_987,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_988,plain,
( ~ isa(X1,c_tptpcol_9_92165)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_847,i_0_949,i_0_627,i_0_945,i_0_462,i_0_476,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316]) ).
cnf(i_0_989,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_990,plain,
( ~ tptpcol_9_92165(X1)
| ~ isa(X1,c_tptpcol_1_1) ),
inference(scs_inference,[],[i_0_847,i_0_949,i_0_627,i_0_945,i_0_462,i_0_476,i_0_328,i_0_326,i_0_323,i_0_322,i_0_316,i_0_397]) ).
cnf(i_0_991,plain,
( isa(X1,c_tptpcol_9_92165)
| ~ tptpcol_9_92165(X1) ),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_993,plain,
disjointwith(c_tptpcol_15_26925,c_tptpcol_1_65536),
inference(scs_inference,[],[i_0_986,i_0_328]) ).
cnf(i_0_994,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_995,plain,
genls(c_tptpcol_15_26925,c_tptpcol_8_26629),
inference(scs_inference,[],[i_0_986,i_0_982,i_0_477,i_0_328,i_0_326]) ).
cnf(i_0_996,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_997,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_13_26920),
inference(scs_inference,[],[i_0_949,i_0_986,i_0_982,i_0_473,i_0_477,i_0_328,i_0_326,i_0_322]) ).
cnf(i_0_998,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_999,plain,
~ disjointwith(c_tptpcol_9_26885,c_tptpcol_16_92269),
inference(scs_inference,[],[i_0_949,i_0_986,i_0_588,i_0_982,i_0_473,i_0_477,i_0_328,i_0_326,i_0_322,i_0_323]) ).
cnf(i_0_1000,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_1001,plain,
( ~ isa(X1,c_tptpcol_1_65536)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_949,i_0_986,i_0_588,i_0_982,i_0_473,i_0_477,i_0_328,i_0_326,i_0_322,i_0_323,i_0_316]) ).
cnf(i_0_1002,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_1003,plain,
( ~ isa(X1,c_tptpcol_15_92268)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_949,i_0_986,i_0_588,i_0_982,i_0_473,i_0_477,i_0_911,i_0_328,i_0_326,i_0_322,i_0_323,i_0_316,i_0_321]) ).
cnf(i_0_1004,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_1005,plain,
( ~ tptpcol_15_92268(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_949,i_0_986,i_0_588,i_0_982,i_0_473,i_0_477,i_0_911,i_0_328,i_0_326,i_0_322,i_0_323,i_0_316,i_0_321,i_0_391]) ).
cnf(i_0_1006,plain,
( isa(X1,c_tptpcol_15_92268)
| ~ tptpcol_15_92268(X1) ),
inference(rename_variables,[],[i_0_391]) ).
cnf(i_0_1007,plain,
( ~ tptpcol_1_65536(X1)
| ~ isa(X1,c_tptpcol_15_26925) ),
inference(scs_inference,[],[i_0_949,i_0_986,i_0_588,i_0_982,i_0_473,i_0_477,i_0_911,i_0_328,i_0_326,i_0_322,i_0_323,i_0_316,i_0_321,i_0_391,i_0_404]) ).
cnf(i_0_1008,plain,
( isa(X1,c_tptpcol_1_65536)
| ~ tptpcol_1_65536(X1) ),
inference(rename_variables,[],[i_0_404]) ).
cnf(i_0_1010,plain,
disjointwith(c_tptpcol_13_26920,c_tptpcol_1_65536),
inference(scs_inference,[],[i_0_997,i_0_328]) ).
cnf(i_0_1011,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_1012,plain,
genls(c_tptpcol_15_26925,c_tptpcol_7_26628),
inference(scs_inference,[],[i_0_997,i_0_995,i_0_478,i_0_328,i_0_326]) ).
cnf(i_0_1013,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_1014,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_14_26921),
inference(scs_inference,[],[i_0_997,i_0_995,i_0_472,i_0_478,i_0_328,i_0_326,i_0_322]) ).
cnf(i_0_1015,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_1016,plain,
disjointwith(c_tptpcol_7_92163,c_tptpcol_1_1),
inference(scs_inference,[],[i_0_997,i_0_572,i_0_995,i_0_464,i_0_472,i_0_478,i_0_328,i_0_326,i_0_322,i_0_323]) ).
cnf(i_0_1017,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_1018,plain,
( ~ isa(X1,c_tptpcol_1_65536)
| ~ isa(X1,c_tptpcol_13_26920) ),
inference(scs_inference,[],[i_0_997,i_0_572,i_0_995,i_0_464,i_0_472,i_0_478,i_0_328,i_0_326,i_0_322,i_0_323,i_0_316]) ).
cnf(i_0_1019,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_1020,plain,
( ~ isa(X1,c_tptpcol_15_92268)
| ~ isa(X1,c_tptpcol_13_26920) ),
inference(scs_inference,[],[i_0_997,i_0_572,i_0_995,i_0_464,i_0_472,i_0_478,i_0_911,i_0_328,i_0_326,i_0_322,i_0_323,i_0_316,i_0_321]) ).
cnf(i_0_1021,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_1022,plain,
( ~ tptpcol_15_92268(X1)
| ~ isa(X1,c_tptpcol_13_26920) ),
inference(scs_inference,[],[i_0_997,i_0_572,i_0_995,i_0_464,i_0_472,i_0_478,i_0_911,i_0_328,i_0_326,i_0_322,i_0_323,i_0_316,i_0_321,i_0_391]) ).
cnf(i_0_1023,plain,
( isa(X1,c_tptpcol_15_92268)
| ~ tptpcol_15_92268(X1) ),
inference(rename_variables,[],[i_0_391]) ).
cnf(i_0_1024,plain,
( ~ tptpcol_1_65536(X1)
| ~ isa(X1,c_tptpcol_13_26920) ),
inference(scs_inference,[],[i_0_997,i_0_572,i_0_995,i_0_464,i_0_472,i_0_478,i_0_911,i_0_328,i_0_326,i_0_322,i_0_323,i_0_316,i_0_321,i_0_391,i_0_404]) ).
cnf(i_0_1025,plain,
( isa(X1,c_tptpcol_1_65536)
| ~ tptpcol_1_65536(X1) ),
inference(rename_variables,[],[i_0_404]) ).
cnf(i_0_1027,plain,
disjointwith(c_tptpcol_14_26921,c_tptpcol_1_65536),
inference(scs_inference,[],[i_0_1014,i_0_328]) ).
cnf(i_0_1028,plain,
( ~ disjointwith(X1,X2)
| disjointwith(X2,X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_1029,plain,
genls(c_tptpcol_15_26925,c_tptpcol_6_26627),
inference(scs_inference,[],[i_0_1014,i_0_1012,i_0_479,i_0_328,i_0_326]) ).
cnf(i_0_1030,plain,
( ~ genls(X1,X2)
| genls(X1,X3)
| ~ genls(X2,X3) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_1031,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_16_26926),
inference(scs_inference,[],[i_0_1014,i_0_1012,i_0_584,i_0_479,i_0_328,i_0_326,i_0_322]) ).
cnf(i_0_1032,plain,
( ~ genls(X1,X2)
| disjointwith(X3,X1)
| ~ disjointwith(X3,X2) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_1033,plain,
~ disjointwith(c_tptpcol_7_26628,c_tptpcol_16_92269),
inference(scs_inference,[],[i_0_1014,i_0_588,i_0_1012,i_0_584,i_0_479,i_0_328,i_0_326,i_0_322,i_0_323]) ).
cnf(i_0_1034,plain,
( ~ genls(X1,X2)
| disjointwith(X1,X3)
| ~ disjointwith(X2,X3) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_1035,plain,
( ~ isa(X1,c_tptpcol_1_65536)
| ~ isa(X1,c_tptpcol_14_26921) ),
inference(scs_inference,[],[i_0_1014,i_0_588,i_0_1012,i_0_584,i_0_479,i_0_328,i_0_326,i_0_322,i_0_323,i_0_316]) ).
cnf(i_0_1036,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X3,X1)
| ~ isa(X3,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_1037,plain,
( ~ isa(X1,c_tptpcol_15_92268)
| ~ isa(X1,c_tptpcol_14_26921) ),
inference(scs_inference,[],[i_0_1014,i_0_588,i_0_1012,i_0_584,i_0_479,i_0_911,i_0_328,i_0_326,i_0_322,i_0_323,i_0_316,i_0_321]) ).
cnf(i_0_1038,plain,
( ~ genls(X1,X2)
| isa(X3,X2)
| ~ isa(X3,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_1039,plain,
( ~ tptpcol_15_92268(X1)
| ~ isa(X1,c_tptpcol_14_26921) ),
inference(scs_inference,[],[i_0_1014,i_0_588,i_0_1012,i_0_584,i_0_479,i_0_911,i_0_328,i_0_326,i_0_322,i_0_323,i_0_316,i_0_321,i_0_391]) ).
cnf(i_0_1040,plain,
( isa(X1,c_tptpcol_15_92268)
| ~ tptpcol_15_92268(X1) ),
inference(rename_variables,[],[i_0_391]) ).
cnf(i_0_1041,plain,
( ~ tptpcol_1_65536(X1)
| ~ isa(X1,c_tptpcol_14_26921) ),
inference(scs_inference,[],[i_0_1014,i_0_588,i_0_1012,i_0_584,i_0_479,i_0_911,i_0_328,i_0_326,i_0_322,i_0_323,i_0_316,i_0_321,i_0_391,i_0_404]) ).
cnf(i_0_1042,plain,
( isa(X1,c_tptpcol_1_65536)
| ~ tptpcol_1_65536(X1) ),
inference(rename_variables,[],[i_0_404]) ).
cnf(i_0_1044,plain,
$false,
inference(scs_inference,[],[i_0_1031,i_0_932,i_0_328]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : CSR049+1 : TPTP v9.2.1. Released v3.4.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n027.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 16:34:50 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 1.18/1.61 % Version : CSE_E---1.7
% 1.18/1.61 % Problem : theBenchmark.p
% 1.18/1.61 % SZS status Theorem for theBenchmark.p
% 1.18/1.61 % SZS output start CNFRefutation
% See solution above
% 1.89/2.35 % Total time : 1.273s
%------------------------------------------------------------------------------