%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR045+2 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %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 : 600s
% DateTime : Fri Jul 15 20:53:14 EDT 2022
% Result : Theorem 6.47s 6.57s
% Output : Proof 6.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : CSR045+2 : TPTP v8.1.0. Released v3.4.0.
% 0.06/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n022.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:00:49 EDT 2022
% 0.12/0.33 % CPUTime :
% 6.47/6.57 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.47/6.57 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.47/6.58
% 6.47/6.58 %-----------------------------------------------------
% 6.47/6.58 fof(query95, conjecture, ~ genls(c_wamt_evalinitial_p14, c_tptpcol_15_80088), file('/export/starexec/sandbox/benchmark/theBenchmark.p', query95)).
% 6.47/6.58 fof(ax1_32, axiom, genls(c_partiallyintangibleindividual, c_individual), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_32)).
% 6.47/6.58 fof(ax1_83, axiom, applicationcontext(c_wamt_evalinitial_p14), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_83)).
% 6.47/6.58 fof(ax1_155, axiom, genls(c_microtheory, c_aspatialinformationstore), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_155)).
% 6.47/6.58 fof(ax1_170, axiom, genls(c_applicationcontext, c_microtheory), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_170)).
% 6.47/6.58 fof(ax1_229, axiom, ! [_452792, _452795] : (genls(_452792, _452795) => collection(_452792)), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_229)).
% 6.47/6.58 fof(ax1_290, axiom, disjointwith(c_collection, c_individual), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_290)).
% 6.47/6.58 fof(ax1_319, axiom, genls(c_intangibleindividual, c_partiallyintangibleindividual), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_319)).
% 6.47/6.58 fof(ax1_363, axiom, ! [_453162, _453165, _453168] : ~ (isa(_453162, _453165) & isa(_453162, _453168) & disjointwith(_453165, _453168)), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_363)).
% 6.47/6.58 fof(ax1_381, axiom, genls(c_aspatialinformationstore, c_intangibleindividual), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_381)).
% 6.47/6.58 fof(ax1_814, axiom, ! [_453853] : (collection(_453853) => isa(_453853, c_collection)), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_814)).
% 6.47/6.58 fof(ax1_930, axiom, ! [_454096] : (applicationcontext(_454096) => isa(_454096, c_applicationcontext)), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_930)).
% 6.47/6.58 fof(ax1_1094, axiom, ! [_454387, _454390, _454393] : (isa(_454387, _454390) & genls(_454390, _454393) => isa(_454387, _454393)), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_1094)).
% 6.47/6.58 fof(ax1_1109, axiom, ! [_454586, _454589, _454592] : (genls(_454586, _454589) & genls(_454589, _454592) => genls(_454586, _454592)), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_1109)).
% 6.47/6.58 fof(ax1_1121, axiom, ! [_454782, _454785, _454788] : (disjointwith(_454782, _454785) & genls(_454788, _454785) => disjointwith(_454782, _454788)), file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax', ax1_1121)).
% 6.47/6.58
% 6.47/6.58 cnf(1, plain, [-(genls(c_wamt_evalinitial_p14, c_tptpcol_15_80088))], clausify(query95)).
% 6.47/6.58 cnf(2, plain, [-(genls(c_partiallyintangibleindividual, c_individual))], clausify(ax1_32)).
% 6.47/6.58 cnf(3, plain, [-(applicationcontext(c_wamt_evalinitial_p14))], clausify(ax1_83)).
% 6.47/6.58 cnf(4, plain, [-(genls(c_microtheory, c_aspatialinformationstore))], clausify(ax1_155)).
% 6.47/6.58 cnf(5, plain, [-(genls(c_applicationcontext, c_microtheory))], clausify(ax1_170)).
% 6.47/6.58 cnf(6, plain, [genls(_66265, _66309), -(collection(_66265))], clausify(ax1_229)).
% 6.47/6.58 cnf(7, plain, [-(disjointwith(c_collection, c_individual))], clausify(ax1_290)).
% 6.47/6.58 cnf(8, plain, [-(genls(c_intangibleindividual, c_partiallyintangibleindividual))], clausify(ax1_319)).
% 6.47/6.58 cnf(9, plain, [isa(_90511, _90569), isa(_90511, _90626), disjointwith(_90569, _90626)], clausify(ax1_363)).
% 6.47/6.58 cnf(10, plain, [-(genls(c_aspatialinformationstore, c_intangibleindividual))], clausify(ax1_381)).
% 6.47/6.58 cnf(11, plain, [collection(_198111), -(isa(_198111, c_collection))], clausify(ax1_814)).
% 6.47/6.58 cnf(12, plain, [applicationcontext(_227968), -(isa(_227968, c_applicationcontext))], clausify(ax1_930)).
% 6.47/6.58 cnf(13, plain, [-(isa(_272312, _272423)), isa(_272312, _272368), genls(_272368, _272423)], clausify(ax1_1094)).
% 6.47/6.58 cnf(14, plain, [-(genls(_276247, _276358)), genls(_276247, _276303), genls(_276303, _276358)], clausify(ax1_1109)).
% 6.47/6.58 cnf(15, plain, [-(disjointwith(_279924, _280035)), disjointwith(_279924, _279980), genls(_280035, _279980)], clausify(ax1_1121)).
% 6.47/6.58
% 6.47/6.58 cnf('1',plain,[isa(c_wamt_evalinitial_p14, c_collection), isa(c_wamt_evalinitial_p14, c_aspatialinformationstore), disjointwith(c_collection, c_aspatialinformationstore)],start(9,bind([[_90511, _90569, _90626], [c_wamt_evalinitial_p14, c_collection, c_aspatialinformationstore]]))).
% 6.47/6.58 cnf('1.1',plain,[-(isa(c_wamt_evalinitial_p14, c_collection)), collection(c_wamt_evalinitial_p14)],extension(11,bind([[_198111], [c_wamt_evalinitial_p14]]))).
% 6.47/6.58 cnf('1.1.1',plain,[-(collection(c_wamt_evalinitial_p14)), genls(c_wamt_evalinitial_p14, c_tptpcol_15_80088)],extension(6,bind([[_66265, _66309], [c_wamt_evalinitial_p14, c_tptpcol_15_80088]]))).
% 6.47/6.58 cnf('1.1.1.1',plain,[-(genls(c_wamt_evalinitial_p14, c_tptpcol_15_80088))],extension(1)).
% 6.47/6.58 cnf('1.2',plain,[-(isa(c_wamt_evalinitial_p14, c_aspatialinformationstore)), isa(c_wamt_evalinitial_p14, c_applicationcontext), genls(c_applicationcontext, c_aspatialinformationstore)],extension(13,bind([[_272312, _272368, _272423], [c_wamt_evalinitial_p14, c_applicationcontext, c_aspatialinformationstore]]))).
% 6.47/6.58 cnf('1.2.1',plain,[-(isa(c_wamt_evalinitial_p14, c_applicationcontext)), applicationcontext(c_wamt_evalinitial_p14)],extension(12,bind([[_227968], [c_wamt_evalinitial_p14]]))).
% 6.47/6.58 cnf('1.2.1.1',plain,[-(applicationcontext(c_wamt_evalinitial_p14))],extension(3)).
% 6.47/6.58 cnf('1.2.2',plain,[-(genls(c_applicationcontext, c_aspatialinformationstore)), genls(c_applicationcontext, c_microtheory), genls(c_microtheory, c_aspatialinformationstore)],extension(14,bind([[_276247, _276303, _276358], [c_applicationcontext, c_microtheory, c_aspatialinformationstore]]))).
% 6.47/6.58 cnf('1.2.2.1',plain,[-(genls(c_applicationcontext, c_microtheory))],extension(5)).
% 6.47/6.58 cnf('1.2.2.2',plain,[-(genls(c_microtheory, c_aspatialinformationstore))],extension(4)).
% 6.47/6.58 cnf('1.3',plain,[-(disjointwith(c_collection, c_aspatialinformationstore)), disjointwith(c_collection, c_partiallyintangibleindividual), genls(c_aspatialinformationstore, c_partiallyintangibleindividual)],extension(15,bind([[_279924, _280035, _279980], [c_collection, c_aspatialinformationstore, c_partiallyintangibleindividual]]))).
% 6.47/6.58 cnf('1.3.1',plain,[-(disjointwith(c_collection, c_partiallyintangibleindividual)), disjointwith(c_collection, c_individual), genls(c_partiallyintangibleindividual, c_individual)],extension(15,bind([[_279924, _280035, _279980], [c_collection, c_partiallyintangibleindividual, c_individual]]))).
% 6.47/6.58 cnf('1.3.1.1',plain,[-(disjointwith(c_collection, c_individual))],extension(7)).
% 6.47/6.58 cnf('1.3.1.2',plain,[-(genls(c_partiallyintangibleindividual, c_individual))],extension(2)).
% 6.47/6.58 cnf('1.3.2',plain,[-(genls(c_aspatialinformationstore, c_partiallyintangibleindividual)), genls(c_aspatialinformationstore, c_intangibleindividual), genls(c_intangibleindividual, c_partiallyintangibleindividual)],extension(14,bind([[_276247, _276303, _276358], [c_aspatialinformationstore, c_intangibleindividual, c_partiallyintangibleindividual]]))).
% 6.47/6.58 cnf('1.3.2.1',plain,[-(genls(c_aspatialinformationstore, c_intangibleindividual))],extension(10)).
% 6.47/6.58 cnf('1.3.2.2',plain,[-(genls(c_intangibleindividual, c_partiallyintangibleindividual))],extension(8)).
% 6.47/6.58 %-----------------------------------------------------
% 6.47/6.58
% 6.47/6.59 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------