%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CSR057+2 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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 : Thu May 9 17:18:27 EDT 2024
% Result : Theorem 92.24s 92.43s
% Output : Refutation 92.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR057+2 : TPTP v8.1.2. Released v3.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n028.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 : 300
% 0.13/0.33 % DateTime : Thu May 9 02:01:37 EDT 2024
% 0.13/0.34 % CPUTime :
% 92.24/92.43 % Version: 1.5
% 92.24/92.43 % SZS status Theorem
% 92.24/92.43 % SZS output start CNFRefutation
% 92.24/92.43 fof(query107,conjecture,(?[X]:(mtvisible(c_tptpgeo_member8_mt)=>inregion(X,c_georegion_l4_x75_y75))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', query107)).
% 92.24/92.43 fof(c0,negated_conjecture,(~(?[X]:(mtvisible(c_tptpgeo_member8_mt)=>inregion(X,c_georegion_l4_x75_y75)))),inference(assume_negation,[status(cth)],[query107])).
% 92.24/92.43 fof(c1,negated_conjecture,(![X]:(mtvisible(c_tptpgeo_member8_mt)&~inregion(X,c_georegion_l4_x75_y75))),inference(fof_nnf,[status(thm)],[c0])).
% 92.24/92.43 fof(c2,negated_conjecture,(mtvisible(c_tptpgeo_member8_mt)&(![X]:~inregion(X,c_georegion_l4_x75_y75))),inference(shift_quantors,[status(thm)],[c1])).
% 92.24/92.43 fof(c4,negated_conjecture,(![X2]:(mtvisible(c_tptpgeo_member8_mt)&~inregion(X2,c_georegion_l4_x75_y75))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,(mtvisible(c_tptpgeo_member8_mt)&(![X2]:~inregion(X2,c_georegion_l4_x75_y75))),inference(variable_rename,[status(thm)],[c2])).])).
% 92.24/92.43 cnf(c6,negated_conjecture,~inregion(X1125,c_georegion_l4_x75_y75),inference(split_conjunct,[status(thm)],[c4])).
% 92.24/92.43 fof(ax1_934,axiom,(![X]:(spatialthing_nonsituational(X)=>inregion(X,X))),file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_934)).
% 92.24/92.43 fof(c619,plain,(![X]:(~spatialthing_nonsituational(X)|inregion(X,X))),inference(fof_nnf,[status(thm)],[ax1_934])).
% 92.24/92.43 fof(c620,plain,(![X302]:(~spatialthing_nonsituational(X302)|inregion(X302,X302))),inference(variable_rename,[status(thm)],[c619])).
% 92.24/92.43 cnf(c621,plain,~spatialthing_nonsituational(X1562)|inregion(X1562,X1562),inference(split_conjunct,[status(thm)],[c620])).
% 92.24/92.43 fof(ax1_288,axiom,(![OBJ]:(enduringthing_localized(OBJ)=>spatialthing_nonsituational(OBJ))),file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_288)).
% 92.24/92.43 fof(c2331,plain,(![OBJ]:(~enduringthing_localized(OBJ)|spatialthing_nonsituational(OBJ))),inference(fof_nnf,[status(thm)],[ax1_288])).
% 92.24/92.43 fof(c2332,plain,(![X1001]:(~enduringthing_localized(X1001)|spatialthing_nonsituational(X1001))),inference(variable_rename,[status(thm)],[c2331])).
% 92.24/92.43 cnf(c2333,plain,~enduringthing_localized(X1347)|spatialthing_nonsituational(X1347),inference(split_conjunct,[status(thm)],[c2332])).
% 92.24/92.43 fof(ax1_39,axiom,(![OBJ]:(partiallytangible(OBJ)=>enduringthing_localized(OBJ))),file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_39)).
% 92.24/92.43 fof(c2784,plain,(![OBJ]:(~partiallytangible(OBJ)|enduringthing_localized(OBJ))),inference(fof_nnf,[status(thm)],[ax1_39])).
% 92.24/92.43 fof(c2785,plain,(![X1105]:(~partiallytangible(X1105)|enduringthing_localized(X1105))),inference(variable_rename,[status(thm)],[c2784])).
% 92.24/92.43 cnf(c2786,plain,~partiallytangible(X1608)|enduringthing_localized(X1608),inference(split_conjunct,[status(thm)],[c2785])).
% 92.24/92.43 fof(ax1_219,axiom,(![OBJ]:(geographicalregion(OBJ)=>partiallytangible(OBJ))),file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_219)).
% 92.24/92.43 fof(c2457,plain,(![OBJ]:(~geographicalregion(OBJ)|partiallytangible(OBJ))),inference(fof_nnf,[status(thm)],[ax1_219])).
% 92.24/92.43 fof(c2458,plain,(![X1030]:(~geographicalregion(X1030)|partiallytangible(X1030))),inference(variable_rename,[status(thm)],[c2457])).
% 92.24/92.43 cnf(c2459,plain,~geographicalregion(X1395)|partiallytangible(X1395),inference(split_conjunct,[status(thm)],[c2458])).
% 92.24/92.43 fof(ax1_462,axiom,(![OBJ]:(geolevel_4(OBJ)=>geographicalregion(OBJ))),file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_462)).
% 92.24/92.43 fof(c2014,plain,(![OBJ]:(~geolevel_4(OBJ)|geographicalregion(OBJ))),inference(fof_nnf,[status(thm)],[ax1_462])).
% 92.24/92.43 fof(c2015,plain,(![X923]:(~geolevel_4(X923)|geographicalregion(X923))),inference(variable_rename,[status(thm)],[c2014])).
% 92.24/92.43 cnf(c2016,plain,~geolevel_4(X1182)|geographicalregion(X1182),inference(split_conjunct,[status(thm)],[c2015])).
% 92.24/92.43 fof(ax1_464,axiom,(mtvisible(c_worldgeographymt)=>geolevel_4(c_georegion_l4_x75_y75)),file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_464)).
% 92.24/92.43 fof(c2010,plain,(~mtvisible(c_worldgeographymt)|geolevel_4(c_georegion_l4_x75_y75)),inference(fof_nnf,[status(thm)],[ax1_464])).
% 92.24/92.43 cnf(c2011,plain,~mtvisible(c_worldgeographymt)|geolevel_4(c_georegion_l4_x75_y75),inference(split_conjunct,[status(thm)],[c2010])).
% 92.24/92.43 fof(ax1_1123,axiom,(![SPECMT]:(![GENLMT]:((mtvisible(SPECMT)&genlmt(SPECMT,GENLMT))=>mtvisible(GENLMT)))),file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_1123)).
% 92.24/92.43 fof(c33,plain,(![SPECMT]:(![GENLMT]:((~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT))|mtvisible(GENLMT)))),inference(fof_nnf,[status(thm)],[ax1_1123])).
% 92.24/92.43 fof(c34,plain,(![X16]:(![X17]:((~mtvisible(X16)|~genlmt(X16,X17))|mtvisible(X17)))),inference(variable_rename,[status(thm)],[c33])).
% 92.24/92.43 cnf(c35,plain,~mtvisible(X1159)|~genlmt(X1159,X1160)|mtvisible(X1160),inference(split_conjunct,[status(thm)],[c34])).
% 92.24/92.43 fof(ax1_326,axiom,genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt),file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_326)).
% 92.24/92.43 cnf(c2261,plain,genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt),inference(split_conjunct,[status(thm)],[ax1_326])).
% 92.24/92.43 cnf(c3487,plain,~mtvisible(c_tptpgeo_spindleheadmt)|mtvisible(c_worldgeographymt),inference(resolution,[status(thm)],[c2261, c35])).
% 92.24/92.43 cnf(c5,negated_conjecture,mtvisible(c_tptpgeo_member8_mt),inference(split_conjunct,[status(thm)],[c4])).
% 92.24/92.43 fof(ax1_1,axiom,genlmt(c_tptpgeo_member8_mt,c_tptpgeo_spindleheadmt),file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_1)).
% 92.24/92.43 cnf(c2856,plain,genlmt(c_tptpgeo_member8_mt,c_tptpgeo_spindleheadmt),inference(split_conjunct,[status(thm)],[ax1_1])).
% 92.24/92.43 cnf(c5376,plain,~mtvisible(c_tptpgeo_member8_mt)|mtvisible(c_tptpgeo_spindleheadmt),inference(resolution,[status(thm)],[c2856, c35])).
% 92.24/92.43 cnf(c16861,plain,mtvisible(c_tptpgeo_spindleheadmt),inference(resolution,[status(thm)],[c5376, c5])).
% 92.24/92.43 cnf(c16862,plain,mtvisible(c_worldgeographymt),inference(resolution,[status(thm)],[c16861, c3487])).
% 92.24/92.43 cnf(c16865,plain,geolevel_4(c_georegion_l4_x75_y75),inference(resolution,[status(thm)],[c16862, c2011])).
% 92.24/92.43 cnf(c16873,plain,geographicalregion(c_georegion_l4_x75_y75),inference(resolution,[status(thm)],[c16865, c2016])).
% 92.24/92.43 cnf(c16878,plain,partiallytangible(c_georegion_l4_x75_y75),inference(resolution,[status(thm)],[c16873, c2459])).
% 92.24/92.43 cnf(c16882,plain,enduringthing_localized(c_georegion_l4_x75_y75),inference(resolution,[status(thm)],[c16878, c2786])).
% 92.24/92.43 cnf(c16885,plain,spatialthing_nonsituational(c_georegion_l4_x75_y75),inference(resolution,[status(thm)],[c16882, c2333])).
% 92.24/92.43 cnf(c16887,plain,inregion(c_georegion_l4_x75_y75,c_georegion_l4_x75_y75),inference(resolution,[status(thm)],[c16885, c621])).
% 92.24/92.43 cnf(c22553,plain,$false,inference(resolution,[status(thm)],[c16887, c6])).
% 92.24/92.43 % SZS output end CNFRefutation
% 92.24/92.43
% 92.24/92.43 % Initial clauses : 1133
% 92.24/92.43 % Processed clauses : 6877
% 92.24/92.43 % Factors computed : 8
% 92.24/92.43 % Resolvents computed: 19692
% 92.24/92.43 % Tautologies deleted: 780
% 92.24/92.43 % Forward subsumed : 7977
% 92.24/92.43 % Backward subsumed : 11
% 92.24/92.43 % -------- CPU Time ---------
% 92.24/92.43 % User time : 92.018 s
% 92.24/92.43 % System time : 0.056 s
% 92.24/92.43 % Total time : 92.074 s
%------------------------------------------------------------------------------