%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWV487+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n029.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 : Wed Jul 20 19:51:14 EDT 2022
% Result : Theorem 36.19s 35.63s
% Output : Proof 36.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV487+3 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n029.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 : Thu Jun 16 01:43:27 EDT 2022
% 0.12/0.33 % CPUTime :
% 36.19/35.63 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 36.19/35.63 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 36.19/35.64
% 36.19/35.64 %-----------------------------------------------------
% 36.19/35.64 fof(qii, hypothesis, ! [_41815, _41818] : (int_leq(int_one, _41815) & int_leq(_41815, n) & int_leq(int_one, _41818) & int_leq(_41818, n) => ! [_41866] : (int_less(int_zero, _41866) & _41815 = plus(_41818, _41866) => ! [_41897] : (int_leq(int_one, _41897) & int_leq(_41897, _41818) => a(plus(_41897, _41866), _41897) = real_zero)) & ! [_41897] : (int_leq(int_one, _41897) & int_leq(_41897, _41818) => a(_41897, _41897) = real_one) & ! [_41866] : (int_less(int_zero, _41866) & _41818 = plus(_41815, _41866) => ! [_41897] : (int_leq(int_one, _41897) & int_leq(_41897, _41815) => a(_41897, plus(_41897, _41866)) = real_zero))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', qii)).
% 36.19/35.64 fof(plus_and_inverse, axiom, ! [_42620, _42623] : (int_less(_42620, _42623) <=> ? [_42641] : (plus(_42620, _42641) = _42623 & int_less(int_zero, _42641))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', plus_and_inverse)).
% 36.19/35.64 fof(int_leq, axiom, ! [_42848, _42851] : (int_leq(_42848, _42851) <=> int_less(_42848, _42851) | _42848 = _42851), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', int_leq)).
% 36.19/35.64 fof(ut, conjecture, ! [_43030, _43033] : (int_leq(int_one, _43033) & int_less(_43033, _43030) & int_leq(_43030, n) => a(_43030, _43033) = real_zero), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ut)).
% 36.19/35.64 fof(int_less_transitive, axiom, ! [_43366, _43369, _43372] : (int_less(_43366, _43369) & int_less(_43369, _43372) => int_less(_43366, _43372)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', int_less_transitive)).
% 36.19/35.64 fof(int_less_irreflexive, axiom, ! [_43551, _43554] : (int_less(_43551, _43554) => (! _43551) = _43554), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', int_less_irreflexive)).
% 36.19/35.64 fof(int_less_total, axiom, ! [_43700, _43703] : (int_less(_43700, _43703) | int_leq(_43703, _43700)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', int_less_total)).
% 36.19/35.64 fof(one_successor_of_zero, axiom, ! [_43874] : (int_less(int_zero, _43874) <=> int_leq(int_one, _43874)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', one_successor_of_zero)).
% 36.19/35.64
% 36.19/35.64 cnf(1, plain, [-(4 ^ [_15841, _15660]), _15660 = plus(_15841, _16312), int_less(int_zero, _16312), -(a(plus(_16562, _16312), _16562) = real_zero), int_leq(int_one, _16562), int_leq(_16562, _15841)], clausify(qii)).
% 36.19/35.64 cnf(2, plain, [-(3 ^ [_14818, _14759]), -(int_less(int_zero, 2 ^ [_14818, _14759]))], clausify(plus_and_inverse)).
% 36.19/35.64 cnf(3, plain, [-(3 ^ [_14818, _14759]), -(plus(_14759, 2 ^ [_14818, _14759]) = _14818)], clausify(plus_and_inverse)).
% 36.19/35.64 cnf(4, plain, [-(1 ^ [_12005, _11954]), _11954 = _12005], clausify(int_leq)).
% 36.19/35.64 cnf(5, plain, [-(1 ^ [_12005, _11954]), int_less(_11954, _12005)], clausify(int_leq)).
% 36.19/35.64 cnf(6, plain, [-(int_leq(int_one, 6 ^ []))], clausify(ut)).
% 36.19/35.64 cnf(7, plain, [-(int_less(6 ^ [], 5 ^ []))], clausify(ut)).
% 36.19/35.64 cnf(8, plain, [-(int_leq(5 ^ [], n))], clausify(ut)).
% 36.19/35.64 cnf(9, plain, [a(5 ^ [], 6 ^ []) = real_zero], clausify(ut)).
% 36.19/35.64 cnf(10, plain, [-(a(_10665, _10798) = a(_10732, _10863)), _10665 = _10732, _10798 = _10863], theory(equality)).
% 36.19/35.64 cnf(11, plain, [-(_8489 = _8489)], theory(equality)).
% 36.19/35.64 cnf(12, plain, [_8642 = _8687, -(_8687 = _8642)], theory(equality)).
% 36.19/35.64 cnf(13, plain, [-(_8921 = _9032), _8921 = _8977, _8977 = _9032], theory(equality)).
% 36.19/35.64 cnf(14, plain, [-(int_leq(_9464, _9595)), int_leq(_9397, _9530), _9397 = _9464, _9530 = _9595], theory(equality)).
% 36.19/35.64 cnf(15, plain, [-(int_leq(_11954, _12005)), 1 ^ [_12005, _11954]], clausify(int_leq)).
% 36.19/35.64 cnf(16, plain, [int_leq(_11954, _12005), -(int_less(_11954, _12005)), -(_11954 = _12005)], clausify(int_leq)).
% 36.19/35.64 cnf(17, plain, [-(int_less(_12350, _12461)), int_less(_12350, _12406), int_less(_12406, _12461)], clausify(int_less_transitive)).
% 36.19/35.64 cnf(18, plain, [int_less(_12817, _12864), _12817 = _12864], clausify(int_less_irreflexive)).
% 36.19/35.64 cnf(19, plain, [-(int_less(_13147, _13192)), -(int_leq(_13192, _13147))], clausify(int_less_total)).
% 36.19/35.64 cnf(20, plain, [int_less(_14759, _14818), 3 ^ [_14818, _14759]], clausify(plus_and_inverse)).
% 36.19/35.64 cnf(21, plain, [-(int_less(_14759, _14818)), plus(_14759, _14936) = _14818, int_less(int_zero, _14936)], clausify(plus_and_inverse)).
% 36.19/35.64 cnf(22, plain, [int_less(int_zero, _15267), -(int_leq(int_one, _15267))], clausify(one_successor_of_zero)).
% 36.19/35.64 cnf(23, plain, [-(int_less(int_zero, _15267)), int_leq(int_one, _15267)], clausify(one_successor_of_zero)).
% 36.19/35.64 cnf(24, plain, [int_leq(_15841, n), int_leq(int_one, _15841), int_leq(_15660, n), int_leq(int_one, _15660), 4 ^ [_15841, _15660]], clausify(qii)).
% 36.19/35.64
% 36.19/35.64 cnf('1',plain,[-(int_leq(int_one, 6 ^ []))],start(6)).
% 36.19/35.64 cnf('1.1',plain,[int_leq(int_one, 6 ^ []), int_leq(6 ^ [], n), int_leq(5 ^ [], n), int_leq(int_one, 5 ^ []), 4 ^ [6 ^ [], 5 ^ []]],extension(24,bind([[_15841, _15660], [6 ^ [], 5 ^ []]]))).
% 36.19/35.64 cnf('1.1.1',plain,[-(int_leq(6 ^ [], n)), 1 ^ [n, 6 ^ []]],extension(15,bind([[_12005, _11954], [n, 6 ^ []]]))).
% 36.19/35.64 cnf('1.1.1.1',plain,[-(1 ^ [n, 6 ^ []]), int_less(6 ^ [], n)],extension(5,bind([[_11954, _12005], [6 ^ [], n]]))).
% 36.19/35.64 cnf('1.1.1.1.1',plain,[-(int_less(6 ^ [], n)), plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]) = n, int_less(int_zero, 2 ^ [5 ^ [], 6 ^ []])],extension(21,bind([[_14759, _14818, _14936], [6 ^ [], n, 2 ^ [5 ^ [], 6 ^ []]]]))).
% 36.19/35.64 cnf('1.1.1.1.1.1',plain,[-(plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]) = n), plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]) = 5 ^ [], 5 ^ [] = n],extension(13,bind([[_8921, _8977, _9032], [plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]), 5 ^ [], n]]))).
% 36.19/35.64 cnf('1.1.1.1.1.1.1',plain,[-(plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]) = 5 ^ []), -(3 ^ [5 ^ [], 6 ^ []])],extension(3,bind([[_14818, _14759], [5 ^ [], 6 ^ []]]))).
% 36.19/35.64 cnf('1.1.1.1.1.1.1.1',plain,[3 ^ [5 ^ [], 6 ^ []], int_less(6 ^ [], 5 ^ [])],extension(20,bind([[_14759, _14818], [6 ^ [], 5 ^ []]]))).
% 36.19/35.64 cnf('1.1.1.1.1.1.1.1.1',plain,[-(int_less(6 ^ [], 5 ^ []))],extension(7)).
% 36.19/35.64 cnf('1.1.1.1.1.1.2',plain,[-(5 ^ [] = n), int_leq(5 ^ [], n), -(int_less(5 ^ [], n))],extension(16,bind([[_11954, _12005], [5 ^ [], n]]))).
% 36.19/35.64 cnf('1.1.1.1.1.1.2.1',plain,[-(int_leq(5 ^ [], n))],extension(8)).
% 36.19/35.64 cnf('1.1.1.1.1.1.2.2',plain,[int_less(5 ^ [], n), -(int_less(6 ^ [], n)), int_less(6 ^ [], 5 ^ [])],extension(17,bind([[_12461, _12350, _12406], [n, 6 ^ [], 5 ^ []]]))).
% 36.19/35.64 cnf('1.1.1.1.1.1.2.2.1',plain,[int_less(6 ^ [], n)],reduction('1.1.1.1')).
% 36.19/35.64 cnf('1.1.1.1.1.1.2.2.2',plain,[-(int_less(6 ^ [], 5 ^ []))],extension(7)).
% 36.19/35.64 cnf('1.1.1.1.1.2',plain,[-(int_less(int_zero, 2 ^ [5 ^ [], 6 ^ []])), -(3 ^ [5 ^ [], 6 ^ []])],extension(2,bind([[_14818, _14759], [5 ^ [], 6 ^ []]]))).
% 36.19/35.64 cnf('1.1.1.1.1.2.1',plain,[3 ^ [5 ^ [], 6 ^ []], int_less(6 ^ [], 5 ^ [])],extension(20,bind([[_14759, _14818], [6 ^ [], 5 ^ []]]))).
% 36.19/35.64 cnf('1.1.1.1.1.2.1.1',plain,[-(int_less(6 ^ [], 5 ^ []))],extension(7)).
% 36.19/35.64 cnf('1.1.2',plain,[-(int_leq(5 ^ [], n))],extension(8)).
% 36.19/35.64 cnf('1.1.3',plain,[-(int_leq(int_one, 5 ^ [])), int_leq(int_one, 6 ^ []), int_one = int_one, 6 ^ [] = 5 ^ []],extension(14,bind([[_9397, _9464, _9530, _9595], [int_one, int_one, 6 ^ [], 5 ^ []]]))).
% 36.19/35.64 cnf('1.1.3.1',plain,[-(int_leq(int_one, 6 ^ []))],extension(6)).
% 36.19/35.64 cnf('1.1.3.2',plain,[-(int_one = int_one)],extension(11,bind([[_8489], [int_one]]))).
% 36.19/35.64 cnf('1.1.3.3',plain,[-(6 ^ [] = 5 ^ []), 5 ^ [] = 6 ^ []],extension(12,bind([[_8642, _8687], [5 ^ [], 6 ^ []]]))).
% 36.19/35.64 cnf('1.1.3.3.1',plain,[-(5 ^ [] = 6 ^ []), int_leq(5 ^ [], 6 ^ []), -(int_less(5 ^ [], 6 ^ []))],extension(16,bind([[_11954, _12005], [5 ^ [], 6 ^ []]]))).
% 36.19/35.64 cnf('1.1.3.3.1.1',plain,[-(int_leq(5 ^ [], 6 ^ [])), -(int_less(6 ^ [], 5 ^ []))],extension(19,bind([[_13147, _13192], [6 ^ [], 5 ^ []]]))).
% 36.19/35.64 cnf('1.1.3.3.1.1.1',plain,[int_less(6 ^ [], 5 ^ []), -(int_less(int_zero, 5 ^ [])), int_less(int_zero, 6 ^ [])],extension(17,bind([[_12461, _12350, _12406], [5 ^ [], int_zero, 6 ^ []]]))).
% 36.19/35.64 cnf('1.1.3.3.1.1.1.1',plain,[int_less(int_zero, 5 ^ []), -(int_leq(int_one, 5 ^ []))],extension(22,bind([[_15267], [5 ^ []]]))).
% 36.19/35.64 cnf('1.1.3.3.1.1.1.1.1',plain,[int_leq(int_one, 5 ^ [])],reduction('1.1')).
% 36.19/35.64 cnf('1.1.3.3.1.1.1.2',plain,[-(int_less(int_zero, 6 ^ [])), int_leq(int_one, 6 ^ [])],extension(23,bind([[_15267], [6 ^ []]]))).
% 36.19/35.64 cnf('1.1.3.3.1.1.1.2.1',plain,[-(int_leq(int_one, 6 ^ []))],extension(6)).
% 36.19/35.64 cnf('1.1.3.3.1.2',plain,[int_less(5 ^ [], 6 ^ []), -(int_less(5 ^ [], 5 ^ [])), int_less(6 ^ [], 5 ^ [])],extension(17,bind([[_12350, _12406, _12461], [5 ^ [], 6 ^ [], 5 ^ []]]))).
% 36.19/35.64 cnf('1.1.3.3.1.2.1',plain,[int_less(5 ^ [], 5 ^ []), 5 ^ [] = 5 ^ []],extension(18,bind([[_12817, _12864], [5 ^ [], 5 ^ []]]))).
% 36.19/35.64 cnf('1.1.3.3.1.2.1.1',plain,[-(5 ^ [] = 5 ^ [])],extension(11,bind([[_8489], [5 ^ []]]))).
% 36.19/35.64 cnf('1.1.3.3.1.2.2',plain,[-(int_less(6 ^ [], 5 ^ []))],extension(7)).
% 36.19/35.64 cnf('1.1.4',plain,[-(4 ^ [6 ^ [], 5 ^ []]), 5 ^ [] = plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]), int_less(int_zero, 2 ^ [5 ^ [], 6 ^ []]), -(a(plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]), 6 ^ []) = real_zero), int_leq(int_one, 6 ^ []), int_leq(6 ^ [], 6 ^ [])],extension(1,bind([[_15660, _16312, _16562, _15841], [5 ^ [], 2 ^ [5 ^ [], 6 ^ []], 6 ^ [], 6 ^ []]]))).
% 36.19/35.64 cnf('1.1.4.1',plain,[-(5 ^ [] = plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []])), plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]) = 5 ^ []],extension(12,bind([[_8642, _8687], [plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]), 5 ^ []]]))).
% 36.19/35.64 cnf('1.1.4.1.1',plain,[-(plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]) = 5 ^ []), -(3 ^ [5 ^ [], 6 ^ []])],extension(3,bind([[_14818, _14759], [5 ^ [], 6 ^ []]]))).
% 36.19/35.64 cnf('1.1.4.1.1.1',plain,[3 ^ [5 ^ [], 6 ^ []], int_less(6 ^ [], 5 ^ [])],extension(20,bind([[_14759, _14818], [6 ^ [], 5 ^ []]]))).
% 36.19/35.64 cnf('1.1.4.1.1.1.1',plain,[-(int_less(6 ^ [], 5 ^ []))],extension(7)).
% 36.19/35.64 cnf('1.1.4.2',plain,[-(int_less(int_zero, 2 ^ [5 ^ [], 6 ^ []])), -(3 ^ [5 ^ [], 6 ^ []])],extension(2,bind([[_14818, _14759], [5 ^ [], 6 ^ []]]))).
% 36.19/35.64 cnf('1.1.4.2.1',plain,[3 ^ [5 ^ [], 6 ^ []], int_less(6 ^ [], 5 ^ [])],extension(20,bind([[_14759, _14818], [6 ^ [], 5 ^ []]]))).
% 36.19/35.64 cnf('1.1.4.2.1.1',plain,[-(int_less(6 ^ [], 5 ^ []))],extension(7)).
% 36.19/35.64 cnf('1.1.4.3',plain,[a(plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]), 6 ^ []) = real_zero, -(real_zero = a(plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]), 6 ^ []))],extension(12,bind([[_8687, _8642], [real_zero, a(plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]), 6 ^ [])]]))).
% 36.19/35.64 cnf('1.1.4.3.1',plain,[real_zero = a(plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]), 6 ^ []), -(real_zero = a(5 ^ [], 6 ^ [])), a(plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]), 6 ^ []) = a(5 ^ [], 6 ^ [])],extension(13,bind([[_8921, _8977, _9032], [real_zero, a(plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]), 6 ^ []), a(5 ^ [], 6 ^ [])]]))).
% 36.19/35.64 cnf('1.1.4.3.1.1',plain,[real_zero = a(5 ^ [], 6 ^ []), -(a(5 ^ [], 6 ^ []) = real_zero)],extension(12,bind([[_8687, _8642], [a(5 ^ [], 6 ^ []), real_zero]]))).
% 36.19/35.64 cnf('1.1.4.3.1.1.1',plain,[a(5 ^ [], 6 ^ []) = real_zero],extension(9)).
% 36.19/35.64 cnf('1.1.4.3.1.2',plain,[-(a(plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]), 6 ^ []) = a(5 ^ [], 6 ^ [])), plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]) = 5 ^ [], 6 ^ [] = 6 ^ []],extension(10,bind([[_10665, _10732, _10798, _10863], [plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]), 5 ^ [], 6 ^ [], 6 ^ []]]))).
% 36.19/35.64 cnf('1.1.4.3.1.2.1',plain,[-(plus(6 ^ [], 2 ^ [5 ^ [], 6 ^ []]) = 5 ^ []), -(3 ^ [5 ^ [], 6 ^ []])],extension(3,bind([[_14818, _14759], [5 ^ [], 6 ^ []]]))).
% 36.19/35.64 cnf('1.1.4.3.1.2.1.1',plain,[3 ^ [5 ^ [], 6 ^ []], int_less(6 ^ [], 5 ^ [])],extension(20,bind([[_14759, _14818], [6 ^ [], 5 ^ []]]))).
% 36.19/35.64 cnf('1.1.4.3.1.2.1.1.1',plain,[-(int_less(6 ^ [], 5 ^ []))],extension(7)).
% 36.19/35.64 cnf('1.1.4.3.1.2.2',plain,[-(6 ^ [] = 6 ^ [])],extension(11,bind([[_8489], [6 ^ []]]))).
% 36.19/35.64 cnf('1.1.4.4',plain,[-(int_leq(int_one, 6 ^ []))],extension(6)).
% 36.19/35.64 cnf('1.1.4.5',plain,[-(int_leq(6 ^ [], 6 ^ [])), 1 ^ [6 ^ [], 6 ^ []]],extension(15,bind([[_12005, _11954], [6 ^ [], 6 ^ []]]))).
% 36.19/35.64 cnf('1.1.4.5.1',plain,[-(1 ^ [6 ^ [], 6 ^ []]), 6 ^ [] = 6 ^ []],extension(4,bind([[_11954, _12005], [6 ^ [], 6 ^ []]]))).
% 36.19/35.64 cnf('1.1.4.5.1.1',plain,[-(6 ^ [] = 6 ^ [])],extension(11,bind([[_8489], [6 ^ []]]))).
% 36.19/35.64 %-----------------------------------------------------
% 36.19/35.65
% 36.19/35.65 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------