%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR045+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 20:53:14 EDT 2022
% Result : Theorem 0.37s 1.40s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CSR045+1 : TPTP v8.1.0. Released v3.4.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n021.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 : Fri Jun 10 18:40:24 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.37/1.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/1.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/1.41
% 0.37/1.41 %-----------------------------------------------------
% 0.37/1.41 fof(query45, conjecture, ~ genls(c_wamt_evalinitial_p14, c_tptpcol_15_80088), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', query45)).
% 0.37/1.41 fof(just1, axiom, applicationcontext(c_wamt_evalinitial_p14), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just1)).
% 0.37/1.41 fof(just3, axiom, ! [_53767] : (microtheory(_53767) => aspatialinformationstore(_53767)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just3)).
% 0.37/1.41 fof(just6, axiom, ! [_53890] : (intangibleindividual(_53890) => partiallyintangibleindividual(_53890)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just6)).
% 0.37/1.41 fof(just8, axiom, ! [_54012] : (aspatialinformationstore(_54012) => intangibleindividual(_54012)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just8)).
% 0.37/1.41 fof(just10, axiom, ! [_54134] : (partiallyintangibleindividual(_54134) => individual(_54134)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just10)).
% 0.37/1.41 fof(just14, axiom, ! [_54258] : (applicationcontext(_54258) => microtheory(_54258)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just14)).
% 0.37/1.41 fof(just15, axiom, ! [_54379] : ~ (collection(_54379) & individual(_54379)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just15)).
% 0.37/1.41 fof(just20, axiom, ! [_54511, _54514] : (genls(_54511, _54514) => collection(_54511)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just20)).
% 0.37/1.41
% 0.37/1.41 cnf(1, plain, [-(genls(c_wamt_evalinitial_p14, c_tptpcol_15_80088))], clausify(query45)).
% 0.37/1.41 cnf(2, plain, [-(applicationcontext(c_wamt_evalinitial_p14))], clausify(just1)).
% 0.37/1.41 cnf(3, plain, [microtheory(_16004), -(aspatialinformationstore(_16004))], clausify(just3)).
% 0.37/1.41 cnf(4, plain, [intangibleindividual(_16480), -(partiallyintangibleindividual(_16480))], clausify(just6)).
% 0.37/1.41 cnf(5, plain, [aspatialinformationstore(_16823), -(intangibleindividual(_16823))], clausify(just8)).
% 0.37/1.41 cnf(6, plain, [partiallyintangibleindividual(_17166), -(individual(_17166))], clausify(just10)).
% 0.37/1.41 cnf(7, plain, [applicationcontext(_17754), -(microtheory(_17754))], clausify(just14)).
% 0.37/1.41 cnf(8, plain, [collection(_17964), individual(_17964)], clausify(just15)).
% 0.37/1.41 cnf(9, plain, [genls(_19414, _19458), -(collection(_19414))], clausify(just20)).
% 0.37/1.41
% 0.37/1.41 cnf('1',plain,[collection(c_wamt_evalinitial_p14), individual(c_wamt_evalinitial_p14)],start(8,bind([[_17964], [c_wamt_evalinitial_p14]]))).
% 0.37/1.41 cnf('1.1',plain,[-(collection(c_wamt_evalinitial_p14)), genls(c_wamt_evalinitial_p14, c_tptpcol_15_80088)],extension(9,bind([[_19414, _19458], [c_wamt_evalinitial_p14, c_tptpcol_15_80088]]))).
% 0.37/1.41 cnf('1.1.1',plain,[-(genls(c_wamt_evalinitial_p14, c_tptpcol_15_80088))],extension(1)).
% 0.37/1.41 cnf('1.2',plain,[-(individual(c_wamt_evalinitial_p14)), partiallyintangibleindividual(c_wamt_evalinitial_p14)],extension(6,bind([[_17166], [c_wamt_evalinitial_p14]]))).
% 0.37/1.41 cnf('1.2.1',plain,[-(partiallyintangibleindividual(c_wamt_evalinitial_p14)), intangibleindividual(c_wamt_evalinitial_p14)],extension(4,bind([[_16480], [c_wamt_evalinitial_p14]]))).
% 0.37/1.41 cnf('1.2.1.1',plain,[-(intangibleindividual(c_wamt_evalinitial_p14)), aspatialinformationstore(c_wamt_evalinitial_p14)],extension(5,bind([[_16823], [c_wamt_evalinitial_p14]]))).
% 0.37/1.41 cnf('1.2.1.1.1',plain,[-(aspatialinformationstore(c_wamt_evalinitial_p14)), microtheory(c_wamt_evalinitial_p14)],extension(3,bind([[_16004], [c_wamt_evalinitial_p14]]))).
% 0.37/1.41 cnf('1.2.1.1.1.1',plain,[-(microtheory(c_wamt_evalinitial_p14)), applicationcontext(c_wamt_evalinitial_p14)],extension(7,bind([[_17754], [c_wamt_evalinitial_p14]]))).
% 0.37/1.41 cnf('1.2.1.1.1.1.1',plain,[-(applicationcontext(c_wamt_evalinitial_p14))],extension(2)).
% 0.37/1.41 %-----------------------------------------------------
% 0.37/1.42
% 0.37/1.42 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------