%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : CSR049+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n006.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 : Wed Jul 27 12:49:07 EDT 2022
% Result : Theorem 2.07s 2.28s
% Output : Refutation 2.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 35
% Syntax : Number of clauses : 66 ( 63 unt; 0 nHn; 66 RR)
% Number of literals : 72 ( 0 equ; 7 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 32 con; 0-0 aty)
% Number of variables : 9 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(45,axiom,
( ~ disjointwith(A,B)
| ~ genls(C,B)
| disjointwith(A,C) ),
file('CSR049+1.p',unknown),
[] ).
cnf(46,axiom,
( ~ disjointwith(A,B)
| ~ genls(C,A)
| disjointwith(C,B) ),
file('CSR049+1.p',unknown),
[] ).
cnf(113,axiom,
( ~ genls(A,B)
| ~ genls(B,C)
| genls(A,C) ),
file('CSR049+1.p',unknown),
[] ).
cnf(125,axiom,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),
file('CSR049+1.p',unknown),
[] ).
cnf(132,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('CSR049+1.p',unknown),
[] ).
cnf(133,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('CSR049+1.p',unknown),
[] ).
cnf(134,axiom,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
file('CSR049+1.p',unknown),
[] ).
cnf(135,axiom,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
file('CSR049+1.p',unknown),
[] ).
cnf(136,axiom,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
file('CSR049+1.p',unknown),
[] ).
cnf(137,axiom,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
file('CSR049+1.p',unknown),
[] ).
cnf(138,axiom,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
file('CSR049+1.p',unknown),
[] ).
cnf(139,axiom,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
file('CSR049+1.p',unknown),
[] ).
cnf(140,axiom,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
file('CSR049+1.p',unknown),
[] ).
cnf(141,axiom,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
file('CSR049+1.p',unknown),
[] ).
cnf(142,axiom,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
file('CSR049+1.p',unknown),
[] ).
cnf(143,axiom,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
file('CSR049+1.p',unknown),
[] ).
cnf(144,axiom,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
file('CSR049+1.p',unknown),
[] ).
cnf(145,axiom,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
file('CSR049+1.p',unknown),
[] ).
cnf(146,axiom,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
file('CSR049+1.p',unknown),
[] ).
cnf(147,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('CSR049+1.p',unknown),
[] ).
cnf(148,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('CSR049+1.p',unknown),
[] ).
cnf(149,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('CSR049+1.p',unknown),
[] ).
cnf(150,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('CSR049+1.p',unknown),
[] ).
cnf(151,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('CSR049+1.p',unknown),
[] ).
cnf(152,axiom,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
file('CSR049+1.p',unknown),
[] ).
cnf(153,axiom,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
file('CSR049+1.p',unknown),
[] ).
cnf(154,axiom,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
file('CSR049+1.p',unknown),
[] ).
cnf(155,axiom,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
file('CSR049+1.p',unknown),
[] ).
cnf(156,axiom,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
file('CSR049+1.p',unknown),
[] ).
cnf(157,axiom,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
file('CSR049+1.p',unknown),
[] ).
cnf(158,axiom,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
file('CSR049+1.p',unknown),
[] ).
cnf(159,axiom,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
file('CSR049+1.p',unknown),
[] ).
cnf(160,axiom,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
file('CSR049+1.p',unknown),
[] ).
cnf(161,axiom,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
file('CSR049+1.p',unknown),
[] ).
cnf(162,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('CSR049+1.p',unknown),
[] ).
cnf(193,plain,
genls(c_tptpcol_4_24578,c_tptpcol_2_2),
inference(hyper,[status(thm)],[134,113,133]),
[iquote('hyper,134,113,133')] ).
cnf(199,plain,
genls(c_tptpcol_6_26627,c_tptpcol_4_24578),
inference(hyper,[status(thm)],[136,113,135]),
[iquote('hyper,136,113,135')] ).
cnf(204,plain,
genls(c_tptpcol_8_26629,c_tptpcol_6_26627),
inference(hyper,[status(thm)],[138,113,137]),
[iquote('hyper,138,113,137')] ).
cnf(211,plain,
genls(c_tptpcol_10_26886,c_tptpcol_8_26629),
inference(hyper,[status(thm)],[140,113,139]),
[iquote('hyper,140,113,139')] ).
cnf(217,plain,
genls(c_tptpcol_12_26919,c_tptpcol_10_26886),
inference(hyper,[status(thm)],[142,113,141]),
[iquote('hyper,142,113,141')] ).
cnf(223,plain,
genls(c_tptpcol_14_26921,c_tptpcol_12_26919),
inference(hyper,[status(thm)],[144,113,143]),
[iquote('hyper,144,113,143')] ).
cnf(229,plain,
genls(c_tptpcol_16_26926,c_tptpcol_14_26921),
inference(hyper,[status(thm)],[146,113,145]),
[iquote('hyper,146,113,145')] ).
cnf(234,plain,
genls(c_tptpcol_3_81921,c_tptpcol_1_65536),
inference(hyper,[status(thm)],[148,113,147]),
[iquote('hyper,148,113,147')] ).
cnf(241,plain,
genls(c_tptpcol_5_90114,c_tptpcol_3_81921),
inference(hyper,[status(thm)],[150,113,149]),
[iquote('hyper,150,113,149')] ).
cnf(248,plain,
genls(c_tptpcol_7_92163,c_tptpcol_5_90114),
inference(hyper,[status(thm)],[152,113,151]),
[iquote('hyper,152,113,151')] ).
cnf(254,plain,
genls(c_tptpcol_9_92165,c_tptpcol_7_92163),
inference(hyper,[status(thm)],[154,113,153]),
[iquote('hyper,154,113,153')] ).
cnf(260,plain,
genls(c_tptpcol_11_92230,c_tptpcol_9_92165),
inference(hyper,[status(thm)],[156,113,155]),
[iquote('hyper,156,113,155')] ).
cnf(266,plain,
genls(c_tptpcol_13_92263,c_tptpcol_11_92230),
inference(hyper,[status(thm)],[158,113,157]),
[iquote('hyper,158,113,157')] ).
cnf(271,plain,
genls(c_tptpcol_15_92268,c_tptpcol_13_92263),
inference(hyper,[status(thm)],[160,113,159]),
[iquote('hyper,160,113,159')] ).
cnf(278,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536),
inference(hyper,[status(thm)],[162,46,132]),
[iquote('hyper,162,46,132')] ).
cnf(299,plain,
genls(c_tptpcol_8_26629,c_tptpcol_4_24578),
inference(hyper,[status(thm)],[204,113,199]),
[iquote('hyper,204,113,199')] ).
cnf(307,plain,
genls(c_tptpcol_12_26919,c_tptpcol_8_26629),
inference(hyper,[status(thm)],[217,113,211]),
[iquote('hyper,217,113,211')] ).
cnf(314,plain,
genls(c_tptpcol_16_26926,c_tptpcol_12_26919),
inference(hyper,[status(thm)],[229,113,223]),
[iquote('hyper,229,113,223')] ).
cnf(319,plain,
genls(c_tptpcol_5_90114,c_tptpcol_1_65536),
inference(hyper,[status(thm)],[241,113,234]),
[iquote('hyper,241,113,234')] ).
cnf(327,plain,
genls(c_tptpcol_9_92165,c_tptpcol_5_90114),
inference(hyper,[status(thm)],[254,113,248]),
[iquote('hyper,254,113,248')] ).
cnf(335,plain,
genls(c_tptpcol_13_92263,c_tptpcol_9_92165),
inference(hyper,[status(thm)],[266,113,260]),
[iquote('hyper,266,113,260')] ).
cnf(338,plain,
genls(c_tptpcol_16_92269,c_tptpcol_13_92263),
inference(hyper,[status(thm)],[271,113,161]),
[iquote('hyper,271,113,161')] ).
cnf(341,plain,
disjointwith(c_tptpcol_4_24578,c_tptpcol_1_65536),
inference(hyper,[status(thm)],[278,46,193]),
[iquote('hyper,278,46,193')] ).
cnf(396,plain,
genls(c_tptpcol_16_26926,c_tptpcol_8_26629),
inference(hyper,[status(thm)],[314,113,307]),
[iquote('hyper,314,113,307')] ).
cnf(423,plain,
genls(c_tptpcol_9_92165,c_tptpcol_1_65536),
inference(hyper,[status(thm)],[327,113,319]),
[iquote('hyper,327,113,319')] ).
cnf(443,plain,
genls(c_tptpcol_16_92269,c_tptpcol_9_92165),
inference(hyper,[status(thm)],[338,113,335]),
[iquote('hyper,338,113,335')] ).
cnf(446,plain,
disjointwith(c_tptpcol_8_26629,c_tptpcol_1_65536),
inference(hyper,[status(thm)],[341,46,299]),
[iquote('hyper,341,46,299')] ).
cnf(652,plain,
genls(c_tptpcol_16_92269,c_tptpcol_1_65536),
inference(hyper,[status(thm)],[443,113,423]),
[iquote('hyper,443,113,423')] ).
cnf(654,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_1_65536),
inference(hyper,[status(thm)],[446,46,396]),
[iquote('hyper,446,46,396')] ).
cnf(970,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),
inference(hyper,[status(thm)],[654,45,652]),
[iquote('hyper,654,45,652')] ).
cnf(971,plain,
$false,
inference(binary,[status(thm)],[970,125]),
[iquote('binary,970.1,125.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : CSR049+1 : TPTP v8.1.0. Released v3.4.0.
% 0.10/0.12 % Command : otter-tptp-script %s
% 0.12/0.33 % Computer : n006.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Jul 27 04:12:47 EDT 2022
% 0.12/0.33 % CPUTime :
% 2.07/2.25 ----- Otter 3.3f, August 2004 -----
% 2.07/2.25 The process was started by sandbox2 on n006.cluster.edu,
% 2.07/2.25 Wed Jul 27 04:12:47 2022
% 2.07/2.25 The command was "./otter". The process ID is 14770.
% 2.07/2.25
% 2.07/2.25 set(prolog_style_variables).
% 2.07/2.25 set(auto).
% 2.07/2.25 dependent: set(auto1).
% 2.07/2.25 dependent: set(process_input).
% 2.07/2.25 dependent: clear(print_kept).
% 2.07/2.25 dependent: clear(print_new_demod).
% 2.07/2.25 dependent: clear(print_back_demod).
% 2.07/2.25 dependent: clear(print_back_sub).
% 2.07/2.25 dependent: set(control_memory).
% 2.07/2.25 dependent: assign(max_mem, 12000).
% 2.07/2.25 dependent: assign(pick_given_ratio, 4).
% 2.07/2.25 dependent: assign(stats_level, 1).
% 2.07/2.25 dependent: assign(max_seconds, 10800).
% 2.07/2.25 clear(print_given).
% 2.07/2.25
% 2.07/2.25 formula_list(usable).
% 2.07/2.25 genlmt(c_gregoriancalendarmt,c_basekb).
% 2.07/2.25 genlmt(c_unitedstatesgeographypeoplemt,c_peopledatamt).
% 2.07/2.25 genlmt(c_unitedstatessociallifemt,c_gregoriancalendarmt).
% 2.07/2.25 transitivebinarypredicate(c_genlmt).
% 2.07/2.25 genlmt(c_basekb,c_universalvocabularymt).
% 2.07/2.25 genlmt(c_peopledatamt,c_unitedstatessociallifemt).
% 2.07/2.25 genls(c_tptpcol_2_2,c_tptpcol_1_1).
% 2.07/2.25 all OBJ (tptpcol_2_2(OBJ)->tptpcol_1_1(OBJ)).
% 2.07/2.25 genls(c_tptpcol_3_16386,c_tptpcol_2_2).
% 2.07/2.25 all OBJ (tptpcol_3_16386(OBJ)->tptpcol_2_2(OBJ)).
% 2.07/2.25 genls(c_tptpcol_4_24578,c_tptpcol_3_16386).
% 2.07/2.25 all OBJ (tptpcol_4_24578(OBJ)->tptpcol_3_16386(OBJ)).
% 2.07/2.25 genls(c_tptpcol_5_24579,c_tptpcol_4_24578).
% 2.07/2.25 all OBJ (tptpcol_5_24579(OBJ)->tptpcol_4_24578(OBJ)).
% 2.07/2.25 genls(c_tptpcol_6_26627,c_tptpcol_5_24579).
% 2.07/2.25 all OBJ (tptpcol_6_26627(OBJ)->tptpcol_5_24579(OBJ)).
% 2.07/2.25 genls(c_tptpcol_7_26628,c_tptpcol_6_26627).
% 2.07/2.25 all OBJ (tptpcol_7_26628(OBJ)->tptpcol_6_26627(OBJ)).
% 2.07/2.25 genls(c_tptpcol_8_26629,c_tptpcol_7_26628).
% 2.07/2.25 all OBJ (tptpcol_8_26629(OBJ)->tptpcol_7_26628(OBJ)).
% 2.07/2.25 genls(c_tptpcol_9_26885,c_tptpcol_8_26629).
% 2.07/2.25 all OBJ (tptpcol_9_26885(OBJ)->tptpcol_8_26629(OBJ)).
% 2.07/2.25 genls(c_tptpcol_10_26886,c_tptpcol_9_26885).
% 2.07/2.25 all OBJ (tptpcol_10_26886(OBJ)->tptpcol_9_26885(OBJ)).
% 2.07/2.25 genls(c_tptpcol_11_26887,c_tptpcol_10_26886).
% 2.07/2.25 all OBJ (tptpcol_11_26887(OBJ)->tptpcol_10_26886(OBJ)).
% 2.07/2.25 genls(c_tptpcol_12_26919,c_tptpcol_11_26887).
% 2.07/2.25 all OBJ (tptpcol_12_26919(OBJ)->tptpcol_11_26887(OBJ)).
% 2.07/2.25 genls(c_tptpcol_13_26920,c_tptpcol_12_26919).
% 2.07/2.25 all OBJ (tptpcol_13_26920(OBJ)->tptpcol_12_26919(OBJ)).
% 2.07/2.25 genls(c_tptpcol_14_26921,c_tptpcol_13_26920).
% 2.07/2.25 all OBJ (tptpcol_14_26921(OBJ)->tptpcol_13_26920(OBJ)).
% 2.07/2.25 genls(c_tptpcol_15_26925,c_tptpcol_14_26921).
% 2.07/2.25 all OBJ (tptpcol_15_26925(OBJ)->tptpcol_14_26921(OBJ)).
% 2.07/2.25 genls(c_tptpcol_16_26926,c_tptpcol_15_26925).
% 2.07/2.25 all OBJ (tptpcol_16_26926(OBJ)->tptpcol_15_26925(OBJ)).
% 2.07/2.25 genls(c_tptpcol_2_65537,c_tptpcol_1_65536).
% 2.07/2.25 all OBJ (tptpcol_2_65537(OBJ)->tptpcol_1_65536(OBJ)).
% 2.07/2.25 genls(c_tptpcol_3_81921,c_tptpcol_2_65537).
% 2.07/2.25 all OBJ (tptpcol_3_81921(OBJ)->tptpcol_2_65537(OBJ)).
% 2.07/2.25 genls(c_tptpcol_4_90113,c_tptpcol_3_81921).
% 2.07/2.25 all OBJ (tptpcol_4_90113(OBJ)->tptpcol_3_81921(OBJ)).
% 2.07/2.25 genls(c_tptpcol_5_90114,c_tptpcol_4_90113).
% 2.07/2.25 all OBJ (tptpcol_5_90114(OBJ)->tptpcol_4_90113(OBJ)).
% 2.07/2.25 genls(c_tptpcol_6_92162,c_tptpcol_5_90114).
% 2.07/2.25 all OBJ (tptpcol_6_92162(OBJ)->tptpcol_5_90114(OBJ)).
% 2.07/2.25 genls(c_tptpcol_7_92163,c_tptpcol_6_92162).
% 2.07/2.25 all OBJ (tptpcol_7_92163(OBJ)->tptpcol_6_92162(OBJ)).
% 2.07/2.25 genls(c_tptpcol_8_92164,c_tptpcol_7_92163).
% 2.07/2.25 all OBJ (tptpcol_8_92164(OBJ)->tptpcol_7_92163(OBJ)).
% 2.07/2.25 genls(c_tptpcol_9_92165,c_tptpcol_8_92164).
% 2.07/2.25 all OBJ (tptpcol_9_92165(OBJ)->tptpcol_8_92164(OBJ)).
% 2.07/2.25 genls(c_tptpcol_10_92166,c_tptpcol_9_92165).
% 2.07/2.25 all OBJ (tptpcol_10_92166(OBJ)->tptpcol_9_92165(OBJ)).
% 2.07/2.25 genls(c_tptpcol_11_92230,c_tptpcol_10_92166).
% 2.07/2.25 all OBJ (tptpcol_11_92230(OBJ)->tptpcol_10_92166(OBJ)).
% 2.07/2.25 genls(c_tptpcol_12_92262,c_tptpcol_11_92230).
% 2.07/2.25 all OBJ (tptpcol_12_92262(OBJ)->tptpcol_11_92230(OBJ)).
% 2.07/2.25 genls(c_tptpcol_13_92263,c_tptpcol_12_92262).
% 2.07/2.25 all OBJ (tptpcol_13_92263(OBJ)->tptpcol_12_92262(OBJ)).
% 2.07/2.25 genls(c_tptpcol_14_92264,c_tptpcol_13_92263).
% 2.07/2.25 all OBJ (tptpcol_14_92264(OBJ)->tptpcol_13_92263(OBJ)).
% 2.07/2.25 genls(c_tptpcol_15_92268,c_tptpcol_14_92264).
% 2.07/2.25 all OBJ (tptpcol_15_92268(OBJ)->tptpcol_14_92264(OBJ)).
% 2.07/2.25 genls(c_tptpcol_16_92269,c_tptpcol_15_92268).
% 2.07/2.25 all OBJ (tptpcol_16_92269(OBJ)->tptpcol_15_92268(OBJ)).
% 2.07/2.25 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536).
% 2.07/2.25 all OBJ (-(tptpcol_1_1(OBJ)&tptpcol_1_65536(OBJ))).
% 2.07/2.25 all OBJ COL1 COL2 (-(isa(OBJ,COL1)&isa(OBJ,COL2)&disjointwith(COL1,COL2))).
% 2.07/2.25 all SPECPRED PRED GENLPRED (genlinverse(SPECPRED,PRED)&genlinverse(PRED,GENLPRED)->genlpreds(SPECPRED,GENLPRED)).
% 2.07/2.25 all ARG1 INS (genlpreds(ARG1,INS)->predicate(INS)).
% 2.07/2.25 all ARG1 INS (genlpreds(ARG1,INS)->predicate(INS)).
% 2.07/2.25 all INS ARG2 (genlpreds(INS,ARG2)->predicate(INS)).
% 2.07/2.25 all INS ARG2 (genlpreds(INS,ARG2)->predicate(INS)).
% 2.07/2.25 all X Y Z (genlpreds(X,Y)&genlpreds(Y,Z)->genlpreds(X,Z)).
% 2.07/2.25 all X (predicate(X)->genlpreds(X,X)).
% 2.07/2.25 all X (predicate(X)->genlpreds(X,X)).
% 2.07/2.25 all ARG1 INS (genlinverse(ARG1,INS)->binarypredicate(INS)).
% 2.07/2.25 all INS ARG2 (genlinverse(INS,ARG2)->binarypredicate(INS)).
% 2.07/2.25 all OLD ARG2 NEW (genlinverse(OLD,ARG2)&genlpreds(NEW,OLD)->genlinverse(NEW,ARG2)).
% 2.07/2.25 all ARG1 OLD NEW (genlinverse(ARG1,OLD)&genlpreds(OLD,NEW)->genlinverse(ARG1,NEW)).
% 2.07/2.25 all ARG1 INS (disjointwith(ARG1,INS)->collection(INS)).
% 2.07/2.25 all INS ARG2 (disjointwith(INS,ARG2)->collection(INS)).
% 2.07/2.25 all X Y (disjointwith(X,Y)->disjointwith(Y,X)).
% 2.07/2.25 all ARG1 OLD NEW (disjointwith(ARG1,OLD)&genls(NEW,OLD)->disjointwith(ARG1,NEW)).
% 2.07/2.25 all OLD ARG2 NEW (disjointwith(OLD,ARG2)&genls(NEW,OLD)->disjointwith(NEW,ARG2)).
% 2.07/2.25 all X (isa(X,c_tptpcol_16_92269)->tptpcol_16_92269(X)).
% 2.07/2.25 all X (tptpcol_16_92269(X)->isa(X,c_tptpcol_16_92269)).
% 2.07/2.25 all X (isa(X,c_tptpcol_15_92268)->tptpcol_15_92268(X)).
% 2.07/2.25 all X (tptpcol_15_92268(X)->isa(X,c_tptpcol_15_92268)).
% 2.07/2.25 all X (isa(X,c_tptpcol_14_92264)->tptpcol_14_92264(X)).
% 2.07/2.25 all X (tptpcol_14_92264(X)->isa(X,c_tptpcol_14_92264)).
% 2.07/2.25 all X (isa(X,c_tptpcol_13_92263)->tptpcol_13_92263(X)).
% 2.07/2.25 all X (tptpcol_13_92263(X)->isa(X,c_tptpcol_13_92263)).
% 2.07/2.25 all X (isa(X,c_tptpcol_12_92262)->tptpcol_12_92262(X)).
% 2.07/2.25 all X (tptpcol_12_92262(X)->isa(X,c_tptpcol_12_92262)).
% 2.07/2.25 all X (isa(X,c_tptpcol_11_92230)->tptpcol_11_92230(X)).
% 2.07/2.25 all X (tptpcol_11_92230(X)->isa(X,c_tptpcol_11_92230)).
% 2.07/2.25 all X (isa(X,c_tptpcol_10_92166)->tptpcol_10_92166(X)).
% 2.07/2.25 all X (tptpcol_10_92166(X)->isa(X,c_tptpcol_10_92166)).
% 2.07/2.25 all X (isa(X,c_tptpcol_9_92165)->tptpcol_9_92165(X)).
% 2.07/2.25 all X (tptpcol_9_92165(X)->isa(X,c_tptpcol_9_92165)).
% 2.07/2.25 all X (isa(X,c_tptpcol_8_92164)->tptpcol_8_92164(X)).
% 2.07/2.25 all X (tptpcol_8_92164(X)->isa(X,c_tptpcol_8_92164)).
% 2.07/2.25 all X (isa(X,c_tptpcol_7_92163)->tptpcol_7_92163(X)).
% 2.07/2.25 all X (tptpcol_7_92163(X)->isa(X,c_tptpcol_7_92163)).
% 2.07/2.25 all X (isa(X,c_tptpcol_6_92162)->tptpcol_6_92162(X)).
% 2.07/2.25 all X (tptpcol_6_92162(X)->isa(X,c_tptpcol_6_92162)).
% 2.07/2.25 all X (isa(X,c_tptpcol_5_90114)->tptpcol_5_90114(X)).
% 2.07/2.25 all X (tptpcol_5_90114(X)->isa(X,c_tptpcol_5_90114)).
% 2.07/2.25 all X (isa(X,c_tptpcol_4_90113)->tptpcol_4_90113(X)).
% 2.07/2.25 all X (tptpcol_4_90113(X)->isa(X,c_tptpcol_4_90113)).
% 2.07/2.25 all X (isa(X,c_tptpcol_3_81921)->tptpcol_3_81921(X)).
% 2.07/2.25 all X (tptpcol_3_81921(X)->isa(X,c_tptpcol_3_81921)).
% 2.07/2.25 all X (isa(X,c_tptpcol_1_65536)->tptpcol_1_65536(X)).
% 2.07/2.25 all X (tptpcol_1_65536(X)->isa(X,c_tptpcol_1_65536)).
% 2.07/2.25 all X (isa(X,c_tptpcol_2_65537)->tptpcol_2_65537(X)).
% 2.07/2.25 all X (tptpcol_2_65537(X)->isa(X,c_tptpcol_2_65537)).
% 2.07/2.25 all X (isa(X,c_tptpcol_16_26926)->tptpcol_16_26926(X)).
% 2.07/2.25 all X (tptpcol_16_26926(X)->isa(X,c_tptpcol_16_26926)).
% 2.07/2.25 all X (isa(X,c_tptpcol_15_26925)->tptpcol_15_26925(X)).
% 2.07/2.25 all X (tptpcol_15_26925(X)->isa(X,c_tptpcol_15_26925)).
% 2.07/2.25 all X (isa(X,c_tptpcol_14_26921)->tptpcol_14_26921(X)).
% 2.07/2.25 all X (tptpcol_14_26921(X)->isa(X,c_tptpcol_14_26921)).
% 2.07/2.25 all X (isa(X,c_tptpcol_13_26920)->tptpcol_13_26920(X)).
% 2.07/2.25 all X (tptpcol_13_26920(X)->isa(X,c_tptpcol_13_26920)).
% 2.07/2.25 all X (isa(X,c_tptpcol_12_26919)->tptpcol_12_26919(X)).
% 2.07/2.25 all X (tptpcol_12_26919(X)->isa(X,c_tptpcol_12_26919)).
% 2.07/2.25 all X (isa(X,c_tptpcol_11_26887)->tptpcol_11_26887(X)).
% 2.07/2.25 all X (tptpcol_11_26887(X)->isa(X,c_tptpcol_11_26887)).
% 2.07/2.25 all X (isa(X,c_tptpcol_10_26886)->tptpcol_10_26886(X)).
% 2.07/2.25 all X (tptpcol_10_26886(X)->isa(X,c_tptpcol_10_26886)).
% 2.07/2.25 all X (isa(X,c_tptpcol_9_26885)->tptpcol_9_26885(X)).
% 2.07/2.25 all X (tptpcol_9_26885(X)->isa(X,c_tptpcol_9_26885)).
% 2.07/2.25 all X (isa(X,c_tptpcol_8_26629)->tptpcol_8_26629(X)).
% 2.07/2.25 all X (tptpcol_8_26629(X)->isa(X,c_tptpcol_8_26629)).
% 2.07/2.25 all X (isa(X,c_tptpcol_7_26628)->tptpcol_7_26628(X)).
% 2.07/2.25 all X (tptpcol_7_26628(X)->isa(X,c_tptpcol_7_26628)).
% 2.07/2.25 all X (isa(X,c_tptpcol_6_26627)->tptpcol_6_26627(X)).
% 2.07/2.25 all X (tptpcol_6_26627(X)->isa(X,c_tptpcol_6_26627)).
% 2.07/2.25 all X (isa(X,c_tptpcol_5_24579)->tptpcol_5_24579(X)).
% 2.07/2.25 all X (tptpcol_5_24579(X)->isa(X,c_tptpcol_5_24579)).
% 2.07/2.25 all X (isa(X,c_tptpcol_4_24578)->tptpcol_4_24578(X)).
% 2.07/2.25 all X (tptpcol_4_24578(X)->isa(X,c_tptpcol_4_24578)).
% 2.07/2.25 all X (isa(X,c_tptpcol_3_16386)->tptpcol_3_16386(X)).
% 2.07/2.25 all X (tptpcol_3_16386(X)->isa(X,c_tptpcol_3_16386)).
% 2.07/2.25 all X (isa(X,c_tptpcol_1_1)->tptpcol_1_1(X)).
% 2.07/2.25 all X (tptpcol_1_1(X)->isa(X,c_tptpcol_1_1)).
% 2.07/2.25 all X (isa(X,c_tptpcol_2_2)->tptpcol_2_2(X)).
% 2.07/2.25 all X (tptpcol_2_2(X)->isa(X,c_tptpcol_2_2)).
% 2.07/2.25 all ARG1 INS (genls(ARG1,INS)->collection(INS)).
% 2.07/2.25 all ARG1 INS (genls(ARG1,INS)->collection(INS)).
% 2.07/2.25 all INS ARG2 (genls(INS,ARG2)->collection(INS)).
% 2.07/2.25 all INS ARG2 (genls(INS,ARG2)->collection(INS)).
% 2.07/2.25 all X Y Z (genls(X,Y)&genls(Y,Z)->genls(X,Z)).
% 2.07/2.25 all X (collection(X)->genls(X,X)).
% 2.07/2.25 all X (collection(X)->genls(X,X)).
% 2.07/2.25 all OLD ARG2 NEW (genls(OLD,ARG2)&genls(NEW,OLD)->genls(NEW,ARG2)).
% 2.07/2.25 all ARG1 OLD NEW (genls(ARG1,OLD)&genls(OLD,NEW)->genls(ARG1,NEW)).
% 2.07/2.25 all X (isa(X,c_transitivebinarypredicate)->transitivebinarypredicate(X)).
% 2.07/2.25 all X (transitivebinarypredicate(X)->isa(X,c_transitivebinarypredicate)).
% 2.07/2.25 all ARG1 INS (isa(ARG1,INS)->collection(INS)).
% 2.07/2.25 all ARG1 INS (isa(ARG1,INS)->collection(INS)).
% 2.07/2.25 all INS ARG2 (isa(INS,ARG2)->thing(INS)).
% 2.07/2.25 all INS ARG2 (isa(INS,ARG2)->thing(INS)).
% 2.07/2.25 all ARG1 OLD NEW (isa(ARG1,OLD)&genls(OLD,NEW)->isa(ARG1,NEW)).
% 2.07/2.25 mtvisible(c_universalvocabularymt).
% 2.07/2.25 all SPECMT GENLMT (mtvisible(SPECMT)&genlmt(SPECMT,GENLMT)->mtvisible(GENLMT)).
% 2.07/2.25 all ARG1 INS (genlmt(ARG1,INS)->microtheory(INS)).
% 2.07/2.25 all ARG1 INS (genlmt(ARG1,INS)->microtheory(INS)).
% 2.07/2.25 all INS ARG2 (genlmt(INS,ARG2)->microtheory(INS)).
% 2.07/2.25 all INS ARG2 (genlmt(INS,ARG2)->microtheory(INS)).
% 2.07/2.25 all X Y Z (genlmt(X,Y)&genlmt(Y,Z)->genlmt(X,Z)).
% 2.07/2.25 all X (microtheory(X)->genlmt(X,X)).
% 2.07/2.25 all X (microtheory(X)->genlmt(X,X)).
% 2.07/2.25 mtvisible(c_basekb).
% 2.07/2.25 -(mtvisible(c_unitedstatesgeographypeoplemt)->disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)).
% 2.07/2.25 end_of_list.
% 2.07/2.25
% 2.07/2.25 -------> usable clausifies to:
% 2.07/2.25
% 2.07/2.25 list(usable).
% 2.07/2.25 0 [] genlmt(c_gregoriancalendarmt,c_basekb).
% 2.07/2.25 0 [] genlmt(c_unitedstatesgeographypeoplemt,c_peopledatamt).
% 2.07/2.25 0 [] genlmt(c_unitedstatessociallifemt,c_gregoriancalendarmt).
% 2.07/2.25 0 [] transitivebinarypredicate(c_genlmt).
% 2.07/2.25 0 [] genlmt(c_basekb,c_universalvocabularymt).
% 2.07/2.25 0 [] genlmt(c_peopledatamt,c_unitedstatessociallifemt).
% 2.07/2.25 0 [] genls(c_tptpcol_2_2,c_tptpcol_1_1).
% 2.07/2.25 0 [] -tptpcol_2_2(OBJ)|tptpcol_1_1(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_3_16386,c_tptpcol_2_2).
% 2.07/2.25 0 [] -tptpcol_3_16386(OBJ)|tptpcol_2_2(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_4_24578,c_tptpcol_3_16386).
% 2.07/2.25 0 [] -tptpcol_4_24578(OBJ)|tptpcol_3_16386(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_5_24579,c_tptpcol_4_24578).
% 2.07/2.25 0 [] -tptpcol_5_24579(OBJ)|tptpcol_4_24578(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_6_26627,c_tptpcol_5_24579).
% 2.07/2.25 0 [] -tptpcol_6_26627(OBJ)|tptpcol_5_24579(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_7_26628,c_tptpcol_6_26627).
% 2.07/2.25 0 [] -tptpcol_7_26628(OBJ)|tptpcol_6_26627(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_8_26629,c_tptpcol_7_26628).
% 2.07/2.25 0 [] -tptpcol_8_26629(OBJ)|tptpcol_7_26628(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_9_26885,c_tptpcol_8_26629).
% 2.07/2.25 0 [] -tptpcol_9_26885(OBJ)|tptpcol_8_26629(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_10_26886,c_tptpcol_9_26885).
% 2.07/2.25 0 [] -tptpcol_10_26886(OBJ)|tptpcol_9_26885(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_11_26887,c_tptpcol_10_26886).
% 2.07/2.25 0 [] -tptpcol_11_26887(OBJ)|tptpcol_10_26886(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_12_26919,c_tptpcol_11_26887).
% 2.07/2.25 0 [] -tptpcol_12_26919(OBJ)|tptpcol_11_26887(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_13_26920,c_tptpcol_12_26919).
% 2.07/2.25 0 [] -tptpcol_13_26920(OBJ)|tptpcol_12_26919(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_14_26921,c_tptpcol_13_26920).
% 2.07/2.25 0 [] -tptpcol_14_26921(OBJ)|tptpcol_13_26920(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_15_26925,c_tptpcol_14_26921).
% 2.07/2.25 0 [] -tptpcol_15_26925(OBJ)|tptpcol_14_26921(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_16_26926,c_tptpcol_15_26925).
% 2.07/2.25 0 [] -tptpcol_16_26926(OBJ)|tptpcol_15_26925(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_2_65537,c_tptpcol_1_65536).
% 2.07/2.25 0 [] -tptpcol_2_65537(OBJ)|tptpcol_1_65536(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_3_81921,c_tptpcol_2_65537).
% 2.07/2.25 0 [] -tptpcol_3_81921(OBJ)|tptpcol_2_65537(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_4_90113,c_tptpcol_3_81921).
% 2.07/2.25 0 [] -tptpcol_4_90113(OBJ)|tptpcol_3_81921(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_5_90114,c_tptpcol_4_90113).
% 2.07/2.25 0 [] -tptpcol_5_90114(OBJ)|tptpcol_4_90113(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_6_92162,c_tptpcol_5_90114).
% 2.07/2.25 0 [] -tptpcol_6_92162(OBJ)|tptpcol_5_90114(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_7_92163,c_tptpcol_6_92162).
% 2.07/2.25 0 [] -tptpcol_7_92163(OBJ)|tptpcol_6_92162(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_8_92164,c_tptpcol_7_92163).
% 2.07/2.25 0 [] -tptpcol_8_92164(OBJ)|tptpcol_7_92163(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_9_92165,c_tptpcol_8_92164).
% 2.07/2.25 0 [] -tptpcol_9_92165(OBJ)|tptpcol_8_92164(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_10_92166,c_tptpcol_9_92165).
% 2.07/2.25 0 [] -tptpcol_10_92166(OBJ)|tptpcol_9_92165(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_11_92230,c_tptpcol_10_92166).
% 2.07/2.25 0 [] -tptpcol_11_92230(OBJ)|tptpcol_10_92166(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_12_92262,c_tptpcol_11_92230).
% 2.07/2.25 0 [] -tptpcol_12_92262(OBJ)|tptpcol_11_92230(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_13_92263,c_tptpcol_12_92262).
% 2.07/2.25 0 [] -tptpcol_13_92263(OBJ)|tptpcol_12_92262(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_14_92264,c_tptpcol_13_92263).
% 2.07/2.25 0 [] -tptpcol_14_92264(OBJ)|tptpcol_13_92263(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_15_92268,c_tptpcol_14_92264).
% 2.07/2.25 0 [] -tptpcol_15_92268(OBJ)|tptpcol_14_92264(OBJ).
% 2.07/2.25 0 [] genls(c_tptpcol_16_92269,c_tptpcol_15_92268).
% 2.07/2.25 0 [] -tptpcol_16_92269(OBJ)|tptpcol_15_92268(OBJ).
% 2.07/2.25 0 [] disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536).
% 2.07/2.25 0 [] -tptpcol_1_1(OBJ)| -tptpcol_1_65536(OBJ).
% 2.07/2.25 0 [] -isa(OBJ,COL1)| -isa(OBJ,COL2)| -disjointwith(COL1,COL2).
% 2.07/2.25 0 [] -genlinverse(SPECPRED,PRED)| -genlinverse(PRED,GENLPRED)|genlpreds(SPECPRED,GENLPRED).
% 2.07/2.25 0 [] -genlpreds(ARG1,INS)|predicate(INS).
% 2.07/2.25 0 [] -genlpreds(ARG1,INS)|predicate(INS).
% 2.07/2.25 0 [] -genlpreds(INS,ARG2)|predicate(INS).
% 2.07/2.25 0 [] -genlpreds(INS,ARG2)|predicate(INS).
% 2.07/2.25 0 [] -genlpreds(X,Y)| -genlpreds(Y,Z)|genlpreds(X,Z).
% 2.07/2.25 0 [] -predicate(X)|genlpreds(X,X).
% 2.07/2.25 0 [] -predicate(X)|genlpreds(X,X).
% 2.07/2.25 0 [] -genlinverse(ARG1,INS)|binarypredicate(INS).
% 2.07/2.25 0 [] -genlinverse(INS,ARG2)|binarypredicate(INS).
% 2.07/2.25 0 [] -genlinverse(OLD,ARG2)| -genlpreds(NEW,OLD)|genlinverse(NEW,ARG2).
% 2.07/2.25 0 [] -genlinverse(ARG1,OLD)| -genlpreds(OLD,NEW)|genlinverse(ARG1,NEW).
% 2.07/2.25 0 [] -disjointwith(ARG1,INS)|collection(INS).
% 2.07/2.25 0 [] -disjointwith(INS,ARG2)|collection(INS).
% 2.07/2.25 0 [] -disjointwith(X,Y)|disjointwith(Y,X).
% 2.07/2.25 0 [] -disjointwith(ARG1,OLD)| -genls(NEW,OLD)|disjointwith(ARG1,NEW).
% 2.07/2.25 0 [] -disjointwith(OLD,ARG2)| -genls(NEW,OLD)|disjointwith(NEW,ARG2).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_16_92269)|tptpcol_16_92269(X).
% 2.07/2.25 0 [] -tptpcol_16_92269(X)|isa(X,c_tptpcol_16_92269).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_15_92268)|tptpcol_15_92268(X).
% 2.07/2.25 0 [] -tptpcol_15_92268(X)|isa(X,c_tptpcol_15_92268).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_14_92264)|tptpcol_14_92264(X).
% 2.07/2.25 0 [] -tptpcol_14_92264(X)|isa(X,c_tptpcol_14_92264).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_13_92263)|tptpcol_13_92263(X).
% 2.07/2.25 0 [] -tptpcol_13_92263(X)|isa(X,c_tptpcol_13_92263).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_12_92262)|tptpcol_12_92262(X).
% 2.07/2.25 0 [] -tptpcol_12_92262(X)|isa(X,c_tptpcol_12_92262).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_11_92230)|tptpcol_11_92230(X).
% 2.07/2.25 0 [] -tptpcol_11_92230(X)|isa(X,c_tptpcol_11_92230).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_10_92166)|tptpcol_10_92166(X).
% 2.07/2.25 0 [] -tptpcol_10_92166(X)|isa(X,c_tptpcol_10_92166).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_9_92165)|tptpcol_9_92165(X).
% 2.07/2.25 0 [] -tptpcol_9_92165(X)|isa(X,c_tptpcol_9_92165).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_8_92164)|tptpcol_8_92164(X).
% 2.07/2.25 0 [] -tptpcol_8_92164(X)|isa(X,c_tptpcol_8_92164).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_7_92163)|tptpcol_7_92163(X).
% 2.07/2.25 0 [] -tptpcol_7_92163(X)|isa(X,c_tptpcol_7_92163).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_6_92162)|tptpcol_6_92162(X).
% 2.07/2.25 0 [] -tptpcol_6_92162(X)|isa(X,c_tptpcol_6_92162).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_5_90114)|tptpcol_5_90114(X).
% 2.07/2.25 0 [] -tptpcol_5_90114(X)|isa(X,c_tptpcol_5_90114).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_4_90113)|tptpcol_4_90113(X).
% 2.07/2.25 0 [] -tptpcol_4_90113(X)|isa(X,c_tptpcol_4_90113).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_3_81921)|tptpcol_3_81921(X).
% 2.07/2.25 0 [] -tptpcol_3_81921(X)|isa(X,c_tptpcol_3_81921).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_1_65536)|tptpcol_1_65536(X).
% 2.07/2.25 0 [] -tptpcol_1_65536(X)|isa(X,c_tptpcol_1_65536).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_2_65537)|tptpcol_2_65537(X).
% 2.07/2.25 0 [] -tptpcol_2_65537(X)|isa(X,c_tptpcol_2_65537).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_16_26926)|tptpcol_16_26926(X).
% 2.07/2.25 0 [] -tptpcol_16_26926(X)|isa(X,c_tptpcol_16_26926).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_15_26925)|tptpcol_15_26925(X).
% 2.07/2.25 0 [] -tptpcol_15_26925(X)|isa(X,c_tptpcol_15_26925).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_14_26921)|tptpcol_14_26921(X).
% 2.07/2.25 0 [] -tptpcol_14_26921(X)|isa(X,c_tptpcol_14_26921).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_13_26920)|tptpcol_13_26920(X).
% 2.07/2.25 0 [] -tptpcol_13_26920(X)|isa(X,c_tptpcol_13_26920).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_12_26919)|tptpcol_12_26919(X).
% 2.07/2.25 0 [] -tptpcol_12_26919(X)|isa(X,c_tptpcol_12_26919).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_11_26887)|tptpcol_11_26887(X).
% 2.07/2.25 0 [] -tptpcol_11_26887(X)|isa(X,c_tptpcol_11_26887).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_10_26886)|tptpcol_10_26886(X).
% 2.07/2.25 0 [] -tptpcol_10_26886(X)|isa(X,c_tptpcol_10_26886).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_9_26885)|tptpcol_9_26885(X).
% 2.07/2.25 0 [] -tptpcol_9_26885(X)|isa(X,c_tptpcol_9_26885).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_8_26629)|tptpcol_8_26629(X).
% 2.07/2.25 0 [] -tptpcol_8_26629(X)|isa(X,c_tptpcol_8_26629).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_7_26628)|tptpcol_7_26628(X).
% 2.07/2.25 0 [] -tptpcol_7_26628(X)|isa(X,c_tptpcol_7_26628).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_6_26627)|tptpcol_6_26627(X).
% 2.07/2.25 0 [] -tptpcol_6_26627(X)|isa(X,c_tptpcol_6_26627).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_5_24579)|tptpcol_5_24579(X).
% 2.07/2.25 0 [] -tptpcol_5_24579(X)|isa(X,c_tptpcol_5_24579).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_4_24578)|tptpcol_4_24578(X).
% 2.07/2.25 0 [] -tptpcol_4_24578(X)|isa(X,c_tptpcol_4_24578).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_3_16386)|tptpcol_3_16386(X).
% 2.07/2.25 0 [] -tptpcol_3_16386(X)|isa(X,c_tptpcol_3_16386).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_1_1)|tptpcol_1_1(X).
% 2.07/2.25 0 [] -tptpcol_1_1(X)|isa(X,c_tptpcol_1_1).
% 2.07/2.25 0 [] -isa(X,c_tptpcol_2_2)|tptpcol_2_2(X).
% 2.07/2.25 0 [] -tptpcol_2_2(X)|isa(X,c_tptpcol_2_2).
% 2.07/2.25 0 [] -genls(ARG1,INS)|collection(INS).
% 2.07/2.25 0 [] -genls(ARG1,INS)|collection(INS).
% 2.07/2.25 0 [] -genls(INS,ARG2)|collection(INS).
% 2.07/2.25 0 [] -genls(INS,ARG2)|collection(INS).
% 2.07/2.25 0 [] -genls(X,Y)| -genls(Y,Z)|genls(X,Z).
% 2.07/2.25 0 [] -collection(X)|genls(X,X).
% 2.07/2.25 0 [] -collection(X)|genls(X,X).
% 2.07/2.25 0 [] -genls(OLD,ARG2)| -genls(NEW,OLD)|genls(NEW,ARG2).
% 2.07/2.25 0 [] -genls(ARG1,OLD)| -genls(OLD,NEW)|genls(ARG1,NEW).
% 2.07/2.25 0 [] -isa(X,c_transitivebinarypredicate)|transitivebinarypredicate(X).
% 2.07/2.25 0 [] -transitivebinarypredicate(X)|isa(X,c_transitivebinarypredicate).
% 2.07/2.25 0 [] -isa(ARG1,INS)|collection(INS).
% 2.07/2.25 0 [] -isa(ARG1,INS)|collection(INS).
% 2.07/2.25 0 [] -isa(INS,ARG2)|thing(INS).
% 2.07/2.25 0 [] -isa(INS,ARG2)|thing(INS).
% 2.07/2.25 0 [] -isa(ARG1,OLD)| -genls(OLD,NEW)|isa(ARG1,NEW).
% 2.07/2.25 0 [] mtvisible(c_universalvocabularymt).
% 2.07/2.25 0 [] -mtvisible(SPECMT)| -genlmt(SPECMT,GENLMT)|mtvisible(GENLMT).
% 2.07/2.25 0 [] -genlmt(ARG1,INS)|microtheory(INS).
% 2.07/2.25 0 [] -genlmt(ARG1,INS)|microtheory(INS).
% 2.07/2.25 0 [] -genlmt(INS,ARG2)|microtheory(INS).
% 2.07/2.25 0 [] -genlmt(INS,ARG2)|microtheory(INS).
% 2.07/2.25 0 [] -genlmt(X,Y)| -genlmt(Y,Z)|genlmt(X,Z).
% 2.07/2.25 0 [] -microtheory(X)|genlmt(X,X).
% 2.07/2.25 0 [] -microtheory(X)|genlmt(X,X).
% 2.07/2.25 0 [] mtvisible(c_basekb).
% 2.07/2.25 0 [] mtvisible(c_unitedstatesgeographypeoplemt).
% 2.07/2.25 0 [] -disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269).
% 2.07/2.25 end_of_list.
% 2.07/2.25
% 2.07/2.25 SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=3.
% 2.07/2.25
% 2.07/2.25 This is a Horn set without equality. The strategy will
% 2.07/2.25 be hyperresolution, with satellites in sos and nuclei
% 2.07/2.25 in usable.
% 2.07/2.25
% 2.07/2.25 dependent: set(hyper_res).
% 2.07/2.25 dependent: clear(order_hyper).
% 2.07/2.25
% 2.07/2.25 ------------> process usable:
% 2.07/2.25 ** KEPT (pick-wt=4): 1 [] -tptpcol_2_2(A)|tptpcol_1_1(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 2 [] -tptpcol_3_16386(A)|tptpcol_2_2(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 3 [] -tptpcol_4_24578(A)|tptpcol_3_16386(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 4 [] -tptpcol_5_24579(A)|tptpcol_4_24578(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 5 [] -tptpcol_6_26627(A)|tptpcol_5_24579(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 6 [] -tptpcol_7_26628(A)|tptpcol_6_26627(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 7 [] -tptpcol_8_26629(A)|tptpcol_7_26628(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 8 [] -tptpcol_9_26885(A)|tptpcol_8_26629(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 9 [] -tptpcol_10_26886(A)|tptpcol_9_26885(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 10 [] -tptpcol_11_26887(A)|tptpcol_10_26886(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 11 [] -tptpcol_12_26919(A)|tptpcol_11_26887(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 12 [] -tptpcol_13_26920(A)|tptpcol_12_26919(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 13 [] -tptpcol_14_26921(A)|tptpcol_13_26920(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 14 [] -tptpcol_15_26925(A)|tptpcol_14_26921(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 15 [] -tptpcol_16_26926(A)|tptpcol_15_26925(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 16 [] -tptpcol_2_65537(A)|tptpcol_1_65536(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 17 [] -tptpcol_3_81921(A)|tptpcol_2_65537(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 18 [] -tptpcol_4_90113(A)|tptpcol_3_81921(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 19 [] -tptpcol_5_90114(A)|tptpcol_4_90113(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 20 [] -tptpcol_6_92162(A)|tptpcol_5_90114(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 21 [] -tptpcol_7_92163(A)|tptpcol_6_92162(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 22 [] -tptpcol_8_92164(A)|tptpcol_7_92163(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 23 [] -tptpcol_9_92165(A)|tptpcol_8_92164(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 24 [] -tptpcol_10_92166(A)|tptpcol_9_92165(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 25 [] -tptpcol_11_92230(A)|tptpcol_10_92166(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 26 [] -tptpcol_12_92262(A)|tptpcol_11_92230(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 27 [] -tptpcol_13_92263(A)|tptpcol_12_92262(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 28 [] -tptpcol_14_92264(A)|tptpcol_13_92263(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 29 [] -tptpcol_15_92268(A)|tptpcol_14_92264(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 30 [] -tptpcol_16_92269(A)|tptpcol_15_92268(A).
% 2.07/2.25 ** KEPT (pick-wt=4): 31 [] -tptpcol_1_1(A)| -tptpcol_1_65536(A).
% 2.07/2.25 ** KEPT (pick-wt=9): 32 [] -isa(A,B)| -isa(A,C)| -disjointwith(B,C).
% 2.07/2.25 ** KEPT (pick-wt=9): 33 [] -genlinverse(A,B)| -genlinverse(B,C)|genlpreds(A,C).
% 2.07/2.25 ** KEPT (pick-wt=5): 34 [] -genlpreds(A,B)|predicate(B).
% 2.07/2.25 Following clause subsumed by 34 during input processing: 0 [] -genlpreds(A,B)|predicate(B).
% 2.07/2.25 ** KEPT (pick-wt=5): 35 [] -genlpreds(A,B)|predicate(A).
% 2.07/2.25 Following clause subsumed by 35 during input processing: 0 [] -genlpreds(A,B)|predicate(A).
% 2.07/2.25 ** KEPT (pick-wt=9): 36 [] -genlpreds(A,B)| -genlpreds(B,C)|genlpreds(A,C).
% 2.07/2.25 ** KEPT (pick-wt=5): 37 [] -predicate(A)|genlpreds(A,A).
% 2.07/2.25 Following clause subsumed by 37 during input processing: 0 [] -predicate(A)|genlpreds(A,A).
% 2.07/2.25 ** KEPT (pick-wt=5): 38 [] -genlinverse(A,B)|binarypredicate(B).
% 2.07/2.25 ** KEPT (pick-wt=5): 39 [] -genlinverse(A,B)|binarypredicate(A).
% 2.07/2.25 ** KEPT (pick-wt=9): 40 [] -genlinverse(A,B)| -genlpreds(C,A)|genlinverse(C,B).
% 2.07/2.25 ** KEPT (pick-wt=9): 41 [] -genlinverse(A,B)| -genlpreds(B,C)|genlinverse(A,C).
% 2.07/2.25 ** KEPT (pick-wt=5): 42 [] -disjointwith(A,B)|collection(B).
% 2.07/2.25 ** KEPT (pick-wt=5): 43 [] -disjointwith(A,B)|collection(A).
% 2.07/2.25 ** KEPT (pick-wt=6): 44 [] -disjointwith(A,B)|disjointwith(B,A).
% 2.07/2.25 ** KEPT (pick-wt=9): 45 [] -disjointwith(A,B)| -genls(C,B)|disjointwith(A,C).
% 2.07/2.25 ** KEPT (pick-wt=9): 46 [] -disjointwith(A,B)| -genls(C,A)|disjointwith(C,B).
% 2.07/2.25 ** KEPT (pick-wt=5): 47 [] -isa(A,c_tptpcol_16_92269)|tptpcol_16_92269(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 48 [] -tptpcol_16_92269(A)|isa(A,c_tptpcol_16_92269).
% 2.07/2.25 ** KEPT (pick-wt=5): 49 [] -isa(A,c_tptpcol_15_92268)|tptpcol_15_92268(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 50 [] -tptpcol_15_92268(A)|isa(A,c_tptpcol_15_92268).
% 2.07/2.25 ** KEPT (pick-wt=5): 51 [] -isa(A,c_tptpcol_14_92264)|tptpcol_14_92264(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 52 [] -tptpcol_14_92264(A)|isa(A,c_tptpcol_14_92264).
% 2.07/2.25 ** KEPT (pick-wt=5): 53 [] -isa(A,c_tptpcol_13_92263)|tptpcol_13_92263(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 54 [] -tptpcol_13_92263(A)|isa(A,c_tptpcol_13_92263).
% 2.07/2.25 ** KEPT (pick-wt=5): 55 [] -isa(A,c_tptpcol_12_92262)|tptpcol_12_92262(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 56 [] -tptpcol_12_92262(A)|isa(A,c_tptpcol_12_92262).
% 2.07/2.25 ** KEPT (pick-wt=5): 57 [] -isa(A,c_tptpcol_11_92230)|tptpcol_11_92230(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 58 [] -tptpcol_11_92230(A)|isa(A,c_tptpcol_11_92230).
% 2.07/2.25 ** KEPT (pick-wt=5): 59 [] -isa(A,c_tptpcol_10_92166)|tptpcol_10_92166(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 60 [] -tptpcol_10_92166(A)|isa(A,c_tptpcol_10_92166).
% 2.07/2.25 ** KEPT (pick-wt=5): 61 [] -isa(A,c_tptpcol_9_92165)|tptpcol_9_92165(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 62 [] -tptpcol_9_92165(A)|isa(A,c_tptpcol_9_92165).
% 2.07/2.25 ** KEPT (pick-wt=5): 63 [] -isa(A,c_tptpcol_8_92164)|tptpcol_8_92164(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 64 [] -tptpcol_8_92164(A)|isa(A,c_tptpcol_8_92164).
% 2.07/2.25 ** KEPT (pick-wt=5): 65 [] -isa(A,c_tptpcol_7_92163)|tptpcol_7_92163(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 66 [] -tptpcol_7_92163(A)|isa(A,c_tptpcol_7_92163).
% 2.07/2.25 ** KEPT (pick-wt=5): 67 [] -isa(A,c_tptpcol_6_92162)|tptpcol_6_92162(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 68 [] -tptpcol_6_92162(A)|isa(A,c_tptpcol_6_92162).
% 2.07/2.25 ** KEPT (pick-wt=5): 69 [] -isa(A,c_tptpcol_5_90114)|tptpcol_5_90114(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 70 [] -tptpcol_5_90114(A)|isa(A,c_tptpcol_5_90114).
% 2.07/2.25 ** KEPT (pick-wt=5): 71 [] -isa(A,c_tptpcol_4_90113)|tptpcol_4_90113(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 72 [] -tptpcol_4_90113(A)|isa(A,c_tptpcol_4_90113).
% 2.07/2.25 ** KEPT (pick-wt=5): 73 [] -isa(A,c_tptpcol_3_81921)|tptpcol_3_81921(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 74 [] -tptpcol_3_81921(A)|isa(A,c_tptpcol_3_81921).
% 2.07/2.25 ** KEPT (pick-wt=5): 75 [] -isa(A,c_tptpcol_1_65536)|tptpcol_1_65536(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 76 [] -tptpcol_1_65536(A)|isa(A,c_tptpcol_1_65536).
% 2.07/2.25 ** KEPT (pick-wt=5): 77 [] -isa(A,c_tptpcol_2_65537)|tptpcol_2_65537(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 78 [] -tptpcol_2_65537(A)|isa(A,c_tptpcol_2_65537).
% 2.07/2.25 ** KEPT (pick-wt=5): 79 [] -isa(A,c_tptpcol_16_26926)|tptpcol_16_26926(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 80 [] -tptpcol_16_26926(A)|isa(A,c_tptpcol_16_26926).
% 2.07/2.25 ** KEPT (pick-wt=5): 81 [] -isa(A,c_tptpcol_15_26925)|tptpcol_15_26925(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 82 [] -tptpcol_15_26925(A)|isa(A,c_tptpcol_15_26925).
% 2.07/2.25 ** KEPT (pick-wt=5): 83 [] -isa(A,c_tptpcol_14_26921)|tptpcol_14_26921(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 84 [] -tptpcol_14_26921(A)|isa(A,c_tptpcol_14_26921).
% 2.07/2.25 ** KEPT (pick-wt=5): 85 [] -isa(A,c_tptpcol_13_26920)|tptpcol_13_26920(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 86 [] -tptpcol_13_26920(A)|isa(A,c_tptpcol_13_26920).
% 2.07/2.25 ** KEPT (pick-wt=5): 87 [] -isa(A,c_tptpcol_12_26919)|tptpcol_12_26919(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 88 [] -tptpcol_12_26919(A)|isa(A,c_tptpcol_12_26919).
% 2.07/2.25 ** KEPT (pick-wt=5): 89 [] -isa(A,c_tptpcol_11_26887)|tptpcol_11_26887(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 90 [] -tptpcol_11_26887(A)|isa(A,c_tptpcol_11_26887).
% 2.07/2.25 ** KEPT (pick-wt=5): 91 [] -isa(A,c_tptpcol_10_26886)|tptpcol_10_26886(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 92 [] -tptpcol_10_26886(A)|isa(A,c_tptpcol_10_26886).
% 2.07/2.25 ** KEPT (pick-wt=5): 93 [] -isa(A,c_tptpcol_9_26885)|tptpcol_9_26885(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 94 [] -tptpcol_9_26885(A)|isa(A,c_tptpcol_9_26885).
% 2.07/2.25 ** KEPT (pick-wt=5): 95 [] -isa(A,c_tptpcol_8_26629)|tptpcol_8_26629(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 96 [] -tptpcol_8_26629(A)|isa(A,c_tptpcol_8_26629).
% 2.07/2.25 ** KEPT (pick-wt=5): 97 [] -isa(A,c_tptpcol_7_26628)|tptpcol_7_26628(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 98 [] -tptpcol_7_26628(A)|isa(A,c_tptpcol_7_26628).
% 2.07/2.25 ** KEPT (pick-wt=5): 99 [] -isa(A,c_tptpcol_6_26627)|tptpcol_6_26627(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 100 [] -tptpcol_6_26627(A)|isa(A,c_tptpcol_6_26627).
% 2.07/2.25 ** KEPT (pick-wt=5): 101 [] -isa(A,c_tptpcol_5_24579)|tptpcol_5_24579(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 102 [] -tptpcol_5_24579(A)|isa(A,c_tptpcol_5_24579).
% 2.07/2.25 ** KEPT (pick-wt=5): 103 [] -isa(A,c_tptpcol_4_24578)|tptpcol_4_24578(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 104 [] -tptpcol_4_24578(A)|isa(A,c_tptpcol_4_24578).
% 2.07/2.25 ** KEPT (pick-wt=5): 105 [] -isa(A,c_tptpcol_3_16386)|tptpcol_3_16386(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 106 [] -tptpcol_3_16386(A)|isa(A,c_tptpcol_3_16386).
% 2.07/2.25 ** KEPT (pick-wt=5): 107 [] -isa(A,c_tptpcol_1_1)|tptpcol_1_1(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 108 [] -tptpcol_1_1(A)|isa(A,c_tptpcol_1_1).
% 2.07/2.25 ** KEPT (pick-wt=5): 109 [] -isa(A,c_tptpcol_2_2)|tptpcol_2_2(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 110 [] -tptpcol_2_2(A)|isa(A,c_tptpcol_2_2).
% 2.07/2.25 ** KEPT (pick-wt=5): 111 [] -genls(A,B)|collection(B).
% 2.07/2.25 Following clause subsumed by 111 during input processing: 0 [] -genls(A,B)|collection(B).
% 2.07/2.25 ** KEPT (pick-wt=5): 112 [] -genls(A,B)|collection(A).
% 2.07/2.25 Following clause subsumed by 112 during input processing: 0 [] -genls(A,B)|collection(A).
% 2.07/2.25 ** KEPT (pick-wt=9): 113 [] -genls(A,B)| -genls(B,C)|genls(A,C).
% 2.07/2.25 ** KEPT (pick-wt=5): 114 [] -collection(A)|genls(A,A).
% 2.07/2.25 Following clause subsumed by 114 during input processing: 0 [] -collection(A)|genls(A,A).
% 2.07/2.25 Following clause subsumed by 113 during input processing: 0 [] -genls(A,B)| -genls(C,A)|genls(C,B).
% 2.07/2.25 Following clause subsumed by 113 during input processing: 0 [] -genls(A,B)| -genls(B,C)|genls(A,C).
% 2.07/2.25 ** KEPT (pick-wt=5): 115 [] -isa(A,c_transitivebinarypredicate)|transitivebinarypredicate(A).
% 2.07/2.25 ** KEPT (pick-wt=5): 116 [] -transitivebinarypredicate(A)|isa(A,c_transitivebinarypredicate).
% 2.07/2.25 ** KEPT (pick-wt=5): 117 [] -isa(A,B)|collection(B).
% 2.07/2.25 Following clause subsumed by 117 during input processing: 0 [] -isa(A,B)|collection(B).
% 2.07/2.25 ** KEPT (pick-wt=5): 118 [] -isa(A,B)|thing(A).
% 2.07/2.25 Following clause subsumed by 118 during input processing: 0 [] -isa(A,B)|thing(A).
% 2.07/2.25 ** KEPT (pick-wt=9): 119 [] -isa(A,B)| -genls(B,C)|isa(A,C).
% 2.07/2.25 ** KEPT (pick-wt=7): 120 [] -mtvisible(A)| -genlmt(A,B)|mtvisible(B).
% 2.07/2.25 ** KEPT (pick-wt=5): 121 [] -genlmt(A,B)|microtheory(B).
% 2.07/2.28 Following clause subsumed by 121 during input processing: 0 [] -genlmt(A,B)|microtheory(B).
% 2.07/2.28 ** KEPT (pick-wt=5): 122 [] -genlmt(A,B)|microtheory(A).
% 2.07/2.28 Following clause subsumed by 122 during input processing: 0 [] -genlmt(A,B)|microtheory(A).
% 2.07/2.28 ** KEPT (pick-wt=9): 123 [] -genlmt(A,B)| -genlmt(B,C)|genlmt(A,C).
% 2.07/2.28 ** KEPT (pick-wt=5): 124 [] -microtheory(A)|genlmt(A,A).
% 2.07/2.28 Following clause subsumed by 124 during input processing: 0 [] -microtheory(A)|genlmt(A,A).
% 2.07/2.28 ** KEPT (pick-wt=3): 125 [] -disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269).
% 2.07/2.28
% 2.07/2.28 ------------> process sos:
% 2.07/2.28 ** KEPT (pick-wt=3): 126 [] genlmt(c_gregoriancalendarmt,c_basekb).
% 2.07/2.28 ** KEPT (pick-wt=3): 127 [] genlmt(c_unitedstatesgeographypeoplemt,c_peopledatamt).
% 2.07/2.28 ** KEPT (pick-wt=3): 128 [] genlmt(c_unitedstatessociallifemt,c_gregoriancalendarmt).
% 2.07/2.28 ** KEPT (pick-wt=2): 129 [] transitivebinarypredicate(c_genlmt).
% 2.07/2.28 ** KEPT (pick-wt=3): 130 [] genlmt(c_basekb,c_universalvocabularymt).
% 2.07/2.28 ** KEPT (pick-wt=3): 131 [] genlmt(c_peopledatamt,c_unitedstatessociallifemt).
% 2.07/2.28 ** KEPT (pick-wt=3): 132 [] genls(c_tptpcol_2_2,c_tptpcol_1_1).
% 2.07/2.28 ** KEPT (pick-wt=3): 133 [] genls(c_tptpcol_3_16386,c_tptpcol_2_2).
% 2.07/2.28 ** KEPT (pick-wt=3): 134 [] genls(c_tptpcol_4_24578,c_tptpcol_3_16386).
% 2.07/2.28 ** KEPT (pick-wt=3): 135 [] genls(c_tptpcol_5_24579,c_tptpcol_4_24578).
% 2.07/2.28 ** KEPT (pick-wt=3): 136 [] genls(c_tptpcol_6_26627,c_tptpcol_5_24579).
% 2.07/2.28 ** KEPT (pick-wt=3): 137 [] genls(c_tptpcol_7_26628,c_tptpcol_6_26627).
% 2.07/2.28 ** KEPT (pick-wt=3): 138 [] genls(c_tptpcol_8_26629,c_tptpcol_7_26628).
% 2.07/2.28 ** KEPT (pick-wt=3): 139 [] genls(c_tptpcol_9_26885,c_tptpcol_8_26629).
% 2.07/2.28 ** KEPT (pick-wt=3): 140 [] genls(c_tptpcol_10_26886,c_tptpcol_9_26885).
% 2.07/2.28 ** KEPT (pick-wt=3): 141 [] genls(c_tptpcol_11_26887,c_tptpcol_10_26886).
% 2.07/2.28 ** KEPT (pick-wt=3): 142 [] genls(c_tptpcol_12_26919,c_tptpcol_11_26887).
% 2.07/2.28 ** KEPT (pick-wt=3): 143 [] genls(c_tptpcol_13_26920,c_tptpcol_12_26919).
% 2.07/2.28 ** KEPT (pick-wt=3): 144 [] genls(c_tptpcol_14_26921,c_tptpcol_13_26920).
% 2.07/2.28 ** KEPT (pick-wt=3): 145 [] genls(c_tptpcol_15_26925,c_tptpcol_14_26921).
% 2.07/2.28 ** KEPT (pick-wt=3): 146 [] genls(c_tptpcol_16_26926,c_tptpcol_15_26925).
% 2.07/2.28 ** KEPT (pick-wt=3): 147 [] genls(c_tptpcol_2_65537,c_tptpcol_1_65536).
% 2.07/2.28 ** KEPT (pick-wt=3): 148 [] genls(c_tptpcol_3_81921,c_tptpcol_2_65537).
% 2.07/2.28 ** KEPT (pick-wt=3): 149 [] genls(c_tptpcol_4_90113,c_tptpcol_3_81921).
% 2.07/2.28 ** KEPT (pick-wt=3): 150 [] genls(c_tptpcol_5_90114,c_tptpcol_4_90113).
% 2.07/2.28 ** KEPT (pick-wt=3): 151 [] genls(c_tptpcol_6_92162,c_tptpcol_5_90114).
% 2.07/2.28 ** KEPT (pick-wt=3): 152 [] genls(c_tptpcol_7_92163,c_tptpcol_6_92162).
% 2.07/2.28 ** KEPT (pick-wt=3): 153 [] genls(c_tptpcol_8_92164,c_tptpcol_7_92163).
% 2.07/2.28 ** KEPT (pick-wt=3): 154 [] genls(c_tptpcol_9_92165,c_tptpcol_8_92164).
% 2.07/2.28 ** KEPT (pick-wt=3): 155 [] genls(c_tptpcol_10_92166,c_tptpcol_9_92165).
% 2.07/2.28 ** KEPT (pick-wt=3): 156 [] genls(c_tptpcol_11_92230,c_tptpcol_10_92166).
% 2.07/2.28 ** KEPT (pick-wt=3): 157 [] genls(c_tptpcol_12_92262,c_tptpcol_11_92230).
% 2.07/2.28 ** KEPT (pick-wt=3): 158 [] genls(c_tptpcol_13_92263,c_tptpcol_12_92262).
% 2.07/2.28 ** KEPT (pick-wt=3): 159 [] genls(c_tptpcol_14_92264,c_tptpcol_13_92263).
% 2.07/2.28 ** KEPT (pick-wt=3): 160 [] genls(c_tptpcol_15_92268,c_tptpcol_14_92264).
% 2.07/2.28 ** KEPT (pick-wt=3): 161 [] genls(c_tptpcol_16_92269,c_tptpcol_15_92268).
% 2.07/2.28 ** KEPT (pick-wt=3): 162 [] disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536).
% 2.07/2.28 ** KEPT (pick-wt=2): 163 [] mtvisible(c_universalvocabularymt).
% 2.07/2.28 ** KEPT (pick-wt=2): 164 [] mtvisible(c_basekb).
% 2.07/2.28 ** KEPT (pick-wt=2): 165 [] mtvisible(c_unitedstatesgeographypeoplemt).
% 2.07/2.28
% 2.07/2.28 ======= end of input processing =======
% 2.07/2.28
% 2.07/2.28 =========== start of search ===========
% 2.07/2.28
% 2.07/2.28 -------- PROOF --------
% 2.07/2.28
% 2.07/2.28 ----> UNIT CONFLICT at 0.03 sec ----> 971 [binary,970.1,125.1] $F.
% 2.07/2.28
% 2.07/2.28 Length of proof is 30. Level of proof is 5.
% 2.07/2.28
% 2.07/2.28 ---------------- PROOF ----------------
% 2.07/2.28 % SZS status Theorem
% 2.07/2.28 % SZS output start Refutation
% See solution above
% 2.07/2.28 ------------ end of proof -------------
% 2.07/2.28
% 2.07/2.28
% 2.07/2.28 Search stopped by max_proofs option.
% 2.07/2.28
% 2.07/2.28
% 2.07/2.28 Search stopped by max_proofs option.
% 2.07/2.28
% 2.07/2.28 ============ end of search ============
% 2.07/2.28
% 2.07/2.28 -------------- statistics -------------
% 2.07/2.28 clauses given 529
% 2.07/2.28 clauses generated 7347
% 2.07/2.28 clauses kept 970
% 2.07/2.28 clauses forward subsumed 6555
% 2.07/2.28 clauses back subsumed 0
% 2.07/2.28 Kbytes malloced 1953
% 2.07/2.28
% 2.07/2.28 ----------- times (seconds) -----------
% 2.07/2.28 user CPU time 0.03 (0 hr, 0 min, 0 sec)
% 2.07/2.28 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 2.07/2.28 wall-clock time 1 (0 hr, 0 min, 1 sec)
% 2.07/2.28
% 2.07/2.28 That finishes the proof of the theorem.
% 2.07/2.28
% 2.07/2.28 Process 14770 finished Wed Jul 27 04:12:48 2022
% 2.07/2.28 Otter interrupted
% 2.07/2.28 PROOF FOUND
%------------------------------------------------------------------------------