%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS075+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n028.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:37 EDT 2022
% Result : Unsatisfiable 0.46s 1.40s
% Output : Proof 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS075+1 : TPTP v8.1.0. Released v3.1.0.
% 0.07/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n028.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 18:10:00 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.46/1.40 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.46/1.41 % SZS output start Proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.46/1.41
% 0.46/1.41 %-----------------------------------------------------
% 0.46/1.41 fof(axiom_2, axiom, ! [_49113] : (cUnsatisfiable(_49113) <=> ? [_49128] : (rf1(_49113, _49128) & ~ cp(_49128)) & ? [_49128] : (rs(_49113, _49128) & cowlThing(_49128)) & ? [_49128] : (rf(_49113, _49128) & cp(_49128))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.46/1.41 fof(cp_substitution_1, axiom, ! [_49503, _49506] : (_49503 = _49506 & cp(_49503) => cp(_49506)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cp_substitution_1)).
% 0.46/1.41 fof(axiom_3, axiom, ! [_49689, _49692, _49695] : (rf(_49689, _49692) & rf(_49689, _49695) => _49692 = _49695), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.46/1.41 fof(axiom_4, axiom, ! [_49870, _49873, _49876] : (rf1(_49870, _49873) & rf1(_49870, _49876) => _49873 = _49876), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.46/1.41 fof(axiom_8, axiom, ! [_50057, _50060, _50063] : (rs(_50057, _50060) & rs(_50057, _50063) => _50060 = _50063), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.46/1.41 fof(axiom_9, axiom, cUnsatisfiable(i2003_11_14_17_19_02584), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_9)).
% 0.46/1.41 fof(axiom_10, axiom, ! [_50285, _50288] : (rs(_50285, _50288) => rf1(_50285, _50288)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_10)).
% 0.46/1.41 fof(axiom_11, axiom, ! [_50431, _50434] : (rs(_50431, _50434) => rf(_50431, _50434)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_11)).
% 0.46/1.41
% 0.46/1.41 cnf(1, plain, [-(4 ^ [_29322]), -(cp(3 ^ [_29322]))], clausify(axiom_2)).
% 0.46/1.41 cnf(2, plain, [-(4 ^ [_29322]), -(rf(_29322, 3 ^ [_29322]))], clausify(axiom_2)).
% 0.46/1.41 cnf(3, plain, [-(4 ^ [_29322]), -(rs(_29322, 2 ^ [_29322]))], clausify(axiom_2)).
% 0.46/1.41 cnf(4, plain, [-(4 ^ [_29322]), cp(1 ^ [_29322])], clausify(axiom_2)).
% 0.46/1.41 cnf(5, plain, [-(4 ^ [_29322]), -(rf1(_29322, 1 ^ [_29322]))], clausify(axiom_2)).
% 0.46/1.41 cnf(6, plain, [-(cp(_22261)), _22212 = _22261, cp(_22212)], clausify(cp_substitution_1)).
% 0.46/1.41 cnf(7, plain, [cUnsatisfiable(_29322), 4 ^ [_29322]], clausify(axiom_2)).
% 0.46/1.41 cnf(8, plain, [-(_30132 = _30187), rf(_30076, _30132), rf(_30076, _30187)], clausify(axiom_3)).
% 0.46/1.41 cnf(9, plain, [-(_30599 = _30654), rf1(_30543, _30599), rf1(_30543, _30654)], clausify(axiom_4)).
% 0.46/1.41 cnf(10, plain, [-(_31996 = _32051), rs(_31940, _31996), rs(_31940, _32051)], clausify(axiom_8)).
% 0.46/1.41 cnf(11, plain, [-(cUnsatisfiable(i2003_11_14_17_19_02584))], clausify(axiom_9)).
% 0.46/1.41 cnf(12, plain, [rs(_32519, _32564), -(rf1(_32519, _32564))], clausify(axiom_10)).
% 0.46/1.41 cnf(13, plain, [rs(_32819, _32864), -(rf(_32819, _32864))], clausify(axiom_11)).
% 0.46/1.41 cnf(14, plain, [-(_14337 = _14337)], theory(equality)).
% 0.46/1.41 cnf(15, plain, [-(_14769 = _14880), _14769 = _14825, _14825 = _14880], theory(equality)).
% 0.46/1.41 cnf(16, plain, [-(rs(_19748, _19879)), rs(_19681, _19814), _19681 = _19748, _19814 = _19879], theory(equality)).
% 0.46/1.41
% 0.46/1.41 cnf('1',plain,[cUnsatisfiable(i2003_11_14_17_19_02584), 4 ^ [i2003_11_14_17_19_02584]],start(7,bind([[_29322], [i2003_11_14_17_19_02584]]))).
% 0.46/1.41 cnf('1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_19_02584))],extension(11)).
% 0.46/1.41 cnf('1.2',plain,[-(4 ^ [i2003_11_14_17_19_02584]), -(rs(i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584]))],extension(3,bind([[_29322], [i2003_11_14_17_19_02584]]))).
% 0.46/1.41 cnf('1.2.1',plain,[rs(i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584]), -(2 ^ [i2003_11_14_17_19_02584] = 1 ^ [i2003_11_14_17_19_02584]), rs(i2003_11_14_17_19_02584, 1 ^ [i2003_11_14_17_19_02584])],extension(10,bind([[_31996, _31940, _32051], [2 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, 1 ^ [i2003_11_14_17_19_02584]]]))).
% 0.46/1.41 cnf('1.2.1.1',plain,[2 ^ [i2003_11_14_17_19_02584] = 1 ^ [i2003_11_14_17_19_02584], -(3 ^ [i2003_11_14_17_19_02584] = 1 ^ [i2003_11_14_17_19_02584]), 3 ^ [i2003_11_14_17_19_02584] = 2 ^ [i2003_11_14_17_19_02584]],extension(15,bind([[_14880, _14769, _14825], [1 ^ [i2003_11_14_17_19_02584], 3 ^ [i2003_11_14_17_19_02584], 2 ^ [i2003_11_14_17_19_02584]]]))).
% 0.46/1.41 cnf('1.2.1.1.1',plain,[3 ^ [i2003_11_14_17_19_02584] = 1 ^ [i2003_11_14_17_19_02584], -(cp(1 ^ [i2003_11_14_17_19_02584])), cp(3 ^ [i2003_11_14_17_19_02584])],extension(6,bind([[_22261, _22212], [1 ^ [i2003_11_14_17_19_02584], 3 ^ [i2003_11_14_17_19_02584]]]))).
% 0.46/1.41 cnf('1.2.1.1.1.1',plain,[cp(1 ^ [i2003_11_14_17_19_02584]), -(4 ^ [i2003_11_14_17_19_02584])],extension(4,bind([[_29322], [i2003_11_14_17_19_02584]]))).
% 0.46/1.41 cnf('1.2.1.1.1.1.1',plain,[4 ^ [i2003_11_14_17_19_02584]],reduction('1')).
% 0.46/1.41 cnf('1.2.1.1.1.2',plain,[-(cp(3 ^ [i2003_11_14_17_19_02584])), -(4 ^ [i2003_11_14_17_19_02584])],extension(1,bind([[_29322], [i2003_11_14_17_19_02584]]))).
% 0.46/1.41 cnf('1.2.1.1.1.2.1',plain,[4 ^ [i2003_11_14_17_19_02584]],reduction('1')).
% 0.46/1.41 cnf('1.2.1.1.2',plain,[-(3 ^ [i2003_11_14_17_19_02584] = 2 ^ [i2003_11_14_17_19_02584]), rf(i2003_11_14_17_19_02584, 3 ^ [i2003_11_14_17_19_02584]), rf(i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584])],extension(8,bind([[_30132, _30076, _30187], [3 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584]]]))).
% 0.46/1.41 cnf('1.2.1.1.2.1',plain,[-(rf(i2003_11_14_17_19_02584, 3 ^ [i2003_11_14_17_19_02584])), -(4 ^ [i2003_11_14_17_19_02584])],extension(2,bind([[_29322], [i2003_11_14_17_19_02584]]))).
% 0.46/1.41 cnf('1.2.1.1.2.1.1',plain,[4 ^ [i2003_11_14_17_19_02584]],reduction('1')).
% 0.46/1.41 cnf('1.2.1.1.2.2',plain,[-(rf(i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584])), rs(i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584])],extension(13,bind([[_32819, _32864], [i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584]]]))).
% 0.46/1.41 cnf('1.2.1.1.2.2.1',plain,[-(rs(i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584]))],reduction('1.2')).
% 0.46/1.41 cnf('1.2.1.2',plain,[-(rs(i2003_11_14_17_19_02584, 1 ^ [i2003_11_14_17_19_02584])), rs(i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584]), i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584] = 1 ^ [i2003_11_14_17_19_02584]],extension(16,bind([[_19681, _19748, _19814, _19879], [i2003_11_14_17_19_02584, i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584], 1 ^ [i2003_11_14_17_19_02584]]]))).
% 0.46/1.41 cnf('1.2.1.2.1',plain,[-(rs(i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584]))],reduction('1.2')).
% 0.46/1.41 cnf('1.2.1.2.2',plain,[-(i2003_11_14_17_19_02584 = i2003_11_14_17_19_02584)],extension(14,bind([[_14337], [i2003_11_14_17_19_02584]]))).
% 0.46/1.41 cnf('1.2.1.2.3',plain,[-(2 ^ [i2003_11_14_17_19_02584] = 1 ^ [i2003_11_14_17_19_02584]), rf1(i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584]), rf1(i2003_11_14_17_19_02584, 1 ^ [i2003_11_14_17_19_02584])],extension(9,bind([[_30599, _30543, _30654], [2 ^ [i2003_11_14_17_19_02584], i2003_11_14_17_19_02584, 1 ^ [i2003_11_14_17_19_02584]]]))).
% 0.46/1.41 cnf('1.2.1.2.3.1',plain,[-(rf1(i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584])), rs(i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584])],extension(12,bind([[_32519, _32564], [i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584]]]))).
% 0.46/1.41 cnf('1.2.1.2.3.1.1',plain,[-(rs(i2003_11_14_17_19_02584, 2 ^ [i2003_11_14_17_19_02584]))],lemmata('1.2.1.2')).
% 0.46/1.41 cnf('1.2.1.2.3.2',plain,[-(rf1(i2003_11_14_17_19_02584, 1 ^ [i2003_11_14_17_19_02584])), -(4 ^ [i2003_11_14_17_19_02584])],extension(5,bind([[_29322], [i2003_11_14_17_19_02584]]))).
% 0.46/1.41 cnf('1.2.1.2.3.2.1',plain,[4 ^ [i2003_11_14_17_19_02584]],reduction('1')).
% 0.46/1.41 %-----------------------------------------------------
% 0.46/1.42
% 0.46/1.42 % SZS output end Proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------