%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR049+2 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n016.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 : 600s
% DateTime : Fri Jul 15 20:56:11 EDT 2022
% Result : Theorem 249.15s 240.82s
% Output : Proof 249.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : CSR049+2 : TPTP v8.1.0. Released v3.4.0.
% 0.10/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.33 % Computer : n016.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Sat Jun 11 03:54:40 EDT 2022
% 0.11/0.33 % CPUTime :
% 249.15/240.82 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 249.15/240.83 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 249.15/240.83
% 249.15/240.83 %-----------------------------------------------------
% 249.15/240.83 fof(ax1_465, axiom, genls(c_tptpcol_13_26920, c_tptpcol_12_26919), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_465)).
% 249.15/240.83 fof(ax1_152, axiom, disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_152)).
% 249.15/240.83 fof(ax1_1109, axiom, ! [_522016, _522019, _522022] : (genls(_522016, _522019) & genls(_522019, _522022) => genls(_522016, _522022)), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_1109)).
% 249.15/240.83 fof(ax1_429, axiom, genls(c_tptpcol_11_26887, c_tptpcol_10_26886), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_429)).
% 249.15/240.83 fof(ax1_476, axiom, genls(c_tptpcol_5_90114, c_tptpcol_4_90113), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_476)).
% 249.15/240.83 fof(ax1_285, axiom, genls(c_tptpcol_4_16387, c_tptpcol_3_16386), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_285)).
% 249.15/240.83 fof(ax1_417, axiom, genls(c_tptpcol_6_92162, c_tptpcol_5_90114), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_417)).
% 249.15/240.83 fof(ax1_1121, axiom, ! [_522568, _522571, _522574] : (disjointwith(_522568, _522571) & genls(_522574, _522571) => disjointwith(_522568, _522574)), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_1121)).
% 249.15/240.83 fof(ax1_141, axiom, genls(c_tptpcol_12_26919, c_tptpcol_11_26887), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_141)).
% 249.15/240.83 fof(ax1_1112, axiom, ! [_522881, _522884, _522887] : (genls(_522881, _522884) & genls(_522887, _522881) => genls(_522887, _522884)), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_1112)).
% 249.15/240.83 fof(ax1_313, axiom, genls(c_tptpcol_14_26921, c_tptpcol_13_26920), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_313)).
% 249.15/240.83 fof(ax1_348, axiom, genls(c_tptpcol_2_65537, c_tptpcol_1_65536), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_348)).
% 249.15/240.83 fof(ax1_1111, axiom, ! [_523222] : (collection(_523222) => genls(_523222, _523222)), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_1111)).
% 249.15/240.83 fof(ax1_473, axiom, genls(c_tptpcol_13_92263, c_tptpcol_12_92262), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_473)).
% 249.15/240.83 fof(ax1_385, axiom, genls(c_tptpcol_3_16386, c_tptpcol_2_2), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_385)).
% 249.15/240.83 fof(ax1_480, axiom, genls(c_tptpcol_15_26925, c_tptpcol_14_26921), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_480)).
% 249.15/240.83 fof(ax1_324, axiom, genls(c_tptpcol_7_92163, c_tptpcol_6_92162), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_324)).
% 249.15/240.83 fof(ax1_1105, axiom, ! [_523680, _523683] : (genls(_523680, _523683) => collection(_523683)), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_1105)).
% 249.15/240.83 fof(ax1_497, axiom, genls(c_tptpcol_10_92166, c_tptpcol_9_92165), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_497)).
% 249.15/240.83 fof(ax1_1122, axiom, ! [_523932, _523935, _523938] : (disjointwith(_523932, _523935) & genls(_523938, _523932) => disjointwith(_523938, _523935)), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_1122)).
% 249.15/240.83 fof(ax1_47, axiom, genls(c_tptpcol_11_92230, c_tptpcol_10_92166), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_47)).
% 249.15/240.83 fof(ax1_376, axiom, genls(c_tptpcol_4_90113, c_tptpcol_3_81921), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_376)).
% 249.15/240.83 fof(ax1_431, axiom, genls(c_tptpcol_16_26926, c_tptpcol_15_26925), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_431)).
% 249.15/240.83 fof(ax1_467, axiom, genls(c_tptpcol_14_92264, c_tptpcol_13_92263), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_467)).
% 249.15/240.83 fof(query99, conjecture, mtvisible(c_unitedstatesgeographypeoplemt) => disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), file('/export/starexec/sandbox/benchmark/theBenchmark.p', query99)).
% 249.15/240.83 fof(ax1_145, axiom, genls(c_tptpcol_2_2, c_tptpcol_1_1), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_145)).
% 249.15/240.83 fof(ax1_239, axiom, genls(c_tptpcol_8_26629, c_tptpcol_7_26628), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_239)).
% 249.15/240.83 fof(ax1_41, axiom, genls(c_tptpcol_3_81921, c_tptpcol_2_65537), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_41)).
% 249.15/240.83 fof(ax1_222, axiom, genls(c_tptpcol_4_24578, c_tptpcol_3_16386), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_222)).
% 249.15/240.83 fof(ax1_420, axiom, genls(c_tptpcol_8_92164, c_tptpcol_7_92163), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_420)).
% 249.15/240.83 fof(ax1_102, axiom, genls(c_tptpcol_15_92268, c_tptpcol_14_92264), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_102)).
% 249.15/240.83 fof(ax1_261, axiom, genls(c_tptpcol_7_26628, c_tptpcol_6_26627), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_261)).
% 249.15/240.83 fof(ax1_410, axiom, genls(c_tptpcol_9_26885, c_tptpcol_8_26629), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_410)).
% 249.15/240.83 fof(ax1_118, axiom, genls(c_tptpcol_5_24579, c_tptpcol_4_24578), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_118)).
% 249.15/240.83 fof(ax1_277, axiom, genls(c_tptpcol_10_26886, c_tptpcol_9_26885), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_277)).
% 249.15/240.83 fof(ax1_374, axiom, genls(c_tptpcol_6_26627, c_tptpcol_5_24579), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_374)).
% 249.15/240.83 fof(ax1_89, axiom, genls(c_tptpcol_12_92262, c_tptpcol_11_92230), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_89)).
% 249.15/240.83 fof(ax1_148, axiom, genls(c_tptpcol_9_92165, c_tptpcol_8_92164), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_148)).
% 249.15/240.83 fof(ax1_267, axiom, genls(c_tptpcol_16_92269, c_tptpcol_15_92268), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_267)).
% 249.15/240.83
% 249.15/240.83 cnf(1, plain, [-(genls(c_tptpcol_13_26920, c_tptpcol_12_26919))], clausify(ax1_465)).
% 249.15/240.83 cnf(2, plain, [-(disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536))], clausify(ax1_152)).
% 249.15/240.83 cnf(3, plain, [-(genls(_276252, _276363)), genls(_276252, _276308), genls(_276308, _276363)], clausify(ax1_1109)).
% 249.15/240.83 cnf(4, plain, [-(genls(c_tptpcol_11_26887, c_tptpcol_10_26886))], clausify(ax1_429)).
% 249.15/240.83 cnf(5, plain, [-(genls(c_tptpcol_5_90114, c_tptpcol_4_90113))], clausify(ax1_476)).
% 249.15/240.83 cnf(6, plain, [-(genls(c_tptpcol_4_16387, c_tptpcol_3_16386))], clausify(ax1_285)).
% 249.15/240.83 cnf(7, plain, [-(genls(c_tptpcol_6_92162, c_tptpcol_5_90114))], clausify(ax1_417)).
% 249.15/240.83 cnf(8, plain, [-(disjointwith(_279929, _280040)), disjointwith(_279929, _279985), genls(_280040, _279985)], clausify(ax1_1121)).
% 249.15/240.83 cnf(9, plain, [-(genls(c_tptpcol_12_26919, c_tptpcol_11_26887))], clausify(ax1_141)).
% 249.15/240.83 cnf(10, plain, [-(genls(_277294, _277239)), genls(_277183, _277239), genls(_277294, _277183)], clausify(ax1_1112)).
% 249.15/240.83 cnf(11, plain, [-(genls(c_tptpcol_14_26921, c_tptpcol_13_26920))], clausify(ax1_313)).
% 249.15/240.83 cnf(12, plain, [-(genls(c_tptpcol_2_65537, c_tptpcol_1_65536))], clausify(ax1_348)).
% 249.15/240.83 cnf(13, plain, [collection(_276951), -(genls(_276951, _276951))], clausify(ax1_1111)).
% 249.15/240.83 cnf(14, plain, [-(genls(c_tptpcol_13_92263, c_tptpcol_12_92262))], clausify(ax1_473)).
% 249.15/240.83 cnf(15, plain, [-(genls(c_tptpcol_3_16386, c_tptpcol_2_2))], clausify(ax1_385)).
% 249.15/240.83 cnf(16, plain, [-(genls(c_tptpcol_15_26925, c_tptpcol_14_26921))], clausify(ax1_480)).
% 249.15/240.83 cnf(17, plain, [-(genls(c_tptpcol_7_92163, c_tptpcol_6_92162))], clausify(ax1_324)).
% 249.15/240.83 cnf(18, plain, [genls(_275104, _275148), -(collection(_275148))], clausify(ax1_1105)).
% 249.15/240.83 cnf(19, plain, [-(genls(c_tptpcol_10_92166, c_tptpcol_9_92165))], clausify(ax1_497)).
% 249.15/240.83 cnf(20, plain, [-(disjointwith(_280507, _280452)), disjointwith(_280396, _280452), genls(_280507, _280396)], clausify(ax1_1122)).
% 249.15/240.83 cnf(21, plain, [-(genls(c_tptpcol_11_92230, c_tptpcol_10_92166))], clausify(ax1_47)).
% 249.15/240.83 cnf(22, plain, [-(genls(c_tptpcol_4_90113, c_tptpcol_3_81921))], clausify(ax1_376)).
% 249.15/240.83 cnf(23, plain, [-(genls(c_tptpcol_16_26926, c_tptpcol_15_26925))], clausify(ax1_431)).
% 249.15/240.83 cnf(24, plain, [-(genls(c_tptpcol_14_92264, c_tptpcol_13_92263))], clausify(ax1_467)).
% 249.15/240.83 cnf(25, plain, [disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269)], clausify(query99)).
% 249.15/240.83 cnf(26, plain, [-(genls(c_tptpcol_2_2, c_tptpcol_1_1))], clausify(ax1_145)).
% 249.15/240.83 cnf(27, plain, [-(genls(c_tptpcol_8_26629, c_tptpcol_7_26628))], clausify(ax1_239)).
% 249.15/240.83 cnf(28, plain, [-(genls(c_tptpcol_3_81921, c_tptpcol_2_65537))], clausify(ax1_41)).
% 249.15/240.83 cnf(29, plain, [-(genls(c_tptpcol_4_24578, c_tptpcol_3_16386))], clausify(ax1_222)).
% 249.15/240.83 cnf(30, plain, [-(genls(c_tptpcol_8_92164, c_tptpcol_7_92163))], clausify(ax1_420)).
% 249.15/240.83 cnf(31, plain, [-(genls(c_tptpcol_15_92268, c_tptpcol_14_92264))], clausify(ax1_102)).
% 249.15/240.83 cnf(32, plain, [-(genls(c_tptpcol_7_26628, c_tptpcol_6_26627))], clausify(ax1_261)).
% 249.15/240.83 cnf(33, plain, [-(genls(c_tptpcol_9_26885, c_tptpcol_8_26629))], clausify(ax1_410)).
% 249.15/240.83 cnf(34, plain, [-(genls(c_tptpcol_5_24579, c_tptpcol_4_24578))], clausify(ax1_118)).
% 249.15/240.83 cnf(35, plain, [-(genls(c_tptpcol_10_26886, c_tptpcol_9_26885))], clausify(ax1_277)).
% 249.15/240.83 cnf(36, plain, [-(genls(c_tptpcol_6_26627, c_tptpcol_5_24579))], clausify(ax1_374)).
% 249.15/240.83 cnf(37, plain, [-(genls(c_tptpcol_12_92262, c_tptpcol_11_92230))], clausify(ax1_89)).
% 249.15/240.83 cnf(38, plain, [-(genls(c_tptpcol_9_92165, c_tptpcol_8_92164))], clausify(ax1_148)).
% 249.15/240.83 cnf(39, plain, [-(genls(c_tptpcol_16_92269, c_tptpcol_15_92268))], clausify(ax1_267)).
% 249.15/240.83
% 249.15/240.83 cnf('1',plain,[disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269)],start(25)).
% 249.15/240.83 cnf('1.1',plain,[-(disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269)), disjointwith(c_tptpcol_1_1, c_tptpcol_16_92269), genls(c_tptpcol_16_26926, c_tptpcol_1_1)],extension(20,bind([[_280452, _280507, _280396], [c_tptpcol_16_92269, c_tptpcol_16_26926, c_tptpcol_1_1]]))).
% 249.15/240.83 cnf('1.1.1',plain,[-(disjointwith(c_tptpcol_1_1, c_tptpcol_16_92269)), disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536), genls(c_tptpcol_16_92269, c_tptpcol_1_65536)],extension(8,bind([[_279929, _280040, _279985], [c_tptpcol_1_1, c_tptpcol_16_92269, c_tptpcol_1_65536]]))).
% 249.15/240.83 cnf('1.1.1.1',plain,[-(disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536))],extension(2)).
% 249.15/240.83 cnf('1.1.1.2',plain,[-(genls(c_tptpcol_16_92269, c_tptpcol_1_65536)), genls(c_tptpcol_16_92269, c_tptpcol_8_92164), genls(c_tptpcol_8_92164, c_tptpcol_1_65536)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_16_92269, c_tptpcol_8_92164, c_tptpcol_1_65536]]))).
% 249.15/240.83 cnf('1.1.1.2.1',plain,[-(genls(c_tptpcol_16_92269, c_tptpcol_8_92164)), genls(c_tptpcol_16_92269, c_tptpcol_12_92262), genls(c_tptpcol_12_92262, c_tptpcol_8_92164)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_16_92269, c_tptpcol_12_92262, c_tptpcol_8_92164]]))).
% 249.15/240.83 cnf('1.1.1.2.1.1',plain,[-(genls(c_tptpcol_16_92269, c_tptpcol_12_92262)), genls(c_tptpcol_16_92269, c_tptpcol_14_92264), genls(c_tptpcol_14_92264, c_tptpcol_12_92262)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_16_92269, c_tptpcol_14_92264, c_tptpcol_12_92262]]))).
% 249.15/240.83 cnf('1.1.1.2.1.1.1',plain,[-(genls(c_tptpcol_16_92269, c_tptpcol_14_92264)), genls(c_tptpcol_16_92269, c_tptpcol_15_92268), genls(c_tptpcol_15_92268, c_tptpcol_14_92264)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_16_92269, c_tptpcol_15_92268, c_tptpcol_14_92264]]))).
% 249.15/240.83 cnf('1.1.1.2.1.1.1.1',plain,[-(genls(c_tptpcol_16_92269, c_tptpcol_15_92268))],extension(39)).
% 249.15/240.83 cnf('1.1.1.2.1.1.1.2',plain,[-(genls(c_tptpcol_15_92268, c_tptpcol_14_92264))],extension(31)).
% 249.15/240.83 cnf('1.1.1.2.1.1.2',plain,[-(genls(c_tptpcol_14_92264, c_tptpcol_12_92262)), genls(c_tptpcol_14_92264, c_tptpcol_13_92263), genls(c_tptpcol_13_92263, c_tptpcol_12_92262)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_14_92264, c_tptpcol_13_92263, c_tptpcol_12_92262]]))).
% 249.15/240.83 cnf('1.1.1.2.1.1.2.1',plain,[-(genls(c_tptpcol_14_92264, c_tptpcol_13_92263))],extension(24)).
% 249.15/240.83 cnf('1.1.1.2.1.1.2.2',plain,[-(genls(c_tptpcol_13_92263, c_tptpcol_12_92262))],extension(14)).
% 249.15/240.83 cnf('1.1.1.2.1.2',plain,[-(genls(c_tptpcol_12_92262, c_tptpcol_8_92164)), genls(c_tptpcol_12_92262, c_tptpcol_10_92166), genls(c_tptpcol_10_92166, c_tptpcol_8_92164)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_12_92262, c_tptpcol_10_92166, c_tptpcol_8_92164]]))).
% 249.15/240.83 cnf('1.1.1.2.1.2.1',plain,[-(genls(c_tptpcol_12_92262, c_tptpcol_10_92166)), genls(c_tptpcol_12_92262, c_tptpcol_11_92230), genls(c_tptpcol_11_92230, c_tptpcol_10_92166)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_12_92262, c_tptpcol_11_92230, c_tptpcol_10_92166]]))).
% 249.15/240.83 cnf('1.1.1.2.1.2.1.1',plain,[-(genls(c_tptpcol_12_92262, c_tptpcol_11_92230))],extension(37)).
% 249.15/240.83 cnf('1.1.1.2.1.2.1.2',plain,[-(genls(c_tptpcol_11_92230, c_tptpcol_10_92166))],extension(21)).
% 249.15/240.83 cnf('1.1.1.2.1.2.2',plain,[-(genls(c_tptpcol_10_92166, c_tptpcol_8_92164)), genls(c_tptpcol_10_92166, c_tptpcol_9_92165), genls(c_tptpcol_9_92165, c_tptpcol_8_92164)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_10_92166, c_tptpcol_9_92165, c_tptpcol_8_92164]]))).
% 249.15/240.83 cnf('1.1.1.2.1.2.2.1',plain,[-(genls(c_tptpcol_10_92166, c_tptpcol_9_92165))],extension(19)).
% 249.15/240.83 cnf('1.1.1.2.1.2.2.2',plain,[-(genls(c_tptpcol_9_92165, c_tptpcol_8_92164))],extension(38)).
% 249.15/240.83 cnf('1.1.1.2.2',plain,[-(genls(c_tptpcol_8_92164, c_tptpcol_1_65536)), genls(c_tptpcol_8_92164, c_tptpcol_4_90113), genls(c_tptpcol_4_90113, c_tptpcol_1_65536)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_8_92164, c_tptpcol_4_90113, c_tptpcol_1_65536]]))).
% 249.15/240.83 cnf('1.1.1.2.2.1',plain,[-(genls(c_tptpcol_8_92164, c_tptpcol_4_90113)), genls(c_tptpcol_8_92164, c_tptpcol_6_92162), genls(c_tptpcol_6_92162, c_tptpcol_4_90113)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_8_92164, c_tptpcol_6_92162, c_tptpcol_4_90113]]))).
% 249.15/240.83 cnf('1.1.1.2.2.1.1',plain,[-(genls(c_tptpcol_8_92164, c_tptpcol_6_92162)), genls(c_tptpcol_8_92164, c_tptpcol_7_92163), genls(c_tptpcol_7_92163, c_tptpcol_6_92162)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_8_92164, c_tptpcol_7_92163, c_tptpcol_6_92162]]))).
% 249.15/240.83 cnf('1.1.1.2.2.1.1.1',plain,[-(genls(c_tptpcol_8_92164, c_tptpcol_7_92163))],extension(30)).
% 249.15/240.83 cnf('1.1.1.2.2.1.1.2',plain,[-(genls(c_tptpcol_7_92163, c_tptpcol_6_92162))],extension(17)).
% 249.15/240.83 cnf('1.1.1.2.2.1.2',plain,[-(genls(c_tptpcol_6_92162, c_tptpcol_4_90113)), genls(c_tptpcol_6_92162, c_tptpcol_5_90114), genls(c_tptpcol_5_90114, c_tptpcol_4_90113)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_6_92162, c_tptpcol_5_90114, c_tptpcol_4_90113]]))).
% 249.15/240.83 cnf('1.1.1.2.2.1.2.1',plain,[-(genls(c_tptpcol_6_92162, c_tptpcol_5_90114))],extension(7)).
% 249.15/240.83 cnf('1.1.1.2.2.1.2.2',plain,[-(genls(c_tptpcol_5_90114, c_tptpcol_4_90113))],extension(5)).
% 249.15/240.83 cnf('1.1.1.2.2.2',plain,[-(genls(c_tptpcol_4_90113, c_tptpcol_1_65536)), genls(c_tptpcol_4_90113, c_tptpcol_2_65537), genls(c_tptpcol_2_65537, c_tptpcol_1_65536)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_4_90113, c_tptpcol_2_65537, c_tptpcol_1_65536]]))).
% 249.15/240.83 cnf('1.1.1.2.2.2.1',plain,[-(genls(c_tptpcol_4_90113, c_tptpcol_2_65537)), genls(c_tptpcol_4_90113, c_tptpcol_3_81921), genls(c_tptpcol_3_81921, c_tptpcol_2_65537)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_4_90113, c_tptpcol_3_81921, c_tptpcol_2_65537]]))).
% 249.15/240.83 cnf('1.1.1.2.2.2.1.1',plain,[-(genls(c_tptpcol_4_90113, c_tptpcol_3_81921))],extension(22)).
% 249.15/240.83 cnf('1.1.1.2.2.2.1.2',plain,[-(genls(c_tptpcol_3_81921, c_tptpcol_2_65537))],extension(28)).
% 249.15/240.83 cnf('1.1.1.2.2.2.2',plain,[-(genls(c_tptpcol_2_65537, c_tptpcol_1_65536))],extension(12)).
% 249.15/240.83 cnf('1.1.2',plain,[-(genls(c_tptpcol_16_26926, c_tptpcol_1_1)), genls(c_tptpcol_16_26926, c_tptpcol_1_1), genls(c_tptpcol_1_1, c_tptpcol_1_1)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_16_26926, c_tptpcol_1_1, c_tptpcol_1_1]]))).
% 249.15/240.83 cnf('1.1.2.1',plain,[-(genls(c_tptpcol_16_26926, c_tptpcol_1_1)), genls(c_tptpcol_16_26926, c_tptpcol_8_26629), genls(c_tptpcol_8_26629, c_tptpcol_1_1)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_16_26926, c_tptpcol_8_26629, c_tptpcol_1_1]]))).
% 249.15/240.83 cnf('1.1.2.1.1',plain,[-(genls(c_tptpcol_16_26926, c_tptpcol_8_26629)), genls(c_tptpcol_16_26926, c_tptpcol_12_26919), genls(c_tptpcol_12_26919, c_tptpcol_8_26629)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_16_26926, c_tptpcol_12_26919, c_tptpcol_8_26629]]))).
% 249.15/240.83 cnf('1.1.2.1.1.1',plain,[-(genls(c_tptpcol_16_26926, c_tptpcol_12_26919)), genls(c_tptpcol_16_26926, c_tptpcol_14_26921), genls(c_tptpcol_14_26921, c_tptpcol_12_26919)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_16_26926, c_tptpcol_14_26921, c_tptpcol_12_26919]]))).
% 249.15/240.83 cnf('1.1.2.1.1.1.1',plain,[-(genls(c_tptpcol_16_26926, c_tptpcol_14_26921)), genls(c_tptpcol_16_26926, c_tptpcol_15_26925), genls(c_tptpcol_15_26925, c_tptpcol_14_26921)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_16_26926, c_tptpcol_15_26925, c_tptpcol_14_26921]]))).
% 249.15/240.83 cnf('1.1.2.1.1.1.1.1',plain,[-(genls(c_tptpcol_16_26926, c_tptpcol_15_26925))],extension(23)).
% 249.15/240.83 cnf('1.1.2.1.1.1.1.2',plain,[-(genls(c_tptpcol_15_26925, c_tptpcol_14_26921))],extension(16)).
% 249.15/240.83 cnf('1.1.2.1.1.1.2',plain,[-(genls(c_tptpcol_14_26921, c_tptpcol_12_26919)), genls(c_tptpcol_14_26921, c_tptpcol_13_26920), genls(c_tptpcol_13_26920, c_tptpcol_12_26919)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_14_26921, c_tptpcol_13_26920, c_tptpcol_12_26919]]))).
% 249.15/240.83 cnf('1.1.2.1.1.1.2.1',plain,[-(genls(c_tptpcol_14_26921, c_tptpcol_13_26920))],extension(11)).
% 249.15/240.83 cnf('1.1.2.1.1.1.2.2',plain,[-(genls(c_tptpcol_13_26920, c_tptpcol_12_26919))],extension(1)).
% 249.15/240.83 cnf('1.1.2.1.1.2',plain,[-(genls(c_tptpcol_12_26919, c_tptpcol_8_26629)), genls(c_tptpcol_12_26919, c_tptpcol_10_26886), genls(c_tptpcol_10_26886, c_tptpcol_8_26629)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_12_26919, c_tptpcol_10_26886, c_tptpcol_8_26629]]))).
% 249.15/240.83 cnf('1.1.2.1.1.2.1',plain,[-(genls(c_tptpcol_12_26919, c_tptpcol_10_26886)), genls(c_tptpcol_12_26919, c_tptpcol_11_26887), genls(c_tptpcol_11_26887, c_tptpcol_10_26886)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_12_26919, c_tptpcol_11_26887, c_tptpcol_10_26886]]))).
% 249.15/240.83 cnf('1.1.2.1.1.2.1.1',plain,[-(genls(c_tptpcol_12_26919, c_tptpcol_11_26887))],extension(9)).
% 249.15/240.83 cnf('1.1.2.1.1.2.1.2',plain,[-(genls(c_tptpcol_11_26887, c_tptpcol_10_26886))],extension(4)).
% 249.15/240.83 cnf('1.1.2.1.1.2.2',plain,[-(genls(c_tptpcol_10_26886, c_tptpcol_8_26629)), genls(c_tptpcol_10_26886, c_tptpcol_9_26885), genls(c_tptpcol_9_26885, c_tptpcol_8_26629)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_10_26886, c_tptpcol_9_26885, c_tptpcol_8_26629]]))).
% 249.15/240.83 cnf('1.1.2.1.1.2.2.1',plain,[-(genls(c_tptpcol_10_26886, c_tptpcol_9_26885))],extension(35)).
% 249.15/240.83 cnf('1.1.2.1.1.2.2.2',plain,[-(genls(c_tptpcol_9_26885, c_tptpcol_8_26629))],extension(33)).
% 249.15/240.83 cnf('1.1.2.1.2',plain,[-(genls(c_tptpcol_8_26629, c_tptpcol_1_1)), genls(c_tptpcol_8_26629, c_tptpcol_4_24578), genls(c_tptpcol_4_24578, c_tptpcol_1_1)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_8_26629, c_tptpcol_4_24578, c_tptpcol_1_1]]))).
% 249.15/240.83 cnf('1.1.2.1.2.1',plain,[-(genls(c_tptpcol_8_26629, c_tptpcol_4_24578)), genls(c_tptpcol_8_26629, c_tptpcol_6_26627), genls(c_tptpcol_6_26627, c_tptpcol_4_24578)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_8_26629, c_tptpcol_6_26627, c_tptpcol_4_24578]]))).
% 249.15/240.83 cnf('1.1.2.1.2.1.1',plain,[-(genls(c_tptpcol_8_26629, c_tptpcol_6_26627)), genls(c_tptpcol_8_26629, c_tptpcol_7_26628), genls(c_tptpcol_7_26628, c_tptpcol_6_26627)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_8_26629, c_tptpcol_7_26628, c_tptpcol_6_26627]]))).
% 249.15/240.83 cnf('1.1.2.1.2.1.1.1',plain,[-(genls(c_tptpcol_8_26629, c_tptpcol_7_26628))],extension(27)).
% 249.15/240.83 cnf('1.1.2.1.2.1.1.2',plain,[-(genls(c_tptpcol_7_26628, c_tptpcol_6_26627))],extension(32)).
% 249.15/240.83 cnf('1.1.2.1.2.1.2',plain,[-(genls(c_tptpcol_6_26627, c_tptpcol_4_24578)), genls(c_tptpcol_6_26627, c_tptpcol_5_24579), genls(c_tptpcol_5_24579, c_tptpcol_4_24578)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_6_26627, c_tptpcol_5_24579, c_tptpcol_4_24578]]))).
% 249.15/240.83 cnf('1.1.2.1.2.1.2.1',plain,[-(genls(c_tptpcol_6_26627, c_tptpcol_5_24579))],extension(36)).
% 249.15/240.83 cnf('1.1.2.1.2.1.2.2',plain,[-(genls(c_tptpcol_5_24579, c_tptpcol_4_24578))],extension(34)).
% 249.15/240.83 cnf('1.1.2.1.2.2',plain,[-(genls(c_tptpcol_4_24578, c_tptpcol_1_1)), genls(c_tptpcol_4_24578, c_tptpcol_2_2), genls(c_tptpcol_2_2, c_tptpcol_1_1)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_4_24578, c_tptpcol_2_2, c_tptpcol_1_1]]))).
% 249.15/240.83 cnf('1.1.2.1.2.2.1',plain,[-(genls(c_tptpcol_4_24578, c_tptpcol_2_2)), genls(c_tptpcol_4_24578, c_tptpcol_3_16386), genls(c_tptpcol_3_16386, c_tptpcol_2_2)],extension(3,bind([[_276252, _276308, _276363], [c_tptpcol_4_24578, c_tptpcol_3_16386, c_tptpcol_2_2]]))).
% 249.15/240.83 cnf('1.1.2.1.2.2.1.1',plain,[-(genls(c_tptpcol_4_24578, c_tptpcol_3_16386))],extension(29)).
% 249.15/240.83 cnf('1.1.2.1.2.2.1.2',plain,[-(genls(c_tptpcol_3_16386, c_tptpcol_2_2))],extension(15)).
% 249.15/240.83 cnf('1.1.2.1.2.2.2',plain,[-(genls(c_tptpcol_2_2, c_tptpcol_1_1))],extension(26)).
% 249.15/240.83 cnf('1.1.2.2',plain,[-(genls(c_tptpcol_1_1, c_tptpcol_1_1)), collection(c_tptpcol_1_1)],extension(13,bind([[_276951], [c_tptpcol_1_1]]))).
% 249.15/240.83 cnf('1.1.2.2.1',plain,[-(collection(c_tptpcol_1_1)), genls(c_tptpcol_4_16387, c_tptpcol_1_1)],extension(18,bind([[_275104, _275148], [c_tptpcol_4_16387, c_tptpcol_1_1]]))).
% 249.15/240.83 cnf('1.1.2.2.1.1',plain,[-(genls(c_tptpcol_4_16387, c_tptpcol_1_1)), genls(c_tptpcol_3_16386, c_tptpcol_1_1), genls(c_tptpcol_4_16387, c_tptpcol_3_16386)],extension(10,bind([[_277239, _277294, _277183], [c_tptpcol_1_1, c_tptpcol_4_16387, c_tptpcol_3_16386]]))).
% 249.15/240.83 cnf('1.1.2.2.1.1.1',plain,[-(genls(c_tptpcol_3_16386, c_tptpcol_1_1)), genls(c_tptpcol_2_2, c_tptpcol_1_1), genls(c_tptpcol_3_16386, c_tptpcol_2_2)],extension(10,bind([[_277239, _277294, _277183], [c_tptpcol_1_1, c_tptpcol_3_16386, c_tptpcol_2_2]]))).
% 249.15/240.83 cnf('1.1.2.2.1.1.1.1',plain,[-(genls(c_tptpcol_2_2, c_tptpcol_1_1))],extension(26)).
% 249.15/240.83 cnf('1.1.2.2.1.1.1.2',plain,[-(genls(c_tptpcol_3_16386, c_tptpcol_2_2))],extension(15)).
% 249.15/240.83 cnf('1.1.2.2.1.1.2',plain,[-(genls(c_tptpcol_4_16387, c_tptpcol_3_16386))],extension(6)).
% 249.15/240.83 %-----------------------------------------------------
% 249.15/240.84
% 249.15/240.84 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------