%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWV486+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n010.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:13 EDT 2022
% Result : Theorem 36.77s 35.67s
% Output : Proof 36.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV486+3 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n010.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Wed Jun 15 06:13:09 EDT 2022
% 0.12/0.34 % CPUTime :
% 36.77/35.67 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 36.77/35.68 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 36.77/35.68
% 36.77/35.68 %-----------------------------------------------------
% 36.77/35.68 fof(qii, hypothesis, ! [_41784, _41787] : (int_leq(int_one, _41784) & int_leq(_41784, n) & int_leq(int_one, _41787) & int_leq(_41787, n) => ! [_41835] : (int_less(int_zero, _41835) & _41784 = plus(_41787, _41835) => ! [_41866] : (int_leq(int_one, _41866) & int_leq(_41866, _41787) => a(plus(_41866, _41835), _41866) = real_zero)) & ! [_41866] : (int_leq(int_one, _41866) & int_leq(_41866, _41787) => a(_41866, _41866) = real_one) & ! [_41835] : (int_less(int_zero, _41835) & _41787 = plus(_41784, _41835) => ! [_41866] : (int_leq(int_one, _41866) & int_leq(_41866, _41784) => a(_41866, plus(_41866, _41835)) = real_zero))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', qii)).
% 36.77/35.68 fof(plus_and_inverse, axiom, ! [_42591, _42594] : (int_less(_42591, _42594) <=> ? [_42612] : (plus(_42591, _42612) = _42594 & int_less(int_zero, _42612))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', plus_and_inverse)).
% 36.77/35.68 fof(int_leq, axiom, ! [_42819, _42822] : (int_leq(_42819, _42822) <=> int_less(_42819, _42822) | _42819 = _42822), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', int_leq)).
% 36.77/35.68 fof(lt, conjecture, ! [_43001, _43004] : (int_leq(int_one, _43001) & int_less(_43001, _43004) & int_leq(_43004, n) => a(_43001, _43004) = real_zero), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', lt)).
% 36.77/35.68 fof(int_less_transitive, axiom, ! [_43337, _43340, _43343] : (int_less(_43337, _43340) & int_less(_43340, _43343) => int_less(_43337, _43343)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', int_less_transitive)).
% 36.77/35.68 fof(int_less_irreflexive, axiom, ! [_43522, _43525] : (int_less(_43522, _43525) => (! _43522) = _43525), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', int_less_irreflexive)).
% 36.77/35.68 fof(int_less_total, axiom, ! [_43671, _43674] : (int_less(_43671, _43674) | int_leq(_43674, _43671)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', int_less_total)).
% 36.77/35.68 fof(one_successor_of_zero, axiom, ! [_43845] : (int_less(int_zero, _43845) <=> int_leq(int_one, _43845)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', one_successor_of_zero)).
% 36.77/35.68
% 36.77/35.68 cnf(1, plain, [-(4 ^ [_15841, _15660]), _15841 = plus(_15660, _17234), int_less(int_zero, _17234), -(a(_17484, plus(_17484, _17234)) = real_zero), int_leq(int_one, _17484), int_leq(_17484, _15660)], clausify(qii)).
% 36.77/35.68 cnf(2, plain, [-(3 ^ [_14818, _14759]), -(int_less(int_zero, 2 ^ [_14818, _14759]))], clausify(plus_and_inverse)).
% 36.77/35.68 cnf(3, plain, [-(3 ^ [_14818, _14759]), -(plus(_14759, 2 ^ [_14818, _14759]) = _14818)], clausify(plus_and_inverse)).
% 36.77/35.68 cnf(4, plain, [-(1 ^ [_12005, _11954]), _11954 = _12005], clausify(int_leq)).
% 36.77/35.68 cnf(5, plain, [-(1 ^ [_12005, _11954]), int_less(_11954, _12005)], clausify(int_leq)).
% 36.77/35.68 cnf(6, plain, [-(int_leq(int_one, 5 ^ []))], clausify(lt)).
% 36.77/35.68 cnf(7, plain, [-(int_less(5 ^ [], 6 ^ []))], clausify(lt)).
% 36.77/35.68 cnf(8, plain, [-(int_leq(6 ^ [], n))], clausify(lt)).
% 36.77/35.68 cnf(9, plain, [a(5 ^ [], 6 ^ []) = real_zero], clausify(lt)).
% 36.77/35.68 cnf(10, plain, [-(a(_10665, _10798) = a(_10732, _10863)), _10665 = _10732, _10798 = _10863], theory(equality)).
% 36.77/35.68 cnf(11, plain, [-(_8489 = _8489)], theory(equality)).
% 36.77/35.68 cnf(12, plain, [_8642 = _8687, -(_8687 = _8642)], theory(equality)).
% 36.77/35.68 cnf(13, plain, [-(_8921 = _9032), _8921 = _8977, _8977 = _9032], theory(equality)).
% 36.77/35.68 cnf(14, plain, [-(int_leq(_9464, _9595)), int_leq(_9397, _9530), _9397 = _9464, _9530 = _9595], theory(equality)).
% 36.77/35.68 cnf(15, plain, [-(int_leq(_11954, _12005)), 1 ^ [_12005, _11954]], clausify(int_leq)).
% 36.77/35.68 cnf(16, plain, [int_leq(_11954, _12005), -(int_less(_11954, _12005)), -(_11954 = _12005)], clausify(int_leq)).
% 36.77/35.68 cnf(17, plain, [-(int_less(_12350, _12461)), int_less(_12350, _12406), int_less(_12406, _12461)], clausify(int_less_transitive)).
% 36.77/35.68 cnf(18, plain, [int_less(_12817, _12864), _12817 = _12864], clausify(int_less_irreflexive)).
% 36.77/35.68 cnf(19, plain, [-(int_less(_13147, _13192)), -(int_leq(_13192, _13147))], clausify(int_less_total)).
% 36.77/35.68 cnf(20, plain, [int_less(_14759, _14818), 3 ^ [_14818, _14759]], clausify(plus_and_inverse)).
% 36.77/35.68 cnf(21, plain, [-(int_less(_14759, _14818)), plus(_14759, _14936) = _14818, int_less(int_zero, _14936)], clausify(plus_and_inverse)).
% 36.77/35.68 cnf(22, plain, [int_less(int_zero, _15267), -(int_leq(int_one, _15267))], clausify(one_successor_of_zero)).
% 36.77/35.68 cnf(23, plain, [-(int_less(int_zero, _15267)), int_leq(int_one, _15267)], clausify(one_successor_of_zero)).
% 36.77/35.68 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.77/35.68
% 36.77/35.68 cnf('1',plain,[-(int_leq(int_one, 5 ^ []))],start(6)).
% 36.77/35.68 cnf('1.1',plain,[int_leq(int_one, 5 ^ []), int_leq(6 ^ [], n), int_leq(int_one, 6 ^ []), int_leq(5 ^ [], n), 4 ^ [6 ^ [], 5 ^ []]],extension(24,bind([[_15841, _15660], [6 ^ [], 5 ^ []]]))).
% 36.77/35.68 cnf('1.1.1',plain,[-(int_leq(6 ^ [], n))],extension(8)).
% 36.77/35.68 cnf('1.1.2',plain,[-(int_leq(int_one, 6 ^ [])), int_leq(int_one, 5 ^ []), int_one = int_one, 5 ^ [] = 6 ^ []],extension(14,bind([[_9397, _9464, _9530, _9595], [int_one, int_one, 5 ^ [], 6 ^ []]]))).
% 36.77/35.68 cnf('1.1.2.1',plain,[-(int_leq(int_one, 5 ^ []))],extension(6)).
% 36.77/35.68 cnf('1.1.2.2',plain,[-(int_one = int_one)],extension(11,bind([[_8489], [int_one]]))).
% 36.77/35.68 cnf('1.1.2.3',plain,[-(5 ^ [] = 6 ^ []), 6 ^ [] = 5 ^ []],extension(12,bind([[_8642, _8687], [6 ^ [], 5 ^ []]]))).
% 36.77/35.68 cnf('1.1.2.3.1',plain,[-(6 ^ [] = 5 ^ []), int_leq(6 ^ [], 5 ^ []), -(int_less(6 ^ [], 5 ^ []))],extension(16,bind([[_11954, _12005], [6 ^ [], 5 ^ []]]))).
% 36.77/35.68 cnf('1.1.2.3.1.1',plain,[-(int_leq(6 ^ [], 5 ^ [])), -(int_less(5 ^ [], 6 ^ []))],extension(19,bind([[_13147, _13192], [5 ^ [], 6 ^ []]]))).
% 36.77/35.68 cnf('1.1.2.3.1.1.1',plain,[int_less(5 ^ [], 6 ^ []), -(int_less(int_zero, 6 ^ [])), int_less(int_zero, 5 ^ [])],extension(17,bind([[_12461, _12350, _12406], [6 ^ [], int_zero, 5 ^ []]]))).
% 36.77/35.68 cnf('1.1.2.3.1.1.1.1',plain,[int_less(int_zero, 6 ^ []), -(int_leq(int_one, 6 ^ []))],extension(22,bind([[_15267], [6 ^ []]]))).
% 36.77/35.68 cnf('1.1.2.3.1.1.1.1.1',plain,[int_leq(int_one, 6 ^ [])],reduction('1.1')).
% 36.77/35.68 cnf('1.1.2.3.1.1.1.2',plain,[-(int_less(int_zero, 5 ^ [])), int_leq(int_one, 5 ^ [])],extension(23,bind([[_15267], [5 ^ []]]))).
% 36.77/35.68 cnf('1.1.2.3.1.1.1.2.1',plain,[-(int_leq(int_one, 5 ^ []))],extension(6)).
% 36.77/35.68 cnf('1.1.2.3.1.2',plain,[int_less(6 ^ [], 5 ^ []), -(int_less(6 ^ [], 6 ^ [])), int_less(5 ^ [], 6 ^ [])],extension(17,bind([[_12350, _12406, _12461], [6 ^ [], 5 ^ [], 6 ^ []]]))).
% 36.77/35.68 cnf('1.1.2.3.1.2.1',plain,[int_less(6 ^ [], 6 ^ []), 6 ^ [] = 6 ^ []],extension(18,bind([[_12817, _12864], [6 ^ [], 6 ^ []]]))).
% 36.77/35.68 cnf('1.1.2.3.1.2.1.1',plain,[-(6 ^ [] = 6 ^ [])],extension(11,bind([[_8489], [6 ^ []]]))).
% 36.77/35.68 cnf('1.1.2.3.1.2.2',plain,[-(int_less(5 ^ [], 6 ^ []))],extension(7)).
% 36.77/35.68 cnf('1.1.3',plain,[-(int_leq(5 ^ [], n)), 1 ^ [n, 5 ^ []]],extension(15,bind([[_12005, _11954], [n, 5 ^ []]]))).
% 36.77/35.68 cnf('1.1.3.1',plain,[-(1 ^ [n, 5 ^ []]), int_less(5 ^ [], n)],extension(5,bind([[_11954, _12005], [5 ^ [], n]]))).
% 36.77/35.68 cnf('1.1.3.1.1',plain,[-(int_less(5 ^ [], n)), plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]) = n, int_less(int_zero, 2 ^ [6 ^ [], 5 ^ []])],extension(21,bind([[_14759, _14818, _14936], [5 ^ [], n, 2 ^ [6 ^ [], 5 ^ []]]]))).
% 36.77/35.68 cnf('1.1.3.1.1.1',plain,[-(plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]) = n), plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]) = 6 ^ [], 6 ^ [] = n],extension(13,bind([[_8921, _8977, _9032], [plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]), 6 ^ [], n]]))).
% 36.77/35.68 cnf('1.1.3.1.1.1.1',plain,[-(plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]) = 6 ^ []), -(3 ^ [6 ^ [], 5 ^ []])],extension(3,bind([[_14818, _14759], [6 ^ [], 5 ^ []]]))).
% 36.77/35.68 cnf('1.1.3.1.1.1.1.1',plain,[3 ^ [6 ^ [], 5 ^ []], int_less(5 ^ [], 6 ^ [])],extension(20,bind([[_14759, _14818], [5 ^ [], 6 ^ []]]))).
% 36.77/35.68 cnf('1.1.3.1.1.1.1.1.1',plain,[-(int_less(5 ^ [], 6 ^ []))],extension(7)).
% 36.77/35.68 cnf('1.1.3.1.1.1.2',plain,[-(6 ^ [] = n), int_leq(6 ^ [], n), -(int_less(6 ^ [], n))],extension(16,bind([[_11954, _12005], [6 ^ [], n]]))).
% 36.77/35.68 cnf('1.1.3.1.1.1.2.1',plain,[-(int_leq(6 ^ [], n))],extension(8)).
% 36.77/35.68 cnf('1.1.3.1.1.1.2.2',plain,[int_less(6 ^ [], n), -(int_less(5 ^ [], n)), int_less(5 ^ [], 6 ^ [])],extension(17,bind([[_12461, _12350, _12406], [n, 5 ^ [], 6 ^ []]]))).
% 36.77/35.68 cnf('1.1.3.1.1.1.2.2.1',plain,[int_less(5 ^ [], n)],reduction('1.1.3.1')).
% 36.77/35.68 cnf('1.1.3.1.1.1.2.2.2',plain,[-(int_less(5 ^ [], 6 ^ []))],extension(7)).
% 36.77/35.68 cnf('1.1.3.1.1.2',plain,[-(int_less(int_zero, 2 ^ [6 ^ [], 5 ^ []])), -(3 ^ [6 ^ [], 5 ^ []])],extension(2,bind([[_14818, _14759], [6 ^ [], 5 ^ []]]))).
% 36.77/35.68 cnf('1.1.3.1.1.2.1',plain,[3 ^ [6 ^ [], 5 ^ []], int_less(5 ^ [], 6 ^ [])],extension(20,bind([[_14759, _14818], [5 ^ [], 6 ^ []]]))).
% 36.77/35.68 cnf('1.1.3.1.1.2.1.1',plain,[-(int_less(5 ^ [], 6 ^ []))],extension(7)).
% 36.77/35.68 cnf('1.1.4',plain,[-(4 ^ [6 ^ [], 5 ^ []]), 6 ^ [] = plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]), int_less(int_zero, 2 ^ [6 ^ [], 5 ^ []]), -(a(5 ^ [], plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []])) = real_zero), int_leq(int_one, 5 ^ []), int_leq(5 ^ [], 5 ^ [])],extension(1,bind([[_15841, _17234, _17484, _15660], [6 ^ [], 2 ^ [6 ^ [], 5 ^ []], 5 ^ [], 5 ^ []]]))).
% 36.77/35.68 cnf('1.1.4.1',plain,[-(6 ^ [] = plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []])), plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]) = 6 ^ []],extension(12,bind([[_8642, _8687], [plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]), 6 ^ []]]))).
% 36.77/35.68 cnf('1.1.4.1.1',plain,[-(plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]) = 6 ^ []), -(3 ^ [6 ^ [], 5 ^ []])],extension(3,bind([[_14818, _14759], [6 ^ [], 5 ^ []]]))).
% 36.77/35.68 cnf('1.1.4.1.1.1',plain,[3 ^ [6 ^ [], 5 ^ []], int_less(5 ^ [], 6 ^ [])],extension(20,bind([[_14759, _14818], [5 ^ [], 6 ^ []]]))).
% 36.77/35.68 cnf('1.1.4.1.1.1.1',plain,[-(int_less(5 ^ [], 6 ^ []))],extension(7)).
% 36.77/35.68 cnf('1.1.4.2',plain,[-(int_less(int_zero, 2 ^ [6 ^ [], 5 ^ []])), -(3 ^ [6 ^ [], 5 ^ []])],extension(2,bind([[_14818, _14759], [6 ^ [], 5 ^ []]]))).
% 36.77/35.68 cnf('1.1.4.2.1',plain,[3 ^ [6 ^ [], 5 ^ []], int_less(5 ^ [], 6 ^ [])],extension(20,bind([[_14759, _14818], [5 ^ [], 6 ^ []]]))).
% 36.77/35.68 cnf('1.1.4.2.1.1',plain,[-(int_less(5 ^ [], 6 ^ []))],extension(7)).
% 36.77/35.68 cnf('1.1.4.3',plain,[a(5 ^ [], plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []])) = real_zero, -(real_zero = a(5 ^ [], plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []])))],extension(12,bind([[_8687, _8642], [real_zero, a(5 ^ [], plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]))]]))).
% 36.77/35.68 cnf('1.1.4.3.1',plain,[real_zero = a(5 ^ [], plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []])), -(real_zero = a(5 ^ [], 6 ^ [])), a(5 ^ [], plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []])) = a(5 ^ [], 6 ^ [])],extension(13,bind([[_8921, _8977, _9032], [real_zero, a(5 ^ [], plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []])), a(5 ^ [], 6 ^ [])]]))).
% 36.77/35.68 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.77/35.68 cnf('1.1.4.3.1.1.1',plain,[a(5 ^ [], 6 ^ []) = real_zero],extension(9)).
% 36.77/35.68 cnf('1.1.4.3.1.2',plain,[-(a(5 ^ [], plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []])) = a(5 ^ [], 6 ^ [])), 5 ^ [] = 5 ^ [], plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]) = 6 ^ []],extension(10,bind([[_10665, _10732, _10798, _10863], [5 ^ [], 5 ^ [], plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]), 6 ^ []]]))).
% 36.77/35.68 cnf('1.1.4.3.1.2.1',plain,[-(5 ^ [] = 5 ^ [])],extension(11,bind([[_8489], [5 ^ []]]))).
% 36.77/35.68 cnf('1.1.4.3.1.2.2',plain,[-(plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]) = 6 ^ []), -(3 ^ [6 ^ [], 5 ^ []])],extension(3,bind([[_14818, _14759], [6 ^ [], 5 ^ []]]))).
% 36.77/35.68 cnf('1.1.4.3.1.2.2.1',plain,[3 ^ [6 ^ [], 5 ^ []], int_less(5 ^ [], 6 ^ [])],extension(20,bind([[_14759, _14818], [5 ^ [], 6 ^ []]]))).
% 36.77/35.68 cnf('1.1.4.3.1.2.2.1.1',plain,[-(int_less(5 ^ [], 6 ^ []))],extension(7)).
% 36.77/35.68 cnf('1.1.4.4',plain,[-(int_leq(int_one, 5 ^ []))],extension(6)).
% 36.77/35.68 cnf('1.1.4.5',plain,[-(int_leq(5 ^ [], 5 ^ [])), 1 ^ [5 ^ [], 5 ^ []]],extension(15,bind([[_12005, _11954], [5 ^ [], 5 ^ []]]))).
% 36.77/35.68 cnf('1.1.4.5.1',plain,[-(1 ^ [5 ^ [], 5 ^ []]), 5 ^ [] = 5 ^ []],extension(4,bind([[_11954, _12005], [5 ^ [], 5 ^ []]]))).
% 36.77/35.68 cnf('1.1.4.5.1.1',plain,[-(5 ^ [] = 5 ^ [])],extension(11,bind([[_8489], [5 ^ []]]))).
% 36.77/35.68 %-----------------------------------------------------
% 36.77/35.69
% 36.77/35.69 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------