%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR061+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n021.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 21:05:02 EDT 2022
% Result : Theorem 29.88s 29.30s
% Output : Proof 29.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR061+1 : TPTP v8.1.0. Released v3.4.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Sat Jun 11 06:33:10 EDT 2022
% 0.13/0.34 % CPUTime :
% 29.88/29.30 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.88/29.31 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.88/29.32
% 29.88/29.32 %-----------------------------------------------------
% 29.88/29.32 fof(query61, conjecture, mtvisible(c_timehasnoendmt) => disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), file('/export/starexec/sandbox/benchmark/theBenchmark.p', query61)).
% 29.88/29.32 fof(just5, axiom, genls(c_tptpcol_4_106497, c_tptpcol_3_98305), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just5)).
% 29.88/29.32 fof(just7, axiom, genls(c_tptpcol_5_110593, c_tptpcol_4_106497), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just7)).
% 29.88/29.32 fof(just9, axiom, genls(c_tptpcol_6_112641, c_tptpcol_5_110593), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just9)).
% 29.88/29.32 fof(just11, axiom, genls(c_tptpcol_7_113665, c_tptpcol_6_112641), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just11)).
% 29.88/29.32 fof(just13, axiom, genls(c_tptpcol_8_114177, c_tptpcol_7_113665), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just13)).
% 29.88/29.32 fof(just15, axiom, genls(c_tptpcol_4_114689, c_tptpcol_3_114688), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just15)).
% 29.88/29.32 fof(just17, axiom, genls(c_tptpcol_5_114690, c_tptpcol_4_114689), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just17)).
% 29.88/29.32 fof(just19, axiom, genls(c_tptpcol_6_116738, c_tptpcol_5_114690), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just19)).
% 29.88/29.32 fof(just21, axiom, genls(c_tptpcol_7_117762, c_tptpcol_6_116738), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just21)).
% 29.88/29.32 fof(just23, axiom, genls(c_tptpcol_8_117763, c_tptpcol_7_117762), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just23)).
% 29.88/29.32 fof(just25, axiom, genls(c_tptpcol_9_118019, c_tptpcol_8_117763), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just25)).
% 29.88/29.32 fof(just27, axiom, genls(c_tptpcol_10_118020, c_tptpcol_9_118019), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just27)).
% 29.88/29.32 fof(just29, axiom, genls(c_tptpcol_11_118084, c_tptpcol_10_118020), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just29)).
% 29.88/29.32 fof(just31, axiom, genls(c_tptpcol_12_118116, c_tptpcol_11_118084), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just31)).
% 29.88/29.32 fof(just33, axiom, genls(c_tptpcol_13_118117, c_tptpcol_12_118116), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just33)).
% 29.88/29.32 fof(just35, axiom, genls(c_tptpcol_14_118118, c_tptpcol_13_118117), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just35)).
% 29.88/29.32 fof(just37, axiom, disjointwith(c_tptpcol_3_98305, c_tptpcol_3_114688), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just37)).
% 29.88/29.32 fof(just54, axiom, ! [_75510, _75513] : (disjointwith(_75510, _75513) => disjointwith(_75513, _75510)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just54)).
% 29.88/29.32 fof(just55, axiom, ! [_75656, _75659, _75662] : (disjointwith(_75656, _75659) & genls(_75662, _75659) => disjointwith(_75656, _75662)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just55)).
% 29.88/29.32 fof(just56, axiom, ! [_75841, _75844, _75847] : (disjointwith(_75841, _75844) & genls(_75847, _75841) => disjointwith(_75847, _75844)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just56)).
% 29.88/29.32 fof(just97, axiom, ! [_76066, _76069, _76072] : (genls(_76066, _76069) & genls(_76069, _76072) => genls(_76066, _76072)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', just97)).
% 29.88/29.32
% 29.88/29.32 cnf(1, plain, [disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118)], clausify(query61)).
% 29.88/29.32 cnf(2, plain, [-(genls(c_tptpcol_4_106497, c_tptpcol_3_98305))], clausify(just5)).
% 29.88/29.32 cnf(3, plain, [-(genls(c_tptpcol_5_110593, c_tptpcol_4_106497))], clausify(just7)).
% 29.88/29.32 cnf(4, plain, [-(genls(c_tptpcol_6_112641, c_tptpcol_5_110593))], clausify(just9)).
% 29.88/29.32 cnf(5, plain, [-(genls(c_tptpcol_7_113665, c_tptpcol_6_112641))], clausify(just11)).
% 29.88/29.32 cnf(6, plain, [-(genls(c_tptpcol_8_114177, c_tptpcol_7_113665))], clausify(just13)).
% 29.88/29.32 cnf(7, plain, [-(genls(c_tptpcol_4_114689, c_tptpcol_3_114688))], clausify(just15)).
% 29.88/29.32 cnf(8, plain, [-(genls(c_tptpcol_5_114690, c_tptpcol_4_114689))], clausify(just17)).
% 29.88/29.32 cnf(9, plain, [-(genls(c_tptpcol_6_116738, c_tptpcol_5_114690))], clausify(just19)).
% 29.88/29.32 cnf(10, plain, [-(genls(c_tptpcol_7_117762, c_tptpcol_6_116738))], clausify(just21)).
% 29.88/29.32 cnf(11, plain, [-(genls(c_tptpcol_8_117763, c_tptpcol_7_117762))], clausify(just23)).
% 29.88/29.32 cnf(12, plain, [-(genls(c_tptpcol_9_118019, c_tptpcol_8_117763))], clausify(just25)).
% 29.88/29.32 cnf(13, plain, [-(genls(c_tptpcol_10_118020, c_tptpcol_9_118019))], clausify(just27)).
% 29.88/29.32 cnf(14, plain, [-(genls(c_tptpcol_11_118084, c_tptpcol_10_118020))], clausify(just29)).
% 29.88/29.32 cnf(15, plain, [-(genls(c_tptpcol_12_118116, c_tptpcol_11_118084))], clausify(just31)).
% 29.88/29.32 cnf(16, plain, [-(genls(c_tptpcol_13_118117, c_tptpcol_12_118116))], clausify(just33)).
% 29.88/29.32 cnf(17, plain, [-(genls(c_tptpcol_14_118118, c_tptpcol_13_118117))], clausify(just35)).
% 29.88/29.32 cnf(18, plain, [-(disjointwith(c_tptpcol_3_98305, c_tptpcol_3_114688))], clausify(just37)).
% 29.88/29.32 cnf(19, plain, [disjointwith(_30861, _30906), -(disjointwith(_30906, _30861))], clausify(just54)).
% 29.88/29.32 cnf(20, plain, [-(disjointwith(_31171, _31282)), disjointwith(_31171, _31227), genls(_31282, _31227)], clausify(just55)).
% 29.88/29.32 cnf(21, plain, [-(disjointwith(_31749, _31694)), disjointwith(_31638, _31694), genls(_31749, _31638)], clausify(just56)).
% 29.88/29.32 cnf(22, plain, [-(genls(_41605, _41716)), genls(_41605, _41661), genls(_41661, _41716)], clausify(just97)).
% 29.88/29.32
% 29.88/29.32 cnf('1',plain,[disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118)],start(1)).
% 29.88/29.32 cnf('1.1',plain,[-(disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118)), disjointwith(c_tptpcol_14_118118, c_tptpcol_8_114177)],extension(19,bind([[_30861, _30906], [c_tptpcol_14_118118, c_tptpcol_8_114177]]))).
% 29.88/29.32 cnf('1.1.1',plain,[-(disjointwith(c_tptpcol_14_118118, c_tptpcol_8_114177)), disjointwith(c_tptpcol_5_114690, c_tptpcol_8_114177), genls(c_tptpcol_14_118118, c_tptpcol_5_114690)],extension(21,bind([[_31694, _31749, _31638], [c_tptpcol_8_114177, c_tptpcol_14_118118, c_tptpcol_5_114690]]))).
% 29.88/29.32 cnf('1.1.1.1',plain,[-(disjointwith(c_tptpcol_5_114690, c_tptpcol_8_114177)), disjointwith(c_tptpcol_8_114177, c_tptpcol_5_114690)],extension(19,bind([[_30861, _30906], [c_tptpcol_8_114177, c_tptpcol_5_114690]]))).
% 29.88/29.32 cnf('1.1.1.1.1',plain,[-(disjointwith(c_tptpcol_8_114177, c_tptpcol_5_114690)), disjointwith(c_tptpcol_8_114177, c_tptpcol_4_114689), genls(c_tptpcol_5_114690, c_tptpcol_4_114689)],extension(20,bind([[_31171, _31282, _31227], [c_tptpcol_8_114177, c_tptpcol_5_114690, c_tptpcol_4_114689]]))).
% 29.88/29.32 cnf('1.1.1.1.1.1',plain,[-(disjointwith(c_tptpcol_8_114177, c_tptpcol_4_114689)), disjointwith(c_tptpcol_8_114177, c_tptpcol_3_114688), genls(c_tptpcol_4_114689, c_tptpcol_3_114688)],extension(20,bind([[_31171, _31282, _31227], [c_tptpcol_8_114177, c_tptpcol_4_114689, c_tptpcol_3_114688]]))).
% 29.88/29.32 cnf('1.1.1.1.1.1.1',plain,[-(disjointwith(c_tptpcol_8_114177, c_tptpcol_3_114688)), disjointwith(c_tptpcol_3_98305, c_tptpcol_3_114688), genls(c_tptpcol_8_114177, c_tptpcol_3_98305)],extension(21,bind([[_31694, _31749, _31638], [c_tptpcol_3_114688, c_tptpcol_8_114177, c_tptpcol_3_98305]]))).
% 29.88/29.32 cnf('1.1.1.1.1.1.1.1',plain,[-(disjointwith(c_tptpcol_3_98305, c_tptpcol_3_114688))],extension(18)).
% 29.88/29.32 cnf('1.1.1.1.1.1.1.2',plain,[-(genls(c_tptpcol_8_114177, c_tptpcol_3_98305)), genls(c_tptpcol_8_114177, c_tptpcol_7_113665), genls(c_tptpcol_7_113665, c_tptpcol_3_98305)],extension(22,bind([[_41605, _41661, _41716], [c_tptpcol_8_114177, c_tptpcol_7_113665, c_tptpcol_3_98305]]))).
% 29.88/29.32 cnf('1.1.1.1.1.1.1.2.1',plain,[-(genls(c_tptpcol_8_114177, c_tptpcol_7_113665))],extension(6)).
% 29.88/29.32 cnf('1.1.1.1.1.1.1.2.2',plain,[-(genls(c_tptpcol_7_113665, c_tptpcol_3_98305)), genls(c_tptpcol_7_113665, c_tptpcol_6_112641), genls(c_tptpcol_6_112641, c_tptpcol_3_98305)],extension(22,bind([[_41605, _41661, _41716], [c_tptpcol_7_113665, c_tptpcol_6_112641, c_tptpcol_3_98305]]))).
% 29.88/29.32 cnf('1.1.1.1.1.1.1.2.2.1',plain,[-(genls(c_tptpcol_7_113665, c_tptpcol_6_112641))],extension(5)).
% 29.88/29.32 cnf('1.1.1.1.1.1.1.2.2.2',plain,[-(genls(c_tptpcol_6_112641, c_tptpcol_3_98305)), genls(c_tptpcol_6_112641, c_tptpcol_5_110593), genls(c_tptpcol_5_110593, c_tptpcol_3_98305)],extension(22,bind([[_41605, _41661, _41716], [c_tptpcol_6_112641, c_tptpcol_5_110593, c_tptpcol_3_98305]]))).
% 29.88/29.32 cnf('1.1.1.1.1.1.1.2.2.2.1',plain,[-(genls(c_tptpcol_6_112641, c_tptpcol_5_110593))],extension(4)).
% 29.88/29.32 cnf('1.1.1.1.1.1.1.2.2.2.2',plain,[-(genls(c_tptpcol_5_110593, c_tptpcol_3_98305)), genls(c_tptpcol_5_110593, c_tptpcol_4_106497), genls(c_tptpcol_4_106497, c_tptpcol_3_98305)],extension(22,bind([[_41605, _41661, _41716], [c_tptpcol_5_110593, c_tptpcol_4_106497, c_tptpcol_3_98305]]))).
% 29.88/29.32 cnf('1.1.1.1.1.1.1.2.2.2.2.1',plain,[-(genls(c_tptpcol_5_110593, c_tptpcol_4_106497))],extension(3)).
% 29.88/29.32 cnf('1.1.1.1.1.1.1.2.2.2.2.2',plain,[-(genls(c_tptpcol_4_106497, c_tptpcol_3_98305))],extension(2)).
% 29.88/29.32 cnf('1.1.1.1.1.1.2',plain,[-(genls(c_tptpcol_4_114689, c_tptpcol_3_114688))],extension(7)).
% 29.88/29.32 cnf('1.1.1.1.1.2',plain,[-(genls(c_tptpcol_5_114690, c_tptpcol_4_114689))],extension(8)).
% 29.88/29.32 cnf('1.1.1.2',plain,[-(genls(c_tptpcol_14_118118, c_tptpcol_5_114690)), genls(c_tptpcol_14_118118, c_tptpcol_13_118117), genls(c_tptpcol_13_118117, c_tptpcol_5_114690)],extension(22,bind([[_41605, _41661, _41716], [c_tptpcol_14_118118, c_tptpcol_13_118117, c_tptpcol_5_114690]]))).
% 29.88/29.32 cnf('1.1.1.2.1',plain,[-(genls(c_tptpcol_14_118118, c_tptpcol_13_118117))],extension(17)).
% 29.88/29.32 cnf('1.1.1.2.2',plain,[-(genls(c_tptpcol_13_118117, c_tptpcol_5_114690)), genls(c_tptpcol_13_118117, c_tptpcol_12_118116), genls(c_tptpcol_12_118116, c_tptpcol_5_114690)],extension(22,bind([[_41605, _41661, _41716], [c_tptpcol_13_118117, c_tptpcol_12_118116, c_tptpcol_5_114690]]))).
% 29.88/29.32 cnf('1.1.1.2.2.1',plain,[-(genls(c_tptpcol_13_118117, c_tptpcol_12_118116))],extension(16)).
% 29.88/29.32 cnf('1.1.1.2.2.2',plain,[-(genls(c_tptpcol_12_118116, c_tptpcol_5_114690)), genls(c_tptpcol_12_118116, c_tptpcol_11_118084), genls(c_tptpcol_11_118084, c_tptpcol_5_114690)],extension(22,bind([[_41605, _41661, _41716], [c_tptpcol_12_118116, c_tptpcol_11_118084, c_tptpcol_5_114690]]))).
% 29.88/29.32 cnf('1.1.1.2.2.2.1',plain,[-(genls(c_tptpcol_12_118116, c_tptpcol_11_118084))],extension(15)).
% 29.88/29.32 cnf('1.1.1.2.2.2.2',plain,[-(genls(c_tptpcol_11_118084, c_tptpcol_5_114690)), genls(c_tptpcol_11_118084, c_tptpcol_10_118020), genls(c_tptpcol_10_118020, c_tptpcol_5_114690)],extension(22,bind([[_41605, _41661, _41716], [c_tptpcol_11_118084, c_tptpcol_10_118020, c_tptpcol_5_114690]]))).
% 29.88/29.32 cnf('1.1.1.2.2.2.2.1',plain,[-(genls(c_tptpcol_11_118084, c_tptpcol_10_118020))],extension(14)).
% 29.88/29.32 cnf('1.1.1.2.2.2.2.2',plain,[-(genls(c_tptpcol_10_118020, c_tptpcol_5_114690)), genls(c_tptpcol_10_118020, c_tptpcol_9_118019), genls(c_tptpcol_9_118019, c_tptpcol_5_114690)],extension(22,bind([[_41605, _41661, _41716], [c_tptpcol_10_118020, c_tptpcol_9_118019, c_tptpcol_5_114690]]))).
% 29.88/29.32 cnf('1.1.1.2.2.2.2.2.1',plain,[-(genls(c_tptpcol_10_118020, c_tptpcol_9_118019))],extension(13)).
% 29.88/29.32 cnf('1.1.1.2.2.2.2.2.2',plain,[-(genls(c_tptpcol_9_118019, c_tptpcol_5_114690)), genls(c_tptpcol_9_118019, c_tptpcol_8_117763), genls(c_tptpcol_8_117763, c_tptpcol_5_114690)],extension(22,bind([[_41605, _41661, _41716], [c_tptpcol_9_118019, c_tptpcol_8_117763, c_tptpcol_5_114690]]))).
% 29.88/29.32 cnf('1.1.1.2.2.2.2.2.2.1',plain,[-(genls(c_tptpcol_9_118019, c_tptpcol_8_117763))],extension(12)).
% 29.88/29.32 cnf('1.1.1.2.2.2.2.2.2.2',plain,[-(genls(c_tptpcol_8_117763, c_tptpcol_5_114690)), genls(c_tptpcol_8_117763, c_tptpcol_7_117762), genls(c_tptpcol_7_117762, c_tptpcol_5_114690)],extension(22,bind([[_41605, _41661, _41716], [c_tptpcol_8_117763, c_tptpcol_7_117762, c_tptpcol_5_114690]]))).
% 29.88/29.32 cnf('1.1.1.2.2.2.2.2.2.2.1',plain,[-(genls(c_tptpcol_8_117763, c_tptpcol_7_117762))],extension(11)).
% 29.88/29.32 cnf('1.1.1.2.2.2.2.2.2.2.2',plain,[-(genls(c_tptpcol_7_117762, c_tptpcol_5_114690)), genls(c_tptpcol_7_117762, c_tptpcol_6_116738), genls(c_tptpcol_6_116738, c_tptpcol_5_114690)],extension(22,bind([[_41605, _41661, _41716], [c_tptpcol_7_117762, c_tptpcol_6_116738, c_tptpcol_5_114690]]))).
% 29.88/29.32 cnf('1.1.1.2.2.2.2.2.2.2.2.1',plain,[-(genls(c_tptpcol_7_117762, c_tptpcol_6_116738))],extension(10)).
% 29.88/29.32 cnf('1.1.1.2.2.2.2.2.2.2.2.2',plain,[-(genls(c_tptpcol_6_116738, c_tptpcol_5_114690))],extension(9)).
% 29.88/29.32 %-----------------------------------------------------
% 29.88/29.32
% 29.88/29.32 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------