%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR033+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n015.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:44:23 EDT 2022
% Result : Theorem 0.34s 1.40s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CSR033+1 : TPTP v8.1.0. Released v3.4.0.
% 0.11/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n015.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Sat Jun 11 14:03:36 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.34/1.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.41
% 0.34/1.41 %-----------------------------------------------------
% 0.34/1.41 fof(query33, conjecture, mtvisible(c_tptpgeo_spindlecollectormt) => inregion(c_geolocation_x76_y23, c_georegion_l1_x2_y0) & geolevel_1(c_georegion_l1_x2_y0), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', query33)).
% 0.34/1.41 fof(just5, axiom, ! [_44124, _44127] : (geographicalsubregions(_44124, _44127) => inregion(_44127, _44124)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just5)).
% 0.34/1.41 fof(just8, axiom, genlmt(c_tptpgeo_spindleheadmt, c_worldgeographymt), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just8)).
% 0.34/1.41 fof(just9, axiom, genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just9)).
% 0.34/1.41 fof(just10, axiom, genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just10)).
% 0.34/1.41 fof(just11, axiom, genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member8_mt), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just11)).
% 0.34/1.41 fof(just12, axiom, mtvisible(c_worldgeographymt) => geolevel_1(c_georegion_l1_x2_y0), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just12)).
% 0.34/1.41 fof(just13, axiom, mtvisible(c_tptpgeo_member2_mt) => geographicalsubregions(c_georegion_l1_x2_y0, c_georegion_l2_x8_y2), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just13)).
% 0.34/1.41 fof(just14, axiom, mtvisible(c_tptpgeo_member2_mt) => geographicalsubregions(c_georegion_l2_x8_y2, c_georegion_l3_x25_y7), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just14)).
% 0.34/1.41 fof(just15, axiom, mtvisible(c_tptpgeo_member2_mt) => geographicalsubregions(c_georegion_l3_x25_y7, c_georegion_l4_x76_y23), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just15)).
% 0.34/1.41 fof(just16, axiom, mtvisible(c_tptpgeo_member2_mt) => inregion(c_geolocation_x76_y23, c_georegion_l4_x76_y23), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just16)).
% 0.34/1.41 fof(just35, axiom, ! [_44772, _44775, _44778] : (geographicalsubregions(_44772, _44775) & geographicalsubregions(_44775, _44778) => geographicalsubregions(_44772, _44778)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just35)).
% 0.34/1.41 fof(just45, axiom, ! [_44966, _44969, _44972] : (inregion(_44966, _44969) & inregion(_44969, _44972) => inregion(_44966, _44972)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just45)).
% 0.34/1.41 fof(just53, axiom, ! [_45158, _45161] : (mtvisible(_45158) & genlmt(_45158, _45161) => mtvisible(_45161)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just53)).
% 0.34/1.41 fof(just58, axiom, ! [_45322, _45325, _45328] : (genlmt(_45322, _45325) & genlmt(_45325, _45328) => genlmt(_45322, _45328)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just58)).
% 0.34/1.41
% 0.34/1.41 cnf(1, plain, [-(mtvisible(c_tptpgeo_spindlecollectormt))], clausify(query33)).
% 0.34/1.41 cnf(2, plain, [inregion(c_geolocation_x76_y23, c_georegion_l1_x2_y0), geolevel_1(c_georegion_l1_x2_y0)], clausify(query33)).
% 0.34/1.41 cnf(3, plain, [geographicalsubregions(_12290, _12335), -(inregion(_12335, _12290))], clausify(just5)).
% 0.34/1.41 cnf(4, plain, [-(genlmt(c_tptpgeo_spindleheadmt, c_worldgeographymt))], clausify(just8)).
% 0.34/1.41 cnf(5, plain, [-(genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt))], clausify(just9)).
% 0.34/1.41 cnf(6, plain, [-(genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))], clausify(just10)).
% 0.34/1.41 cnf(7, plain, [-(genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member8_mt))], clausify(just11)).
% 0.34/1.41 cnf(8, plain, [mtvisible(c_worldgeographymt), -(geolevel_1(c_georegion_l1_x2_y0))], clausify(just12)).
% 0.34/1.41 cnf(9, plain, [mtvisible(c_tptpgeo_member2_mt), -(geographicalsubregions(c_georegion_l1_x2_y0, c_georegion_l2_x8_y2))], clausify(just13)).
% 0.34/1.41 cnf(10, plain, [mtvisible(c_tptpgeo_member2_mt), -(geographicalsubregions(c_georegion_l2_x8_y2, c_georegion_l3_x25_y7))], clausify(just14)).
% 0.34/1.41 cnf(11, plain, [mtvisible(c_tptpgeo_member2_mt), -(geographicalsubregions(c_georegion_l3_x25_y7, c_georegion_l4_x76_y23))], clausify(just15)).
% 0.34/1.41 cnf(12, plain, [mtvisible(c_tptpgeo_member2_mt), -(inregion(c_geolocation_x76_y23, c_georegion_l4_x76_y23))], clausify(just16)).
% 0.34/1.41 cnf(13, plain, [-(geographicalsubregions(_20177, _20288)), geographicalsubregions(_20177, _20233), geographicalsubregions(_20233, _20288)], clausify(just35)).
% 0.34/1.41 cnf(14, plain, [-(inregion(_23422, _23533)), inregion(_23422, _23478), inregion(_23478, _23533)], clausify(just45)).
% 0.34/1.41 cnf(15, plain, [-(mtvisible(_25897)), mtvisible(_25848), genlmt(_25848, _25897)], clausify(just53)).
% 0.34/1.41 cnf(16, plain, [-(genlmt(_27346, _27457)), genlmt(_27346, _27402), genlmt(_27402, _27457)], clausify(just58)).
% 0.34/1.41
% 0.34/1.41 cnf('1',plain,[inregion(c_geolocation_x76_y23, c_georegion_l1_x2_y0), geolevel_1(c_georegion_l1_x2_y0)],start(2)).
% 0.34/1.41 cnf('1.1',plain,[-(inregion(c_geolocation_x76_y23, c_georegion_l1_x2_y0)), inregion(c_geolocation_x76_y23, c_georegion_l3_x25_y7), inregion(c_georegion_l3_x25_y7, c_georegion_l1_x2_y0)],extension(14,bind([[_23422, _23478, _23533], [c_geolocation_x76_y23, c_georegion_l3_x25_y7, c_georegion_l1_x2_y0]]))).
% 0.34/1.41 cnf('1.1.1',plain,[-(inregion(c_geolocation_x76_y23, c_georegion_l3_x25_y7)), inregion(c_geolocation_x76_y23, c_georegion_l4_x76_y23), inregion(c_georegion_l4_x76_y23, c_georegion_l3_x25_y7)],extension(14,bind([[_23422, _23478, _23533], [c_geolocation_x76_y23, c_georegion_l4_x76_y23, c_georegion_l3_x25_y7]]))).
% 0.34/1.41 cnf('1.1.1.1',plain,[-(inregion(c_geolocation_x76_y23, c_georegion_l4_x76_y23)), mtvisible(c_tptpgeo_member2_mt)],extension(12)).
% 0.34/1.41 cnf('1.1.1.1.1',plain,[-(mtvisible(c_tptpgeo_member2_mt)), mtvisible(c_tptpgeo_spindlecollectormt), genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt)],extension(15,bind([[_25848, _25897], [c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt]]))).
% 0.34/1.41 cnf('1.1.1.1.1.1',plain,[-(mtvisible(c_tptpgeo_spindlecollectormt))],extension(1)).
% 0.34/1.41 cnf('1.1.1.1.1.2',plain,[-(genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt))],extension(5)).
% 0.34/1.41 cnf('1.1.1.2',plain,[-(inregion(c_georegion_l4_x76_y23, c_georegion_l3_x25_y7)), geographicalsubregions(c_georegion_l3_x25_y7, c_georegion_l4_x76_y23)],extension(3,bind([[_12290, _12335], [c_georegion_l3_x25_y7, c_georegion_l4_x76_y23]]))).
% 0.34/1.41 cnf('1.1.1.2.1',plain,[-(geographicalsubregions(c_georegion_l3_x25_y7, c_georegion_l4_x76_y23)), mtvisible(c_tptpgeo_member2_mt)],extension(11)).
% 0.34/1.41 cnf('1.1.1.2.1.1',plain,[-(mtvisible(c_tptpgeo_member2_mt)), mtvisible(c_tptpgeo_spindlecollectormt), genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt)],extension(15,bind([[_25848, _25897], [c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt]]))).
% 0.34/1.41 cnf('1.1.1.2.1.1.1',plain,[-(mtvisible(c_tptpgeo_spindlecollectormt))],extension(1)).
% 0.34/1.41 cnf('1.1.1.2.1.1.2',plain,[-(genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt))],extension(5)).
% 0.34/1.41 cnf('1.1.2',plain,[-(inregion(c_georegion_l3_x25_y7, c_georegion_l1_x2_y0)), geographicalsubregions(c_georegion_l1_x2_y0, c_georegion_l3_x25_y7)],extension(3,bind([[_12290, _12335], [c_georegion_l1_x2_y0, c_georegion_l3_x25_y7]]))).
% 0.34/1.41 cnf('1.1.2.1',plain,[-(geographicalsubregions(c_georegion_l1_x2_y0, c_georegion_l3_x25_y7)), geographicalsubregions(c_georegion_l1_x2_y0, c_georegion_l2_x8_y2), geographicalsubregions(c_georegion_l2_x8_y2, c_georegion_l3_x25_y7)],extension(13,bind([[_20177, _20233, _20288], [c_georegion_l1_x2_y0, c_georegion_l2_x8_y2, c_georegion_l3_x25_y7]]))).
% 0.34/1.41 cnf('1.1.2.1.1',plain,[-(geographicalsubregions(c_georegion_l1_x2_y0, c_georegion_l2_x8_y2)), mtvisible(c_tptpgeo_member2_mt)],extension(9)).
% 0.34/1.41 cnf('1.1.2.1.1.1',plain,[-(mtvisible(c_tptpgeo_member2_mt)), mtvisible(c_tptpgeo_spindlecollectormt), genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt)],extension(15,bind([[_25848, _25897], [c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt]]))).
% 0.34/1.41 cnf('1.1.2.1.1.1.1',plain,[-(mtvisible(c_tptpgeo_spindlecollectormt))],extension(1)).
% 0.34/1.41 cnf('1.1.2.1.1.1.2',plain,[-(genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt))],extension(5)).
% 0.34/1.41 cnf('1.1.2.1.2',plain,[-(geographicalsubregions(c_georegion_l2_x8_y2, c_georegion_l3_x25_y7)), mtvisible(c_tptpgeo_member2_mt)],extension(10)).
% 0.34/1.41 cnf('1.1.2.1.2.1',plain,[-(mtvisible(c_tptpgeo_member2_mt)), mtvisible(c_tptpgeo_spindlecollectormt), genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt)],extension(15,bind([[_25848, _25897], [c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt]]))).
% 0.34/1.41 cnf('1.1.2.1.2.1.1',plain,[-(mtvisible(c_tptpgeo_spindlecollectormt))],extension(1)).
% 0.34/1.41 cnf('1.1.2.1.2.1.2',plain,[-(genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member2_mt))],extension(5)).
% 0.34/1.41 cnf('1.2',plain,[-(geolevel_1(c_georegion_l1_x2_y0)), mtvisible(c_worldgeographymt)],extension(8)).
% 0.34/1.41 cnf('1.2.1',plain,[-(mtvisible(c_worldgeographymt)), mtvisible(c_tptpgeo_spindlecollectormt), genlmt(c_tptpgeo_spindlecollectormt, c_worldgeographymt)],extension(15,bind([[_25848, _25897], [c_tptpgeo_spindlecollectormt, c_worldgeographymt]]))).
% 0.34/1.41 cnf('1.2.1.1',plain,[-(mtvisible(c_tptpgeo_spindlecollectormt))],extension(1)).
% 0.34/1.41 cnf('1.2.1.2',plain,[-(genlmt(c_tptpgeo_spindlecollectormt, c_worldgeographymt)), genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member8_mt), genlmt(c_tptpgeo_member8_mt, c_worldgeographymt)],extension(16,bind([[_27346, _27402, _27457], [c_tptpgeo_spindlecollectormt, c_tptpgeo_member8_mt, c_worldgeographymt]]))).
% 0.34/1.41 cnf('1.2.1.2.1',plain,[-(genlmt(c_tptpgeo_spindlecollectormt, c_tptpgeo_member8_mt))],extension(7)).
% 0.34/1.41 cnf('1.2.1.2.2',plain,[-(genlmt(c_tptpgeo_member8_mt, c_worldgeographymt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), genlmt(c_tptpgeo_spindleheadmt, c_worldgeographymt)],extension(16,bind([[_27346, _27402, _27457], [c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt, c_worldgeographymt]]))).
% 0.34/1.41 cnf('1.2.1.2.2.1',plain,[-(genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))],extension(6)).
% 0.34/1.41 cnf('1.2.1.2.2.2',plain,[-(genlmt(c_tptpgeo_spindleheadmt, c_worldgeographymt))],extension(4)).
% 0.34/1.41 %-----------------------------------------------------
% 0.34/1.42
% 0.34/1.42 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------