%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : CSR048+1 : TPTP v9.2.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n022.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 : Tue May 5 04:14:25 PM UTC 2026
% Result : Theorem 0.27s 1.60s
% Output : CNFRefutation 0.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : CSR048+1 : TPTP v9.2.1. Released v3.4.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.13/0.31 % Computer : n022.cluster.edu
% 0.13/0.31 % Model : x86_64 x86_64
% 0.13/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.31 % Memory : 8042.1875MB
% 0.13/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.31 % CPULimit : 300
% 0.13/0.31 % WCLimit : 300
% 0.13/0.31 % DateTime : Mon May 4 16:34:51 EDT 2026
% 0.13/0.31 % CPUTime :
% 0.13/0.32 % start to proof: theBenchmark
% 0.27/1.60 % Version : CSE_E---1.7
% 0.27/1.60 % Problem : theBenchmark.p
% 0.27/1.60 % SZS status Theorem for theBenchmark.p
% 0.27/1.60 % SZS output start CNFRefutation
% 0.27/1.60 fof(just30, axiom, ![X10]:~(borderson(X10,X10)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just30)).
% 0.27/1.60 fof(query48, conjecture, ?[X9]:(mtvisible(c_tptpgeo_spindlecollectormt)=>borderson(c_georegion_l4_x45_y9,X9)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', query48)).
% 0.27/1.60 fof(just3, axiom, ![X1, X2, X3]:~(((isa(X1,X2)&isa(X1,X3))&disjointwith(X2,X3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just3)).
% 0.27/1.60 fof(just9, axiom, ![X10, X11, X12]:((genlpreds(X10,X11)&genlpreds(X11,X12))=>genlpreds(X10,X12)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just9)).
% 0.27/1.60 fof(just4, axiom, ![X4, X5, X6]:((genlinverse(X4,X5)&genlinverse(X5,X6))=>genlpreds(X4,X6)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just4)).
% 0.27/1.60 fof(just15, axiom, ![X7, X13, X14]:((genlinverse(X7,X13)&genlpreds(X13,X14))=>genlinverse(X7,X14)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just15)).
% 0.27/1.60 fof(just14, axiom, ![X13, X9, X14]:((genlinverse(X13,X9)&genlpreds(X14,X13))=>genlinverse(X14,X9)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just14)).
% 0.27/1.60 fof(just19, axiom, ![X7, X13, X14]:((disjointwith(X7,X13)&genls(X14,X13))=>disjointwith(X7,X14)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just19)).
% 0.27/1.60 fof(just20, axiom, ![X13, X9, X14]:((disjointwith(X13,X9)&genls(X14,X13))=>disjointwith(X14,X9)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just20)).
% 0.27/1.60 fof(just25, axiom, ![X7, X13, X14]:((isa(X7,X13)&genls(X13,X14))=>isa(X7,X14)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just25)).
% 0.27/1.60 fof(just36, axiom, ![X10, X11, X12]:((genlmt(X10,X11)&genlmt(X11,X12))=>genlmt(X10,X12)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just36)).
% 0.27/1.60 fof(just18, axiom, ![X10, X11]:(disjointwith(X10,X11)=>disjointwith(X11,X10)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just18)).
% 0.27/1.60 fof(just29, axiom, ![X10, X11]:(borderson(X10,X11)=>borderson(X11,X10)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just29)).
% 0.27/1.60 fof(just31, axiom, ![X15, X16]:((mtvisible(X15)&genlmt(X15,X16))=>mtvisible(X16)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just31)).
% 0.27/1.60 fof(just35, axiom, ![X8, X9]:(genlmt(X8,X9)=>microtheory(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just35)).
% 0.27/1.60 fof(just34, axiom, ![X8, X9]:(genlmt(X8,X9)=>microtheory(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just34)).
% 0.27/1.60 fof(just33, axiom, ![X7, X8]:(genlmt(X7,X8)=>microtheory(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just33)).
% 0.27/1.60 fof(just32, axiom, ![X7, X8]:(genlmt(X7,X8)=>microtheory(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just32)).
% 0.27/1.60 fof(just28, axiom, ![X8, X9]:(borderson(X8,X9)=>geographicalregion(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just28)).
% 0.27/1.60 fof(just27, axiom, ![X7, X8]:(borderson(X7,X8)=>geographicalregion(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just27)).
% 0.27/1.60 fof(just24, axiom, ![X8, X9]:(isa(X8,X9)=>thing(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just24)).
% 0.27/1.60 fof(just23, axiom, ![X8, X9]:(isa(X8,X9)=>thing(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just23)).
% 0.27/1.60 fof(just17, axiom, ![X8, X9]:(disjointwith(X8,X9)=>collection(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just17)).
% 0.27/1.60 fof(just16, axiom, ![X7, X8]:(disjointwith(X7,X8)=>collection(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just16)).
% 0.27/1.60 fof(just22, axiom, ![X7, X8]:(isa(X7,X8)=>collection(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just22)).
% 0.27/1.60 fof(just21, axiom, ![X7, X8]:(isa(X7,X8)=>collection(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just21)).
% 0.27/1.60 fof(just13, axiom, ![X8, X9]:(genlinverse(X8,X9)=>binarypredicate(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just13)).
% 0.27/1.60 fof(just12, axiom, ![X7, X8]:(genlinverse(X7,X8)=>binarypredicate(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just12)).
% 0.27/1.60 fof(just8, axiom, ![X8, X9]:(genlpreds(X8,X9)=>predicate(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just8)).
% 0.27/1.60 fof(just7, axiom, ![X8, X9]:(genlpreds(X8,X9)=>predicate(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just7)).
% 0.27/1.60 fof(just6, axiom, ![X7, X8]:(genlpreds(X7,X8)=>predicate(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just6)).
% 0.27/1.60 fof(just5, axiom, ![X7, X8]:(genlpreds(X7,X8)=>predicate(X8)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just5)).
% 0.27/1.60 fof(just11, axiom, ![X10]:(predicate(X10)=>genlpreds(X10,X10)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just11)).
% 0.27/1.60 fof(just10, axiom, ![X10]:(predicate(X10)=>genlpreds(X10,X10)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just10)).
% 0.27/1.60 fof(just38, axiom, ![X10]:(microtheory(X10)=>genlmt(X10,X10)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just38)).
% 0.27/1.60 fof(just37, axiom, ![X10]:(microtheory(X10)=>genlmt(X10,X10)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just37)).
% 0.27/1.60 fof(just2, axiom, (mtvisible(c_tptpgeo_member1_mt)=>borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just2)).
% 0.27/1.60 fof(just1, axiom, genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just1)).
% 0.27/1.60 fof(just39, axiom, mtvisible(c_universalvocabularymt), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just39)).
% 0.27/1.60 fof(just26, axiom, mtvisible(c_basekb), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just26)).
% 0.27/1.60 fof(i_0_40, plain, ![X10]:~borderson(X10,X10), inference(fof_simplification,[status(thm)],[just30])).
% 0.27/1.60 fof(i_0_41, negated_conjecture, ~(?[X9]:(mtvisible(c_tptpgeo_spindlecollectormt)=>borderson(c_georegion_l4_x45_y9,X9))), inference(assume_negation,[status(cth)],[query48])).
% 0.27/1.60 fof(i_0_42, plain, ![X92, X93, X94]:(~isa(X92,X93)|~isa(X92,X94)|~disjointwith(X93,X94)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just3])])).
% 0.27/1.60 fof(i_0_43, plain, ![X106, X107, X108]:(~genlpreds(X106,X107)|~genlpreds(X107,X108)|genlpreds(X106,X108)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just9])])).
% 0.27/1.60 fof(i_0_44, plain, ![X95, X96, X97]:(~genlinverse(X95,X96)|~genlinverse(X96,X97)|genlpreds(X95,X97)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just4])])).
% 0.27/1.60 fof(i_0_45, plain, ![X118, X119, X120]:(~genlinverse(X118,X119)|~genlpreds(X119,X120)|genlinverse(X118,X120)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just15])])).
% 0.27/1.60 fof(i_0_46, plain, ![X115, X116, X117]:(~genlinverse(X115,X116)|~genlpreds(X117,X115)|genlinverse(X117,X116)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just14])])).
% 0.27/1.60 fof(i_0_47, plain, ![X127, X128, X129]:(~disjointwith(X127,X128)|~genls(X129,X128)|disjointwith(X127,X129)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just19])])).
% 0.27/1.60 fof(i_0_48, plain, ![X130, X131, X132]:(~disjointwith(X130,X131)|~genls(X132,X130)|disjointwith(X132,X131)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just20])])).
% 0.27/1.60 fof(i_0_49, plain, ![X141, X142, X143]:(~isa(X141,X142)|~genls(X142,X143)|isa(X141,X143)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just25])])).
% 0.27/1.60 fof(i_0_50, plain, ![X161, X162, X163]:(~genlmt(X161,X162)|~genlmt(X162,X163)|genlmt(X161,X163)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just36])])).
% 0.27/1.60 fof(i_0_51, plain, ![X125, X126]:(~disjointwith(X125,X126)|disjointwith(X126,X125)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just18])])).
% 0.27/1.60 fof(i_0_52, plain, ![X148, X149]:(~borderson(X148,X149)|borderson(X149,X148)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just29])])).
% 0.27/1.60 fof(i_0_53, plain, ![X151, X152]:(~mtvisible(X151)|~genlmt(X151,X152)|mtvisible(X152)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just31])])).
% 0.27/1.60 fof(i_0_54, plain, ![X159, X160]:(~genlmt(X159,X160)|microtheory(X159)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just35])])).
% 0.27/1.60 fof(i_0_55, plain, ![X157, X158]:(~genlmt(X157,X158)|microtheory(X157)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just34])])).
% 0.27/1.60 fof(i_0_56, plain, ![X155, X156]:(~genlmt(X155,X156)|microtheory(X156)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just33])])).
% 0.27/1.60 fof(i_0_57, plain, ![X153, X154]:(~genlmt(X153,X154)|microtheory(X154)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just32])])).
% 0.27/1.60 fof(i_0_58, plain, ![X146, X147]:(~borderson(X146,X147)|geographicalregion(X146)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just28])])).
% 0.27/1.60 fof(i_0_59, plain, ![X144, X145]:(~borderson(X144,X145)|geographicalregion(X145)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just27])])).
% 0.27/1.60 fof(i_0_60, plain, ![X139, X140]:(~isa(X139,X140)|thing(X139)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just24])])).
% 0.27/1.60 fof(i_0_61, plain, ![X137, X138]:(~isa(X137,X138)|thing(X137)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just23])])).
% 0.27/1.60 fof(i_0_62, plain, ![X123, X124]:(~disjointwith(X123,X124)|collection(X123)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just17])])).
% 0.27/1.60 fof(i_0_63, plain, ![X121, X122]:(~disjointwith(X121,X122)|collection(X122)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just16])])).
% 0.27/1.60 fof(i_0_64, plain, ![X135, X136]:(~isa(X135,X136)|collection(X136)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just22])])).
% 0.27/1.60 fof(i_0_65, plain, ![X133, X134]:(~isa(X133,X134)|collection(X134)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just21])])).
% 0.27/1.60 fof(i_0_66, plain, ![X113, X114]:(~genlinverse(X113,X114)|binarypredicate(X113)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just13])])).
% 0.27/1.60 fof(i_0_67, plain, ![X111, X112]:(~genlinverse(X111,X112)|binarypredicate(X112)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just12])])).
% 0.27/1.60 fof(i_0_68, plain, ![X104, X105]:(~genlpreds(X104,X105)|predicate(X104)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just8])])).
% 0.27/1.60 fof(i_0_69, plain, ![X102, X103]:(~genlpreds(X102,X103)|predicate(X102)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just7])])).
% 0.27/1.60 fof(i_0_70, plain, ![X100, X101]:(~genlpreds(X100,X101)|predicate(X101)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just6])])).
% 0.27/1.60 fof(i_0_71, plain, ![X98, X99]:(~genlpreds(X98,X99)|predicate(X99)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just5])])).
% 0.27/1.60 fof(i_0_72, plain, ![X150]:~borderson(X150,X150), inference(variable_rename,[status(thm)],[i_0_40])).
% 0.27/1.60 fof(i_0_73, plain, ![X110]:(~predicate(X110)|genlpreds(X110,X110)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just11])])).
% 0.27/1.60 fof(i_0_74, plain, ![X109]:(~predicate(X109)|genlpreds(X109,X109)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just10])])).
% 0.27/1.60 fof(i_0_75, plain, ![X165]:(~microtheory(X165)|genlmt(X165,X165)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just38])])).
% 0.27/1.60 fof(i_0_76, plain, ![X164]:(~microtheory(X164)|genlmt(X164,X164)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just37])])).
% 0.27/1.60 fof(i_0_77, negated_conjecture, ![X166]:(mtvisible(c_tptpgeo_spindlecollectormt)&~borderson(c_georegion_l4_x45_y9,X166)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_41])])).
% 0.27/1.60 fof(i_0_78, plain, (~mtvisible(c_tptpgeo_member1_mt)|borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10)), inference(fof_nnf,[status(thm)],[just2])).
% 0.27/1.60 cnf(i_0_79, plain, (~isa(X1,X2)|~isa(X1,X3)|~disjointwith(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_42]), ['final']).
% 0.27/1.60 cnf(i_0_80, plain, (genlpreds(X1,X3)|~genlpreds(X1,X2)|~genlpreds(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_43]), ['final']).
% 0.27/1.60 cnf(i_0_81, plain, (genlpreds(X1,X3)|~genlinverse(X1,X2)|~genlinverse(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_44]), ['final']).
% 0.27/1.60 cnf(i_0_82, plain, (genlinverse(X1,X3)|~genlinverse(X1,X2)|~genlpreds(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_45]), ['final']).
% 0.27/1.60 cnf(i_0_83, plain, (genlinverse(X3,X2)|~genlinverse(X1,X2)|~genlpreds(X3,X1)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.27/1.60 cnf(i_0_84, plain, (disjointwith(X1,X3)|~disjointwith(X1,X2)|~genls(X3,X2)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.27/1.60 cnf(i_0_85, plain, (disjointwith(X3,X2)|~disjointwith(X1,X2)|~genls(X3,X1)), inference(split_conjunct,[status(thm)],[i_0_48]), ['final']).
% 0.27/1.60 cnf(i_0_86, plain, (isa(X1,X3)|~isa(X1,X2)|~genls(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_49]), ['final']).
% 0.27/1.60 cnf(i_0_87, plain, (genlmt(X1,X3)|~genlmt(X1,X2)|~genlmt(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_50]), ['final']).
% 0.27/1.60 cnf(i_0_88, plain, (disjointwith(X2,X1)|~disjointwith(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_51]), ['final']).
% 0.27/1.60 cnf(i_0_89, plain, (borderson(X2,X1)|~borderson(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_52]), ['final']).
% 0.27/1.60 cnf(i_0_90, plain, (mtvisible(X2)|~mtvisible(X1)|~genlmt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.27/1.60 cnf(i_0_91, plain, (microtheory(X1)|~genlmt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.27/1.60 cnf(i_0_92, plain, (microtheory(X1)|~genlmt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.27/1.60 cnf(i_0_93, plain, (microtheory(X2)|~genlmt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_56]), ['final']).
% 0.27/1.60 cnf(i_0_94, plain, (microtheory(X2)|~genlmt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.27/1.60 cnf(i_0_95, plain, (geographicalregion(X1)|~borderson(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.27/1.60 cnf(i_0_96, plain, (geographicalregion(X2)|~borderson(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.27/1.60 cnf(i_0_97, plain, (thing(X1)|~isa(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_60]), ['final']).
% 0.27/1.60 cnf(i_0_98, plain, (thing(X1)|~isa(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_61]), ['final']).
% 0.27/1.60 cnf(i_0_99, plain, (collection(X1)|~disjointwith(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_62]), ['final']).
% 0.27/1.60 cnf(i_0_100, plain, (collection(X2)|~disjointwith(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.27/1.60 cnf(i_0_101, plain, (collection(X2)|~isa(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.27/1.60 cnf(i_0_102, plain, (collection(X2)|~isa(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_65]), ['final']).
% 0.27/1.60 cnf(i_0_103, plain, (binarypredicate(X1)|~genlinverse(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_66]), ['final']).
% 0.27/1.60 cnf(i_0_104, plain, (binarypredicate(X2)|~genlinverse(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.27/1.60 cnf(i_0_105, plain, (predicate(X1)|~genlpreds(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_68]), ['final']).
% 0.27/1.60 cnf(i_0_106, plain, (predicate(X1)|~genlpreds(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_69]), ['final']).
% 0.27/1.60 cnf(i_0_107, plain, (predicate(X2)|~genlpreds(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_70]), ['final']).
% 0.27/1.60 cnf(i_0_108, plain, (predicate(X2)|~genlpreds(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_71]), ['final']).
% 0.27/1.60 cnf(i_0_109, plain, (~borderson(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_72]), ['final']).
% 0.27/1.60 cnf(i_0_110, plain, (genlpreds(X1,X1)|~predicate(X1)), inference(split_conjunct,[status(thm)],[i_0_73]), ['final']).
% 0.27/1.60 cnf(i_0_111, plain, (genlpreds(X1,X1)|~predicate(X1)), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.27/1.60 cnf(i_0_112, plain, (genlmt(X1,X1)|~microtheory(X1)), inference(split_conjunct,[status(thm)],[i_0_75]), ['final']).
% 0.27/1.60 cnf(i_0_113, plain, (genlmt(X1,X1)|~microtheory(X1)), inference(split_conjunct,[status(thm)],[i_0_76]), ['final']).
% 0.27/1.60 cnf(i_0_114, negated_conjecture, (~borderson(c_georegion_l4_x45_y9,X1)), inference(split_conjunct,[status(thm)],[i_0_77]), ['final']).
% 0.27/1.60 cnf(i_0_115, plain, (borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10)|~mtvisible(c_tptpgeo_member1_mt)), inference(split_conjunct,[status(thm)],[i_0_78]), ['final']).
% 0.27/1.60 cnf(i_0_116, plain, (genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), inference(split_conjunct,[status(thm)],[just1]), ['final']).
% 0.27/1.60 cnf(i_0_117, plain, (mtvisible(c_universalvocabularymt)), inference(split_conjunct,[status(thm)],[just39]), ['final']).
% 0.27/1.60 cnf(i_0_118, plain, (mtvisible(c_basekb)), inference(split_conjunct,[status(thm)],[just26]), ['final']).
% 0.27/1.60 cnf(i_0_119, negated_conjecture, (mtvisible(c_tptpgeo_spindlecollectormt)), inference(split_conjunct,[status(thm)],[i_0_77]), ['final']).
% 0.27/1.62 cnf(i_0_120, plain, (~mtvisible(c_tptpgeo_member1_mt)), inference(scs_inference,[],[i_0_114,i_0_115])).
% 0.27/1.62 cnf(i_0_121, plain, (mtvisible(c_tptpgeo_member1_mt)), inference(scs_inference,[],[i_0_119,i_0_116,i_0_90])).
% 0.27/1.62 cnf(i_0_122, plain, (~genlmt(X1,X2)|mtvisible(X2)|~mtvisible(X1)), inference(rename_variables,[],[i_0_90])).
% 0.27/1.62 cnf(i_0_123, plain, (genlmt(X1,c_tptpgeo_member1_mt)|~genlmt(X1,c_tptpgeo_spindlecollectormt)), inference(scs_inference,[],[i_0_119,i_0_116,i_0_90,i_0_87])).
% 0.27/1.62 cnf(i_0_124, plain, (~genlmt(X1,X2)|genlmt(X3,X2)|~genlmt(X3,X1)), inference(rename_variables,[],[i_0_87])).
% 0.27/1.62 cnf(i_0_125,plain, ($false), inference(scs_inference,[],[i_0+120, i_0_121]), ['proof']).
% 0.27/1.62 % SZS output end CNFRefutation
% 0.27/1.62 % Total time : 1.271s
%------------------------------------------------------------------------------