%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS251+1 : TPTP v8.1.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n023.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:04 EDT 2022
% Result : Theorem 29.30s 29.28s
% Output : Proof 29.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : KRS251+1 : TPTP v8.1.0. Bugfixed v5.4.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.32 % Computer : n023.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Tue Jun 7 17:04:38 EDT 2022
% 0.11/0.33 % CPUTime :
% 29.30/29.28 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.30/29.28 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.30/29.29
% 29.30/29.29 %-----------------------------------------------------
% 29.30/29.29 fof(xora, axiom, ! [_62454, _62457] : (! [_62465, _62468] : (status(_62465, _62468, _62454) <~> status(_62465, _62468, _62457)) <=> xora(_62454, _62457)), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax', xora)).
% 29.30/29.29 fof(csa, axiom, ! [_62708, _62711] : (? [_62719] : (model(_62719, _62708) & model(_62719, not _62711)) <=> status(_62708, _62711, csa)), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+0.ax', csa)).
% 29.30/29.29 fof(thm, axiom, ! [_62982, _62985] : (! [_62993] : (model(_62993, _62982) => model(_62993, _62985)) <=> status(_62982, _62985, thm)), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+0.ax', thm)).
% 29.30/29.29 fof(xora_csa_thm, conjecture, xora(csa, thm), file('/export/starexec/sandbox/benchmark/theBenchmark.p', xora_csa_thm)).
% 29.30/29.29 fof(not, axiom, ! [_63288, _63291] : (model(_63288, _63291) <=> ~ model(_63288, not _63291)), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax', not)).
% 29.30/29.29
% 29.30/29.29 cnf(1, plain, [-(82 ^ [_28331, _28266]), -(status(80 ^ [_28331, _28266], 81 ^ [_28331, _28266], _28266)), status(80 ^ [_28331, _28266], 81 ^ [_28331, _28266], _28331)], clausify(xora)).
% 29.30/29.29 cnf(2, plain, [-(82 ^ [_28331, _28266]), status(80 ^ [_28331, _28266], 81 ^ [_28331, _28266], _28266), -(status(80 ^ [_28331, _28266], 81 ^ [_28331, _28266], _28331))], clausify(xora)).
% 29.30/29.29 cnf(3, plain, [-(61 ^ [_23653, _23594]), -(model(60 ^ [_23653, _23594], not _23653))], clausify(csa)).
% 29.30/29.29 cnf(4, plain, [-(61 ^ [_23653, _23594]), -(model(60 ^ [_23653, _23594], _23594))], clausify(csa)).
% 29.30/29.29 cnf(5, plain, [-(17 ^ [_15578, _15521]), model(16 ^ [_15578, _15521], _15578)], clausify(thm)).
% 29.30/29.29 cnf(6, plain, [-(17 ^ [_15578, _15521]), -(model(16 ^ [_15578, _15521], _15521))], clausify(thm)).
% 29.30/29.29 cnf(7, plain, [xora(csa, thm)], clausify(xora_csa_thm)).
% 29.30/29.29 cnf(8, plain, [-(xora(_28266, _28331)), 82 ^ [_28331, _28266]], clausify(xora)).
% 29.30/29.29 cnf(9, plain, [model(_29263, _29312), model(_29263, not _29312)], clausify(not)).
% 29.30/29.29 cnf(10, plain, [-(model(_29263, _29312)), -(model(_29263, not _29312))], clausify(not)).
% 29.30/29.29 cnf(11, plain, [17 ^ [_15578, _15521], -(status(_15521, _15578, thm))], clausify(thm)).
% 29.30/29.29 cnf(12, plain, [status(_15521, _15578, thm), model(_15644, _15521), -(model(_15644, _15578))], clausify(thm)).
% 29.30/29.29 cnf(13, plain, [61 ^ [_23653, _23594], status(_23594, _23653, csa)], clausify(csa)).
% 29.30/29.29 cnf(14, plain, [-(status(_23594, _23653, csa)), model(_23722, _23594), model(_23722, not _23653)], clausify(csa)).
% 29.30/29.29
% 29.30/29.29 cnf('1',plain,[xora(csa, thm)],start(7)).
% 29.30/29.29 cnf('1.1',plain,[-(xora(csa, thm)), 82 ^ [thm, csa]],extension(8,bind([[_28331, _28266], [thm, csa]]))).
% 29.30/29.29 cnf('1.1.1',plain,[-(82 ^ [thm, csa]), -(status(80 ^ [thm, csa], 81 ^ [thm, csa], csa)), status(80 ^ [thm, csa], 81 ^ [thm, csa], thm)],extension(1,bind([[_28266, _28331], [csa, thm]]))).
% 29.30/29.29 cnf('1.1.1.1',plain,[status(80 ^ [thm, csa], 81 ^ [thm, csa], csa), -(82 ^ [thm, csa]), -(status(80 ^ [thm, csa], 81 ^ [thm, csa], thm))],extension(2,bind([[_28266, _28331], [csa, thm]]))).
% 29.30/29.29 cnf('1.1.1.1.1',plain,[82 ^ [thm, csa]],reduction('1.1')).
% 29.30/29.29 cnf('1.1.1.1.2',plain,[status(80 ^ [thm, csa], 81 ^ [thm, csa], thm), model(60 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], 80 ^ [thm, csa]), -(model(60 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], 81 ^ [thm, csa]))],extension(12,bind([[_15521, _15644, _15578], [80 ^ [thm, csa], 60 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], 81 ^ [thm, csa]]]))).
% 29.30/29.29 cnf('1.1.1.1.2.1',plain,[-(model(60 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], 80 ^ [thm, csa])), -(61 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]])],extension(4,bind([[_23653, _23594], [81 ^ [thm, csa], 80 ^ [thm, csa]]]))).
% 29.30/29.29 cnf('1.1.1.1.2.1.1',plain,[61 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], status(80 ^ [thm, csa], 81 ^ [thm, csa], csa)],extension(13,bind([[_23594, _23653], [80 ^ [thm, csa], 81 ^ [thm, csa]]]))).
% 29.30/29.29 cnf('1.1.1.1.2.1.1.1',plain,[-(status(80 ^ [thm, csa], 81 ^ [thm, csa], csa))],reduction('1.1.1')).
% 29.30/29.29 cnf('1.1.1.1.2.2',plain,[model(60 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], 81 ^ [thm, csa]), model(60 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], not 81 ^ [thm, csa])],extension(9,bind([[_29263, _29312], [60 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], 81 ^ [thm, csa]]]))).
% 29.30/29.29 cnf('1.1.1.1.2.2.1',plain,[-(model(60 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], not 81 ^ [thm, csa])), -(61 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]])],extension(3,bind([[_23653, _23594], [81 ^ [thm, csa], 80 ^ [thm, csa]]]))).
% 29.30/29.29 cnf('1.1.1.1.2.2.1.1',plain,[61 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], status(80 ^ [thm, csa], 81 ^ [thm, csa], csa)],extension(13,bind([[_23594, _23653], [80 ^ [thm, csa], 81 ^ [thm, csa]]]))).
% 29.30/29.29 cnf('1.1.1.1.2.2.1.1.1',plain,[-(status(80 ^ [thm, csa], 81 ^ [thm, csa], csa))],reduction('1.1.1')).
% 29.30/29.29 cnf('1.1.1.2',plain,[-(status(80 ^ [thm, csa], 81 ^ [thm, csa], thm)), -(82 ^ [thm, csa]), status(80 ^ [thm, csa], 81 ^ [thm, csa], csa)],extension(2,bind([[_28331, _28266], [thm, csa]]))).
% 29.30/29.29 cnf('1.1.1.2.1',plain,[82 ^ [thm, csa]],reduction('1.1')).
% 29.30/29.29 cnf('1.1.1.2.2',plain,[-(status(80 ^ [thm, csa], 81 ^ [thm, csa], csa)), model(16 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], 80 ^ [thm, csa]), model(16 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], not 81 ^ [thm, csa])],extension(14,bind([[_23594, _23722, _23653], [80 ^ [thm, csa], 16 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], 81 ^ [thm, csa]]]))).
% 29.30/29.29 cnf('1.1.1.2.2.1',plain,[-(model(16 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], 80 ^ [thm, csa])), -(17 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]])],extension(6,bind([[_15578, _15521], [81 ^ [thm, csa], 80 ^ [thm, csa]]]))).
% 29.30/29.29 cnf('1.1.1.2.2.1.1',plain,[17 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], -(status(80 ^ [thm, csa], 81 ^ [thm, csa], thm))],extension(11,bind([[_15521, _15578], [80 ^ [thm, csa], 81 ^ [thm, csa]]]))).
% 29.30/29.29 cnf('1.1.1.2.2.1.1.1',plain,[status(80 ^ [thm, csa], 81 ^ [thm, csa], thm)],reduction('1.1.1')).
% 29.30/29.29 cnf('1.1.1.2.2.2',plain,[-(model(16 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], not 81 ^ [thm, csa])), -(model(16 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], 81 ^ [thm, csa]))],extension(10,bind([[_29263, _29312], [16 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], 81 ^ [thm, csa]]]))).
% 29.30/29.29 cnf('1.1.1.2.2.2.1',plain,[model(16 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], 81 ^ [thm, csa]), -(17 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]])],extension(5,bind([[_15578, _15521], [81 ^ [thm, csa], 80 ^ [thm, csa]]]))).
% 29.30/29.29 cnf('1.1.1.2.2.2.1.1',plain,[17 ^ [81 ^ [thm, csa], 80 ^ [thm, csa]], -(status(80 ^ [thm, csa], 81 ^ [thm, csa], thm))],extension(11,bind([[_15521, _15578], [80 ^ [thm, csa], 81 ^ [thm, csa]]]))).
% 29.30/29.29 cnf('1.1.1.2.2.2.1.1.1',plain,[status(80 ^ [thm, csa], 81 ^ [thm, csa], thm)],reduction('1.1.1')).
% 29.30/29.29 %-----------------------------------------------------
% 29.30/29.29
% 29.30/29.30 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------