%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR036+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n013.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:46:39 EDT 2022
% Result : Theorem 201.46s 195.04s
% Output : Proof 201.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.12 % Problem : CSR036+1 : TPTP v8.1.0. Released v3.4.0.
% 0.12/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n013.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 : 600
% 0.12/0.33 % DateTime : Sat Jun 11 13:33:44 EDT 2022
% 0.12/0.33 % CPUTime :
% 201.46/195.04 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 201.46/195.05 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 201.46/195.05
% 201.46/195.05 %-----------------------------------------------------
% 201.46/195.05 fof(just8, axiom, genls(c_tptpcol_3_16386, c_tptpcol_2_2), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just8)).
% 201.46/195.05 fof(just84, axiom, ! [_113524, _113527, _113530] : (disjointwith(_113524, _113527) & genls(_113530, _113527) => disjointwith(_113524, _113530)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just84)).
% 201.46/195.05 fof(just44, axiom, genls(c_tptpcol_7_72707, c_tptpcol_6_71683), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just44)).
% 201.46/195.05 fof(just24, axiom, genls(c_tptpcol_11_22023, c_tptpcol_10_22022), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just24)).
% 201.46/195.05 fof(just30, axiom, genls(c_tptpcol_14_22072, c_tptpcol_13_22071), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just30)).
% 201.46/195.05 fof(just42, axiom, genls(c_tptpcol_6_71683, c_tptpcol_5_69635), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just42)).
% 201.46/195.05 fof(just60, axiom, genls(c_tptpcol_15_72793, c_tptpcol_14_72792), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just60)).
% 201.46/195.05 fof(just46, axiom, genls(c_tptpcol_8_72708, c_tptpcol_7_72707), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just46)).
% 201.46/195.05 fof(just50, axiom, genls(c_tptpcol_10_72710, c_tptpcol_9_72709), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just50)).
% 201.46/195.05 fof(just148, axiom, ! [_114088, _114091] : (genls(_114088, _114091) => collection(_114091)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just148)).
% 201.46/195.05 fof(just18, axiom, genls(c_tptpcol_8_22020, c_tptpcol_7_21508), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just18)).
% 201.46/195.05 fof(just54, axiom, genls(c_tptpcol_12_72775, c_tptpcol_11_72774), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just54)).
% 201.46/195.05 fof(just156, axiom, ! [_114335, _114338, _114341] : (genls(_114335, _114338) & genls(_114338, _114341) => genls(_114335, _114341)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just156)).
% 201.46/195.05 fof(just34, axiom, genls(c_tptpcol_2_65537, c_tptpcol_1_65536), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just34)).
% 201.46/195.05 fof(just10, axiom, genls(c_tptpcol_4_16387, c_tptpcol_3_16386), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just10)).
% 201.46/195.05 fof(just16, axiom, genls(c_tptpcol_7_21508, c_tptpcol_6_20484), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just16)).
% 201.46/195.05 fof(just56, axiom, genls(c_tptpcol_13_72791, c_tptpcol_12_72775), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just56)).
% 201.46/195.05 fof(just26, axiom, genls(c_tptpcol_12_22055, c_tptpcol_11_22023), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just26)).
% 201.46/195.05 fof(just36, axiom, genls(c_tptpcol_3_65538, c_tptpcol_2_65537), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just36)).
% 201.46/195.05 fof(just85, axiom, ! [_114847, _114850, _114853] : (disjointwith(_114847, _114850) & genls(_114853, _114847) => disjointwith(_114853, _114850)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just85)).
% 201.46/195.05 fof(query36, conjecture, mtvisible(c_tptp_member974_mt) => disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', query36)).
% 201.46/195.05 fof(just64, axiom, disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just64)).
% 201.46/195.05 fof(just38, axiom, genls(c_tptpcol_4_65539, c_tptpcol_3_65538), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just38)).
% 201.46/195.05 fof(just153, axiom, ! [_115214] : (collection(_115214) => genls(_115214, _115214)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just153)).
% 201.46/195.05 fof(just155, axiom, ! [_115345, _115348, _115351] : (genls(_115345, _115348) & genls(_115351, _115345) => genls(_115351, _115348)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just155)).
% 201.46/195.05 fof(just58, axiom, genls(c_tptpcol_14_72792, c_tptpcol_13_72791), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just58)).
% 201.46/195.05 fof(just12, axiom, genls(c_tptpcol_5_20483, c_tptpcol_4_16387), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just12)).
% 201.46/195.05 fof(just20, axiom, genls(c_tptpcol_9_22021, c_tptpcol_8_22020), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just20)).
% 201.46/195.05 fof(just22, axiom, genls(c_tptpcol_10_22022, c_tptpcol_9_22021), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just22)).
% 201.46/195.05 fof(just40, axiom, genls(c_tptpcol_5_69635, c_tptpcol_4_65539), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just40)).
% 201.46/195.05 fof(just62, axiom, genls(c_tptpcol_16_72795, c_tptpcol_15_72793), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just62)).
% 201.46/195.05 fof(just48, axiom, genls(c_tptpcol_9_72709, c_tptpcol_8_72708), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just48)).
% 201.46/195.05 fof(just6, axiom, genls(c_tptpcol_2_2, c_tptpcol_1_1), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just6)).
% 201.46/195.05 fof(just32, axiom, genls(c_tptpcol_15_22076, c_tptpcol_14_22072), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just32)).
% 201.46/195.05 fof(just52, axiom, genls(c_tptpcol_11_72774, c_tptpcol_10_72710), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just52)).
% 201.46/195.05 fof(just28, axiom, genls(c_tptpcol_13_22071, c_tptpcol_12_22055), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just28)).
% 201.46/195.05 fof(just14, axiom, genls(c_tptpcol_6_20484, c_tptpcol_5_20483), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just14)).
% 201.46/195.05
% 201.46/195.05 cnf(1, plain, [-(genls(c_tptpcol_3_16386, c_tptpcol_2_2))], clausify(just8)).
% 201.46/195.05 cnf(2, plain, [-(disjointwith(_42471, _42582)), disjointwith(_42471, _42527), genls(_42582, _42527)], clausify(just84)).
% 201.46/195.05 cnf(3, plain, [-(genls(c_tptpcol_7_72707, c_tptpcol_6_71683))], clausify(just44)).
% 201.46/195.05 cnf(4, plain, [-(genls(c_tptpcol_11_22023, c_tptpcol_10_22022))], clausify(just24)).
% 201.46/195.05 cnf(5, plain, [-(genls(c_tptpcol_14_22072, c_tptpcol_13_22071))], clausify(just30)).
% 201.46/195.05 cnf(6, plain, [-(genls(c_tptpcol_6_71683, c_tptpcol_5_69635))], clausify(just42)).
% 201.46/195.05 cnf(7, plain, [-(genls(c_tptpcol_15_72793, c_tptpcol_14_72792))], clausify(just60)).
% 201.46/195.05 cnf(8, plain, [-(genls(c_tptpcol_8_72708, c_tptpcol_7_72707))], clausify(just46)).
% 201.46/195.05 cnf(9, plain, [-(genls(c_tptpcol_10_72710, c_tptpcol_9_72709))], clausify(just50)).
% 201.46/195.05 cnf(10, plain, [genls(_57789, _57833), -(collection(_57833))], clausify(just148)).
% 201.46/195.05 cnf(11, plain, [-(genls(c_tptpcol_8_22020, c_tptpcol_7_21508))], clausify(just18)).
% 201.46/195.05 cnf(12, plain, [-(genls(c_tptpcol_12_72775, c_tptpcol_11_72774))], clausify(just54)).
% 201.46/195.05 cnf(13, plain, [-(genls(_60335, _60446)), genls(_60335, _60391), genls(_60391, _60446)], clausify(just156)).
% 201.46/195.05 cnf(14, plain, [-(genls(c_tptpcol_2_65537, c_tptpcol_1_65536))], clausify(just34)).
% 201.46/195.05 cnf(15, plain, [-(genls(c_tptpcol_4_16387, c_tptpcol_3_16386))], clausify(just10)).
% 201.46/195.05 cnf(16, plain, [-(genls(c_tptpcol_7_21508, c_tptpcol_6_20484))], clausify(just16)).
% 201.46/195.05 cnf(17, plain, [-(genls(c_tptpcol_13_72791, c_tptpcol_12_72775))], clausify(just56)).
% 201.46/195.05 cnf(18, plain, [-(genls(c_tptpcol_12_22055, c_tptpcol_11_22023))], clausify(just26)).
% 201.46/195.05 cnf(19, plain, [-(genls(c_tptpcol_3_65538, c_tptpcol_2_65537))], clausify(just36)).
% 201.46/195.05 cnf(20, plain, [-(disjointwith(_43049, _42994)), disjointwith(_42938, _42994), genls(_43049, _42938)], clausify(just85)).
% 201.46/195.05 cnf(21, plain, [disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795)], clausify(query36)).
% 201.46/195.05 cnf(22, plain, [-(disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536))], clausify(just64)).
% 201.46/195.05 cnf(23, plain, [-(genls(c_tptpcol_4_65539, c_tptpcol_3_65538))], clausify(just38)).
% 201.46/195.05 cnf(24, plain, [collection(_59404), -(genls(_59404, _59404))], clausify(just153)).
% 201.46/195.05 cnf(25, plain, [-(genls(_59979, _59924)), genls(_59868, _59924), genls(_59979, _59868)], clausify(just155)).
% 201.46/195.05 cnf(26, plain, [-(genls(c_tptpcol_14_72792, c_tptpcol_13_72791))], clausify(just58)).
% 201.46/195.05 cnf(27, plain, [-(genls(c_tptpcol_5_20483, c_tptpcol_4_16387))], clausify(just12)).
% 201.46/195.05 cnf(28, plain, [-(genls(c_tptpcol_9_22021, c_tptpcol_8_22020))], clausify(just20)).
% 201.46/195.05 cnf(29, plain, [-(genls(c_tptpcol_10_22022, c_tptpcol_9_22021))], clausify(just22)).
% 201.46/195.05 cnf(30, plain, [-(genls(c_tptpcol_5_69635, c_tptpcol_4_65539))], clausify(just40)).
% 201.46/195.05 cnf(31, plain, [-(genls(c_tptpcol_16_72795, c_tptpcol_15_72793))], clausify(just62)).
% 201.46/195.05 cnf(32, plain, [-(genls(c_tptpcol_9_72709, c_tptpcol_8_72708))], clausify(just48)).
% 201.46/195.05 cnf(33, plain, [-(genls(c_tptpcol_2_2, c_tptpcol_1_1))], clausify(just6)).
% 201.46/195.05 cnf(34, plain, [-(genls(c_tptpcol_15_22076, c_tptpcol_14_22072))], clausify(just32)).
% 201.46/195.05 cnf(35, plain, [-(genls(c_tptpcol_11_72774, c_tptpcol_10_72710))], clausify(just52)).
% 201.46/195.05 cnf(36, plain, [-(genls(c_tptpcol_13_22071, c_tptpcol_12_22055))], clausify(just28)).
% 201.46/195.05 cnf(37, plain, [-(genls(c_tptpcol_6_20484, c_tptpcol_5_20483))], clausify(just14)).
% 201.46/195.05
% 201.46/195.05 cnf('1',plain,[disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795)],start(21)).
% 201.46/195.05 cnf('1.1',plain,[-(disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795)), disjointwith(c_tptpcol_1_1, c_tptpcol_16_72795), genls(c_tptpcol_15_22076, c_tptpcol_1_1)],extension(20,bind([[_42994, _43049, _42938], [c_tptpcol_16_72795, c_tptpcol_15_22076, c_tptpcol_1_1]]))).
% 201.46/195.05 cnf('1.1.1',plain,[-(disjointwith(c_tptpcol_1_1, c_tptpcol_16_72795)), disjointwith(c_tptpcol_1_1, c_tptpcol_4_65539), genls(c_tptpcol_16_72795, c_tptpcol_4_65539)],extension(2,bind([[_42471, _42582, _42527], [c_tptpcol_1_1, c_tptpcol_16_72795, c_tptpcol_4_65539]]))).
% 201.46/195.05 cnf('1.1.1.1',plain,[-(disjointwith(c_tptpcol_1_1, c_tptpcol_4_65539)), disjointwith(c_tptpcol_1_1, c_tptpcol_4_65539), genls(c_tptpcol_4_65539, c_tptpcol_4_65539)],extension(2,bind([[_42471, _42582, _42527], [c_tptpcol_1_1, c_tptpcol_4_65539, c_tptpcol_4_65539]]))).
% 201.46/195.05 cnf('1.1.1.1.1',plain,[-(disjointwith(c_tptpcol_1_1, c_tptpcol_4_65539)), disjointwith(c_tptpcol_1_1, c_tptpcol_3_65538), genls(c_tptpcol_4_65539, c_tptpcol_3_65538)],extension(2,bind([[_42471, _42582, _42527], [c_tptpcol_1_1, c_tptpcol_4_65539, c_tptpcol_3_65538]]))).
% 201.46/195.05 cnf('1.1.1.1.1.1',plain,[-(disjointwith(c_tptpcol_1_1, c_tptpcol_3_65538)), disjointwith(c_tptpcol_1_1, c_tptpcol_2_65537), genls(c_tptpcol_3_65538, c_tptpcol_2_65537)],extension(2,bind([[_42471, _42582, _42527], [c_tptpcol_1_1, c_tptpcol_3_65538, c_tptpcol_2_65537]]))).
% 201.46/195.05 cnf('1.1.1.1.1.1.1',plain,[-(disjointwith(c_tptpcol_1_1, c_tptpcol_2_65537)), disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536), genls(c_tptpcol_2_65537, c_tptpcol_1_65536)],extension(2,bind([[_42471, _42582, _42527], [c_tptpcol_1_1, c_tptpcol_2_65537, c_tptpcol_1_65536]]))).
% 201.46/195.05 cnf('1.1.1.1.1.1.1.1',plain,[-(disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536))],extension(22)).
% 201.46/195.05 cnf('1.1.1.1.1.1.1.2',plain,[-(genls(c_tptpcol_2_65537, c_tptpcol_1_65536))],extension(14)).
% 201.46/195.05 cnf('1.1.1.1.1.1.2',plain,[-(genls(c_tptpcol_3_65538, c_tptpcol_2_65537))],extension(19)).
% 201.46/195.05 cnf('1.1.1.1.1.2',plain,[-(genls(c_tptpcol_4_65539, c_tptpcol_3_65538))],extension(23)).
% 201.46/195.05 cnf('1.1.1.1.2',plain,[-(genls(c_tptpcol_4_65539, c_tptpcol_4_65539)), collection(c_tptpcol_4_65539)],extension(24,bind([[_59404], [c_tptpcol_4_65539]]))).
% 201.46/195.05 cnf('1.1.1.1.2.1',plain,[-(collection(c_tptpcol_4_65539)), genls(c_tptpcol_6_71683, c_tptpcol_4_65539)],extension(10,bind([[_57789, _57833], [c_tptpcol_6_71683, c_tptpcol_4_65539]]))).
% 201.46/195.05 cnf('1.1.1.1.2.1.1',plain,[-(genls(c_tptpcol_6_71683, c_tptpcol_4_65539)), genls(c_tptpcol_5_69635, c_tptpcol_4_65539), genls(c_tptpcol_6_71683, c_tptpcol_5_69635)],extension(25,bind([[_59924, _59979, _59868], [c_tptpcol_4_65539, c_tptpcol_6_71683, c_tptpcol_5_69635]]))).
% 201.46/195.05 cnf('1.1.1.1.2.1.1.1',plain,[-(genls(c_tptpcol_5_69635, c_tptpcol_4_65539))],extension(30)).
% 201.46/195.05 cnf('1.1.1.1.2.1.1.2',plain,[-(genls(c_tptpcol_6_71683, c_tptpcol_5_69635))],extension(6)).
% 201.46/195.05 cnf('1.1.1.2',plain,[-(genls(c_tptpcol_16_72795, c_tptpcol_4_65539)), genls(c_tptpcol_16_72795, c_tptpcol_11_72774), genls(c_tptpcol_11_72774, c_tptpcol_4_65539)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_16_72795, c_tptpcol_11_72774, c_tptpcol_4_65539]]))).
% 201.46/195.05 cnf('1.1.1.2.1',plain,[-(genls(c_tptpcol_16_72795, c_tptpcol_11_72774)), genls(c_tptpcol_16_72795, c_tptpcol_12_72775), genls(c_tptpcol_12_72775, c_tptpcol_11_72774)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_16_72795, c_tptpcol_12_72775, c_tptpcol_11_72774]]))).
% 201.46/195.05 cnf('1.1.1.2.1.1',plain,[-(genls(c_tptpcol_16_72795, c_tptpcol_12_72775)), genls(c_tptpcol_16_72795, c_tptpcol_14_72792), genls(c_tptpcol_14_72792, c_tptpcol_12_72775)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_16_72795, c_tptpcol_14_72792, c_tptpcol_12_72775]]))).
% 201.46/195.05 cnf('1.1.1.2.1.1.1',plain,[-(genls(c_tptpcol_16_72795, c_tptpcol_14_72792)), genls(c_tptpcol_16_72795, c_tptpcol_15_72793), genls(c_tptpcol_15_72793, c_tptpcol_14_72792)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_16_72795, c_tptpcol_15_72793, c_tptpcol_14_72792]]))).
% 201.46/195.05 cnf('1.1.1.2.1.1.1.1',plain,[-(genls(c_tptpcol_16_72795, c_tptpcol_15_72793))],extension(31)).
% 201.46/195.05 cnf('1.1.1.2.1.1.1.2',plain,[-(genls(c_tptpcol_15_72793, c_tptpcol_14_72792))],extension(7)).
% 201.46/195.05 cnf('1.1.1.2.1.1.2',plain,[-(genls(c_tptpcol_14_72792, c_tptpcol_12_72775)), genls(c_tptpcol_14_72792, c_tptpcol_13_72791), genls(c_tptpcol_13_72791, c_tptpcol_12_72775)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_14_72792, c_tptpcol_13_72791, c_tptpcol_12_72775]]))).
% 201.46/195.05 cnf('1.1.1.2.1.1.2.1',plain,[-(genls(c_tptpcol_14_72792, c_tptpcol_13_72791))],extension(26)).
% 201.46/195.05 cnf('1.1.1.2.1.1.2.2',plain,[-(genls(c_tptpcol_13_72791, c_tptpcol_12_72775))],extension(17)).
% 201.46/195.05 cnf('1.1.1.2.1.2',plain,[-(genls(c_tptpcol_12_72775, c_tptpcol_11_72774))],extension(12)).
% 201.46/195.05 cnf('1.1.1.2.2',plain,[-(genls(c_tptpcol_11_72774, c_tptpcol_4_65539)), genls(c_tptpcol_11_72774, c_tptpcol_7_72707), genls(c_tptpcol_7_72707, c_tptpcol_4_65539)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_11_72774, c_tptpcol_7_72707, c_tptpcol_4_65539]]))).
% 201.46/195.05 cnf('1.1.1.2.2.1',plain,[-(genls(c_tptpcol_11_72774, c_tptpcol_7_72707)), genls(c_tptpcol_11_72774, c_tptpcol_9_72709), genls(c_tptpcol_9_72709, c_tptpcol_7_72707)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_11_72774, c_tptpcol_9_72709, c_tptpcol_7_72707]]))).
% 201.46/195.05 cnf('1.1.1.2.2.1.1',plain,[-(genls(c_tptpcol_11_72774, c_tptpcol_9_72709)), genls(c_tptpcol_11_72774, c_tptpcol_10_72710), genls(c_tptpcol_10_72710, c_tptpcol_9_72709)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_11_72774, c_tptpcol_10_72710, c_tptpcol_9_72709]]))).
% 201.46/195.05 cnf('1.1.1.2.2.1.1.1',plain,[-(genls(c_tptpcol_11_72774, c_tptpcol_10_72710))],extension(35)).
% 201.46/195.05 cnf('1.1.1.2.2.1.1.2',plain,[-(genls(c_tptpcol_10_72710, c_tptpcol_9_72709))],extension(9)).
% 201.46/195.05 cnf('1.1.1.2.2.1.2',plain,[-(genls(c_tptpcol_9_72709, c_tptpcol_7_72707)), genls(c_tptpcol_9_72709, c_tptpcol_8_72708), genls(c_tptpcol_8_72708, c_tptpcol_7_72707)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_9_72709, c_tptpcol_8_72708, c_tptpcol_7_72707]]))).
% 201.46/195.05 cnf('1.1.1.2.2.1.2.1',plain,[-(genls(c_tptpcol_9_72709, c_tptpcol_8_72708))],extension(32)).
% 201.46/195.05 cnf('1.1.1.2.2.1.2.2',plain,[-(genls(c_tptpcol_8_72708, c_tptpcol_7_72707))],extension(8)).
% 201.46/195.05 cnf('1.1.1.2.2.2',plain,[-(genls(c_tptpcol_7_72707, c_tptpcol_4_65539)), genls(c_tptpcol_7_72707, c_tptpcol_6_71683), genls(c_tptpcol_6_71683, c_tptpcol_4_65539)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_7_72707, c_tptpcol_6_71683, c_tptpcol_4_65539]]))).
% 201.46/195.05 cnf('1.1.1.2.2.2.1',plain,[-(genls(c_tptpcol_7_72707, c_tptpcol_6_71683))],extension(3)).
% 201.46/195.05 cnf('1.1.1.2.2.2.2',plain,[-(genls(c_tptpcol_6_71683, c_tptpcol_4_65539)), genls(c_tptpcol_6_71683, c_tptpcol_5_69635), genls(c_tptpcol_5_69635, c_tptpcol_4_65539)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_6_71683, c_tptpcol_5_69635, c_tptpcol_4_65539]]))).
% 201.46/195.06 cnf('1.1.1.2.2.2.2.1',plain,[-(genls(c_tptpcol_6_71683, c_tptpcol_5_69635))],extension(6)).
% 201.46/195.06 cnf('1.1.1.2.2.2.2.2',plain,[-(genls(c_tptpcol_5_69635, c_tptpcol_4_65539))],extension(30)).
% 201.46/195.06 cnf('1.1.2',plain,[-(genls(c_tptpcol_15_22076, c_tptpcol_1_1)), genls(c_tptpcol_15_22076, c_tptpcol_3_16386), genls(c_tptpcol_3_16386, c_tptpcol_1_1)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_15_22076, c_tptpcol_3_16386, c_tptpcol_1_1]]))).
% 201.46/195.06 cnf('1.1.2.1',plain,[-(genls(c_tptpcol_15_22076, c_tptpcol_3_16386)), genls(c_tptpcol_15_22076, c_tptpcol_10_22022), genls(c_tptpcol_10_22022, c_tptpcol_3_16386)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_15_22076, c_tptpcol_10_22022, c_tptpcol_3_16386]]))).
% 201.46/195.06 cnf('1.1.2.1.1',plain,[-(genls(c_tptpcol_15_22076, c_tptpcol_10_22022)), genls(c_tptpcol_15_22076, c_tptpcol_11_22023), genls(c_tptpcol_11_22023, c_tptpcol_10_22022)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_15_22076, c_tptpcol_11_22023, c_tptpcol_10_22022]]))).
% 201.46/195.06 cnf('1.1.2.1.1.1',plain,[-(genls(c_tptpcol_15_22076, c_tptpcol_11_22023)), genls(c_tptpcol_15_22076, c_tptpcol_13_22071), genls(c_tptpcol_13_22071, c_tptpcol_11_22023)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_15_22076, c_tptpcol_13_22071, c_tptpcol_11_22023]]))).
% 201.46/195.06 cnf('1.1.2.1.1.1.1',plain,[-(genls(c_tptpcol_15_22076, c_tptpcol_13_22071)), genls(c_tptpcol_15_22076, c_tptpcol_14_22072), genls(c_tptpcol_14_22072, c_tptpcol_13_22071)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_15_22076, c_tptpcol_14_22072, c_tptpcol_13_22071]]))).
% 201.46/195.06 cnf('1.1.2.1.1.1.1.1',plain,[-(genls(c_tptpcol_15_22076, c_tptpcol_14_22072))],extension(34)).
% 201.46/195.06 cnf('1.1.2.1.1.1.1.2',plain,[-(genls(c_tptpcol_14_22072, c_tptpcol_13_22071))],extension(5)).
% 201.46/195.06 cnf('1.1.2.1.1.1.2',plain,[-(genls(c_tptpcol_13_22071, c_tptpcol_11_22023)), genls(c_tptpcol_13_22071, c_tptpcol_12_22055), genls(c_tptpcol_12_22055, c_tptpcol_11_22023)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_13_22071, c_tptpcol_12_22055, c_tptpcol_11_22023]]))).
% 201.46/195.06 cnf('1.1.2.1.1.1.2.1',plain,[-(genls(c_tptpcol_13_22071, c_tptpcol_12_22055))],extension(36)).
% 201.46/195.06 cnf('1.1.2.1.1.1.2.2',plain,[-(genls(c_tptpcol_12_22055, c_tptpcol_11_22023))],extension(18)).
% 201.46/195.06 cnf('1.1.2.1.1.2',plain,[-(genls(c_tptpcol_11_22023, c_tptpcol_10_22022))],extension(4)).
% 201.46/195.06 cnf('1.1.2.1.2',plain,[-(genls(c_tptpcol_10_22022, c_tptpcol_3_16386)), genls(c_tptpcol_10_22022, c_tptpcol_7_21508), genls(c_tptpcol_7_21508, c_tptpcol_3_16386)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_10_22022, c_tptpcol_7_21508, c_tptpcol_3_16386]]))).
% 201.46/195.06 cnf('1.1.2.1.2.1',plain,[-(genls(c_tptpcol_10_22022, c_tptpcol_7_21508)), genls(c_tptpcol_10_22022, c_tptpcol_8_22020), genls(c_tptpcol_8_22020, c_tptpcol_7_21508)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_10_22022, c_tptpcol_8_22020, c_tptpcol_7_21508]]))).
% 201.46/195.06 cnf('1.1.2.1.2.1.1',plain,[-(genls(c_tptpcol_10_22022, c_tptpcol_8_22020)), genls(c_tptpcol_10_22022, c_tptpcol_9_22021), genls(c_tptpcol_9_22021, c_tptpcol_8_22020)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_10_22022, c_tptpcol_9_22021, c_tptpcol_8_22020]]))).
% 201.46/195.06 cnf('1.1.2.1.2.1.1.1',plain,[-(genls(c_tptpcol_10_22022, c_tptpcol_9_22021))],extension(29)).
% 201.46/195.06 cnf('1.1.2.1.2.1.1.2',plain,[-(genls(c_tptpcol_9_22021, c_tptpcol_8_22020))],extension(28)).
% 201.46/195.06 cnf('1.1.2.1.2.1.2',plain,[-(genls(c_tptpcol_8_22020, c_tptpcol_7_21508))],extension(11)).
% 201.46/195.06 cnf('1.1.2.1.2.2',plain,[-(genls(c_tptpcol_7_21508, c_tptpcol_3_16386)), genls(c_tptpcol_7_21508, c_tptpcol_5_20483), genls(c_tptpcol_5_20483, c_tptpcol_3_16386)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_7_21508, c_tptpcol_5_20483, c_tptpcol_3_16386]]))).
% 201.46/195.06 cnf('1.1.2.1.2.2.1',plain,[-(genls(c_tptpcol_7_21508, c_tptpcol_5_20483)), genls(c_tptpcol_7_21508, c_tptpcol_6_20484), genls(c_tptpcol_6_20484, c_tptpcol_5_20483)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_7_21508, c_tptpcol_6_20484, c_tptpcol_5_20483]]))).
% 201.46/195.06 cnf('1.1.2.1.2.2.1.1',plain,[-(genls(c_tptpcol_7_21508, c_tptpcol_6_20484))],extension(16)).
% 201.46/195.06 cnf('1.1.2.1.2.2.1.2',plain,[-(genls(c_tptpcol_6_20484, c_tptpcol_5_20483))],extension(37)).
% 201.46/195.06 cnf('1.1.2.1.2.2.2',plain,[-(genls(c_tptpcol_5_20483, c_tptpcol_3_16386)), genls(c_tptpcol_5_20483, c_tptpcol_4_16387), genls(c_tptpcol_4_16387, c_tptpcol_3_16386)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_5_20483, c_tptpcol_4_16387, c_tptpcol_3_16386]]))).
% 201.46/195.06 cnf('1.1.2.1.2.2.2.1',plain,[-(genls(c_tptpcol_5_20483, c_tptpcol_4_16387))],extension(27)).
% 201.46/195.06 cnf('1.1.2.1.2.2.2.2',plain,[-(genls(c_tptpcol_4_16387, c_tptpcol_3_16386))],extension(15)).
% 201.46/195.06 cnf('1.1.2.2',plain,[-(genls(c_tptpcol_3_16386, c_tptpcol_1_1)), genls(c_tptpcol_3_16386, c_tptpcol_2_2), genls(c_tptpcol_2_2, c_tptpcol_1_1)],extension(13,bind([[_60335, _60391, _60446], [c_tptpcol_3_16386, c_tptpcol_2_2, c_tptpcol_1_1]]))).
% 201.46/195.06 cnf('1.1.2.2.1',plain,[-(genls(c_tptpcol_3_16386, c_tptpcol_2_2))],extension(1)).
% 201.46/195.06 cnf('1.1.2.2.2',plain,[-(genls(c_tptpcol_2_2, c_tptpcol_1_1))],extension(33)).
% 201.46/195.06 %-----------------------------------------------------
% 201.46/195.06
% 201.46/195.06 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------