%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS088+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n025.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:13:39 EDT 2022
% Result : Unsatisfiable 0.36s 1.40s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : KRS088+1 : TPTP v8.1.0. Released v3.1.0.
% 0.12/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n025.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 19:46:04 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.36/1.40 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.41 % SZS output start Proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.41
% 0.36/1.41 %-----------------------------------------------------
% 0.36/1.41 fof(axiom_2, axiom, ! [_37622] : (cUnsatisfiable(_37622) <=> ? [_37637] : (rf(_37622, _37637) & ! [_37655] : (rinvF(_37637, _37655) => ? [_37673] : (rf(_37655, _37673) & ~ cp1(_37673))) & cp1(_37637))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.36/1.41 fof(cp1_substitution_1, axiom, ! [_37992, _37995] : (_37992 = _37995 & cp1(_37992) => cp1(_37995)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cp1_substitution_1)).
% 0.36/1.41 fof(axiom_3, axiom, ! [_38174, _38177, _38180] : (rf(_38174, _38177) & rf(_38174, _38180) => _38177 = _38180), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.36/1.41 fof(axiom_4, axiom, ! [_38356, _38359] : (rinvF(_38356, _38359) <=> rf(_38359, _38356)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.36/1.41 fof(axiom_7, axiom, cUnsatisfiable(i2003_11_14_17_19_49673), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 0.36/1.41
% 0.36/1.41 cnf(1, plain, [-(3 ^ [_28118, _22962]), cp1(2 ^ [_28118, _22962])], clausify(axiom_2)).
% 0.36/1.41 cnf(2, plain, [-(3 ^ [_28118, _22962]), -(rf(_28118, 2 ^ [_28118, _22962]))], clausify(axiom_2)).
% 0.36/1.41 cnf(3, plain, [-(4 ^ [_22962]), rinvF(1 ^ [_22962], _28118), 3 ^ [_28118, _22962]], clausify(axiom_2)).
% 0.36/1.41 cnf(4, plain, [-(4 ^ [_22962]), -(cp1(1 ^ [_22962]))], clausify(axiom_2)).
% 0.36/1.41 cnf(5, plain, [-(4 ^ [_22962]), -(rf(_22962, 1 ^ [_22962]))], clausify(axiom_2)).
% 0.36/1.41 cnf(6, plain, [-(cp1(_17769)), _17720 = _17769, cp1(_17720)], clausify(cp1_substitution_1)).
% 0.36/1.41 cnf(7, plain, [cUnsatisfiable(_22962), 4 ^ [_22962]], clausify(axiom_2)).
% 0.36/1.41 cnf(8, plain, [-(_23767 = _23822), rf(_23711, _23767), rf(_23711, _23822)], clausify(axiom_3)).
% 0.36/1.41 cnf(9, plain, [-(rinvF(_24178, _24223)), rf(_24223, _24178)], clausify(axiom_4)).
% 0.36/1.41 cnf(10, plain, [-(cUnsatisfiable(i2003_11_14_17_19_49673))], clausify(axiom_7)).
% 0.36/1.41
% 0.36/1.41 cnf('1',plain,[cUnsatisfiable(i2003_11_14_17_19_49673), 4 ^ [i2003_11_14_17_19_49673]],start(7,bind([[_22962], [i2003_11_14_17_19_49673]]))).
% 0.36/1.41 cnf('1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_19_49673))],extension(10)).
% 0.36/1.41 cnf('1.2',plain,[-(4 ^ [i2003_11_14_17_19_49673]), rinvF(1 ^ [i2003_11_14_17_19_49673], i2003_11_14_17_19_49673), 3 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673]],extension(3,bind([[_28118, _22962], [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673]]))).
% 0.36/1.41 cnf('1.2.1',plain,[-(rinvF(1 ^ [i2003_11_14_17_19_49673], i2003_11_14_17_19_49673)), rf(i2003_11_14_17_19_49673, 1 ^ [i2003_11_14_17_19_49673])],extension(9,bind([[_24223, _24178], [i2003_11_14_17_19_49673, 1 ^ [i2003_11_14_17_19_49673]]]))).
% 0.36/1.41 cnf('1.2.1.1',plain,[-(rf(i2003_11_14_17_19_49673, 1 ^ [i2003_11_14_17_19_49673])), -(4 ^ [i2003_11_14_17_19_49673])],extension(5,bind([[_22962], [i2003_11_14_17_19_49673]]))).
% 0.36/1.41 cnf('1.2.1.1.1',plain,[4 ^ [i2003_11_14_17_19_49673]],reduction('1')).
% 0.36/1.41 cnf('1.2.2',plain,[-(3 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673]), -(rf(i2003_11_14_17_19_49673, 2 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673]))],extension(2,bind([[_28118, _22962], [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673]]))).
% 0.36/1.41 cnf('1.2.2.1',plain,[rf(i2003_11_14_17_19_49673, 2 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673]), -(1 ^ [i2003_11_14_17_19_49673] = 2 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673]), rf(i2003_11_14_17_19_49673, 1 ^ [i2003_11_14_17_19_49673])],extension(8,bind([[_23822, _23711, _23767], [2 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673], i2003_11_14_17_19_49673, 1 ^ [i2003_11_14_17_19_49673]]]))).
% 0.36/1.41 cnf('1.2.2.1.1',plain,[1 ^ [i2003_11_14_17_19_49673] = 2 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673], -(cp1(2 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673])), cp1(1 ^ [i2003_11_14_17_19_49673])],extension(6,bind([[_17769, _17720], [2 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673], 1 ^ [i2003_11_14_17_19_49673]]]))).
% 0.36/1.41 cnf('1.2.2.1.1.1',plain,[cp1(2 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673]), -(3 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673])],extension(1,bind([[_28118, _22962], [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673]]))).
% 0.36/1.41 cnf('1.2.2.1.1.1.1',plain,[3 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673]],reduction('1.2')).
% 0.36/1.41 cnf('1.2.2.1.1.2',plain,[-(cp1(1 ^ [i2003_11_14_17_19_49673])), -(4 ^ [i2003_11_14_17_19_49673])],extension(4,bind([[_22962], [i2003_11_14_17_19_49673]]))).
% 0.36/1.41 cnf('1.2.2.1.1.2.1',plain,[4 ^ [i2003_11_14_17_19_49673]],reduction('1')).
% 0.36/1.41 cnf('1.2.2.1.2',plain,[-(rf(i2003_11_14_17_19_49673, 1 ^ [i2003_11_14_17_19_49673])), -(4 ^ [i2003_11_14_17_19_49673])],extension(5,bind([[_22962], [i2003_11_14_17_19_49673]]))).
% 0.36/1.41 cnf('1.2.2.1.2.1',plain,[4 ^ [i2003_11_14_17_19_49673]],reduction('1')).
% 0.36/1.41 %-----------------------------------------------------
% 0.36/1.42
% 0.36/1.42 % SZS output end Proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------