%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS233+1 : TPTP v8.1.0. Bugfixed v5.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 : Sun Jul 17 03:14:02 EDT 2022
% Result : Theorem 29.58s 29.40s
% Output : Proof 29.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : KRS233+1 : TPTP v8.1.0. Bugfixed v5.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 : Tue Jun 7 14:56:20 EDT 2022
% 0.12/0.33 % CPUTime :
% 29.58/29.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.66/29.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.66/29.41
% 29.66/29.41 %-----------------------------------------------------
% 29.66/29.41 fof(nevera, axiom, ! [_57873, _57876] : (! [_57884, _57887] : (status(_57884, _57887, _57873) => ~ status(_57884, _57887, _57876)) <=> nevera(_57873, _57876)), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax', nevera)).
% 29.66/29.41 fof(csa, axiom, ! [_58132, _58135] : (? [_58143] : (model(_58143, _58132) & model(_58143, not _58135)) <=> status(_58132, _58135, csa)), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+0.ax', csa)).
% 29.66/29.41 fof(nevera_csa_thm, conjecture, nevera(csa, thm), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', nevera_csa_thm)).
% 29.66/29.41 fof(not, axiom, ! [_58491, _58494] : (model(_58491, _58494) <=> ~ model(_58491, not _58494)), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax', not)).
% 29.66/29.41 fof(thm, axiom, ! [_58678, _58681] : (! [_58689] : (model(_58689, _58678) => model(_58689, _58681)) <=> status(_58678, _58681, thm)), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+0.ax', thm)).
% 29.66/29.41
% 29.66/29.41 cnf(1, plain, [-(79 ^ [_27720, _27655]), -(status(77 ^ [_27720, _27655], 78 ^ [_27720, _27655], _27720))], clausify(nevera)).
% 29.66/29.41 cnf(2, plain, [-(79 ^ [_27720, _27655]), -(status(77 ^ [_27720, _27655], 78 ^ [_27720, _27655], _27655))], clausify(nevera)).
% 29.66/29.41 cnf(3, plain, [-(61 ^ [_23689, _23630]), -(model(60 ^ [_23689, _23630], not _23689))], clausify(csa)).
% 29.66/29.41 cnf(4, plain, [-(61 ^ [_23689, _23630]), -(model(60 ^ [_23689, _23630], _23630))], clausify(csa)).
% 29.66/29.41 cnf(5, plain, [nevera(csa, thm)], clausify(nevera_csa_thm)).
% 29.66/29.41 cnf(6, plain, [79 ^ [_27720, _27655], -(nevera(_27655, _27720))], clausify(nevera)).
% 29.66/29.41 cnf(7, plain, [model(_29299, _29348), model(_29299, not _29348)], clausify(not)).
% 29.66/29.41 cnf(8, plain, [status(_15557, _15614, thm), model(_15680, _15557), -(model(_15680, _15614))], clausify(thm)).
% 29.66/29.41 cnf(9, plain, [61 ^ [_23689, _23630], status(_23630, _23689, csa)], clausify(csa)).
% 29.66/29.41
% 29.66/29.41 cnf('1',plain,[nevera(csa, thm)],start(5)).
% 29.66/29.41 cnf('1.1',plain,[-(nevera(csa, thm)), 79 ^ [thm, csa]],extension(6,bind([[_27720, _27655], [thm, csa]]))).
% 29.66/29.41 cnf('1.1.1',plain,[-(79 ^ [thm, csa]), -(status(77 ^ [thm, csa], 78 ^ [thm, csa], thm))],extension(1,bind([[_27655, _27720], [csa, thm]]))).
% 29.66/29.41 cnf('1.1.1.1',plain,[status(77 ^ [thm, csa], 78 ^ [thm, csa], thm), model(60 ^ [78 ^ [thm, csa], 77 ^ [thm, csa]], 77 ^ [thm, csa]), -(model(60 ^ [78 ^ [thm, csa], 77 ^ [thm, csa]], 78 ^ [thm, csa]))],extension(8,bind([[_15557, _15680, _15614], [77 ^ [thm, csa], 60 ^ [78 ^ [thm, csa], 77 ^ [thm, csa]], 78 ^ [thm, csa]]]))).
% 29.66/29.41 cnf('1.1.1.1.1',plain,[-(model(60 ^ [78 ^ [thm, csa], 77 ^ [thm, csa]], 77 ^ [thm, csa])), -(61 ^ [78 ^ [thm, csa], 77 ^ [thm, csa]])],extension(4,bind([[_23689, _23630], [78 ^ [thm, csa], 77 ^ [thm, csa]]]))).
% 29.66/29.41 cnf('1.1.1.1.1.1',plain,[61 ^ [78 ^ [thm, csa], 77 ^ [thm, csa]], status(77 ^ [thm, csa], 78 ^ [thm, csa], csa)],extension(9,bind([[_23630, _23689], [77 ^ [thm, csa], 78 ^ [thm, csa]]]))).
% 29.66/29.41 cnf('1.1.1.1.1.1.1',plain,[-(status(77 ^ [thm, csa], 78 ^ [thm, csa], csa)), -(79 ^ [thm, csa])],extension(2,bind([[_27720, _27655], [thm, csa]]))).
% 29.66/29.41 cnf('1.1.1.1.1.1.1.1',plain,[79 ^ [thm, csa]],reduction('1.1')).
% 29.66/29.41 cnf('1.1.1.1.2',plain,[model(60 ^ [78 ^ [thm, csa], 77 ^ [thm, csa]], 78 ^ [thm, csa]), model(60 ^ [78 ^ [thm, csa], 77 ^ [thm, csa]], not 78 ^ [thm, csa])],extension(7,bind([[_29299, _29348], [60 ^ [78 ^ [thm, csa], 77 ^ [thm, csa]], 78 ^ [thm, csa]]]))).
% 29.66/29.41 cnf('1.1.1.1.2.1',plain,[-(model(60 ^ [78 ^ [thm, csa], 77 ^ [thm, csa]], not 78 ^ [thm, csa])), -(61 ^ [78 ^ [thm, csa], 77 ^ [thm, csa]])],extension(3,bind([[_23689, _23630], [78 ^ [thm, csa], 77 ^ [thm, csa]]]))).
% 29.66/29.41 cnf('1.1.1.1.2.1.1',plain,[61 ^ [78 ^ [thm, csa], 77 ^ [thm, csa]], status(77 ^ [thm, csa], 78 ^ [thm, csa], csa)],extension(9,bind([[_23630, _23689], [77 ^ [thm, csa], 78 ^ [thm, csa]]]))).
% 29.66/29.41 cnf('1.1.1.1.2.1.1.1',plain,[-(status(77 ^ [thm, csa], 78 ^ [thm, csa], csa)), -(79 ^ [thm, csa])],extension(2,bind([[_27720, _27655], [thm, csa]]))).
% 29.66/29.41 cnf('1.1.1.1.2.1.1.1.1',plain,[79 ^ [thm, csa]],reduction('1.1')).
% 29.66/29.41 %-----------------------------------------------------
% 29.66/29.42
% 29.66/29.42 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------