%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS097+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n018.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:41 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.07/0.12 % Problem : KRS097+1 : TPTP v8.1.0. Released v3.1.0.
% 0.07/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n018.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 20:47:51 EDT 2022
% 0.12/0.33 % 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, ! [_58836] : (cUnsatisfiable(_58836) <=> ? [_58851] : rr(_58836, _58851) & ? [_58869] : (rr(_58836, _58869) & cd(_58869)) & ~ ? [_58851, _58898] : (rr(_58836, _58851) & rr(_58836, _58898) & (! _58851) = _58898) & ? [_58869] : (rr(_58836, _58869) & cc(_58869))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.36/1.41 fof(cc_substitution_1, axiom, ! [_59332, _59335] : (_59332 = _59335 & cc(_59332) => cc(_59335)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc_substitution_1)).
% 0.36/1.41 fof(axiom_4, axiom, cUnsatisfiable(i2003_11_14_17_20_21603), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.36/1.41 fof(axiom_6, axiom, ! [_59576] : ~ (cd(_59576) & cc(_59576)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.36/1.41
% 0.36/1.41 cnf(1, plain, [-(4 ^ [_38325]), rr(_38325, _38758), rr(_38325, _38816), -(_38758 = _38816)], clausify(axiom_2)).
% 0.36/1.41 cnf(2, plain, [-(4 ^ [_38325]), -(cc(3 ^ [_38325]))], clausify(axiom_2)).
% 0.36/1.41 cnf(3, plain, [-(4 ^ [_38325]), -(rr(_38325, 3 ^ [_38325]))], clausify(axiom_2)).
% 0.36/1.41 cnf(4, plain, [-(4 ^ [_38325]), -(cd(2 ^ [_38325]))], clausify(axiom_2)).
% 0.36/1.41 cnf(5, plain, [-(4 ^ [_38325]), -(rr(_38325, 2 ^ [_38325]))], clausify(axiom_2)).
% 0.36/1.41 cnf(6, plain, [-(cc(_27996)), _27947 = _27996, cc(_27947)], clausify(cc_substitution_1)).
% 0.36/1.41 cnf(7, plain, [cUnsatisfiable(_38325), 4 ^ [_38325]], clausify(axiom_2)).
% 0.36/1.41 cnf(8, plain, [-(cUnsatisfiable(i2003_11_14_17_20_21603))], clausify(axiom_4)).
% 0.36/1.41 cnf(9, plain, [cd(_40019), cc(_40019)], clausify(axiom_6)).
% 0.36/1.41
% 0.36/1.41 cnf('1',plain,[cd(2 ^ [i2003_11_14_17_20_21603]), cc(2 ^ [i2003_11_14_17_20_21603])],start(9,bind([[_40019], [2 ^ [i2003_11_14_17_20_21603]]]))).
% 0.36/1.41 cnf('1.1',plain,[-(cd(2 ^ [i2003_11_14_17_20_21603])), -(4 ^ [i2003_11_14_17_20_21603])],extension(4,bind([[_38325], [i2003_11_14_17_20_21603]]))).
% 0.36/1.41 cnf('1.1.1',plain,[4 ^ [i2003_11_14_17_20_21603], cUnsatisfiable(i2003_11_14_17_20_21603)],extension(7,bind([[_38325], [i2003_11_14_17_20_21603]]))).
% 0.36/1.41 cnf('1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_20_21603))],extension(8)).
% 0.36/1.41 cnf('1.2',plain,[-(cc(2 ^ [i2003_11_14_17_20_21603])), 3 ^ [i2003_11_14_17_20_21603] = 2 ^ [i2003_11_14_17_20_21603], cc(3 ^ [i2003_11_14_17_20_21603])],extension(6,bind([[_27996, _27947], [2 ^ [i2003_11_14_17_20_21603], 3 ^ [i2003_11_14_17_20_21603]]]))).
% 0.36/1.41 cnf('1.2.1',plain,[-(3 ^ [i2003_11_14_17_20_21603] = 2 ^ [i2003_11_14_17_20_21603]), -(4 ^ [i2003_11_14_17_20_21603]), rr(i2003_11_14_17_20_21603, 3 ^ [i2003_11_14_17_20_21603]), rr(i2003_11_14_17_20_21603, 2 ^ [i2003_11_14_17_20_21603])],extension(1,bind([[_38758, _38325, _38816], [3 ^ [i2003_11_14_17_20_21603], i2003_11_14_17_20_21603, 2 ^ [i2003_11_14_17_20_21603]]]))).
% 0.36/1.41 cnf('1.2.1.1',plain,[4 ^ [i2003_11_14_17_20_21603], cUnsatisfiable(i2003_11_14_17_20_21603)],extension(7,bind([[_38325], [i2003_11_14_17_20_21603]]))).
% 0.36/1.41 cnf('1.2.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_20_21603))],extension(8)).
% 0.36/1.41 cnf('1.2.1.2',plain,[-(rr(i2003_11_14_17_20_21603, 3 ^ [i2003_11_14_17_20_21603])), -(4 ^ [i2003_11_14_17_20_21603])],extension(3,bind([[_38325], [i2003_11_14_17_20_21603]]))).
% 0.36/1.41 cnf('1.2.1.2.1',plain,[4 ^ [i2003_11_14_17_20_21603]],lemmata('1.2.1')).
% 0.36/1.41 cnf('1.2.1.3',plain,[-(rr(i2003_11_14_17_20_21603, 2 ^ [i2003_11_14_17_20_21603])), -(4 ^ [i2003_11_14_17_20_21603])],extension(5,bind([[_38325], [i2003_11_14_17_20_21603]]))).
% 0.36/1.41 cnf('1.2.1.3.1',plain,[4 ^ [i2003_11_14_17_20_21603]],lemmata('1.2.1')).
% 0.36/1.41 cnf('1.2.2',plain,[-(cc(3 ^ [i2003_11_14_17_20_21603])), -(4 ^ [i2003_11_14_17_20_21603])],extension(2,bind([[_38325], [i2003_11_14_17_20_21603]]))).
% 0.36/1.41 cnf('1.2.2.1',plain,[4 ^ [i2003_11_14_17_20_21603], cUnsatisfiable(i2003_11_14_17_20_21603)],extension(7,bind([[_38325], [i2003_11_14_17_20_21603]]))).
% 0.36/1.41 cnf('1.2.2.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_20_21603))],extension(8)).
% 0.36/1.41 %-----------------------------------------------------
% 0.36/1.42
% 0.36/1.42 % SZS output end Proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------