%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWV486+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n007.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 45.07s 43.93s
% Output : Proof 45.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SWV486+2 : TPTP v8.1.0. Released v4.0.0.
% 0.10/0.12 % Command : leancop_casc.sh %s %d
% 0.14/0.33 % Computer : n007.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 600
% 0.14/0.33 % DateTime : Wed Jun 15 20:15:56 EDT 2022
% 0.14/0.34 % CPUTime :
% 45.07/43.93 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 45.07/43.94 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 45.07/43.95
% 45.07/43.95 %-----------------------------------------------------
% 45.07/43.95 fof(qil, hypothesis, ! [_42890, _42893] : (int_leq(int_one, _42890) & int_leq(_42890, n) & int_leq(int_one, _42893) & int_leq(_42893, n) => ! [_42941] : (int_less(int_zero, _42941) & _42890 = plus(_42893, _42941) => ! [_42972] : (int_leq(int_one, _42972) & int_leq(_42972, _42893) => a(plus(_42972, _42941), _42972) = lu(plus(_42972, _42941), _42972))) & ! [_42972] : (int_leq(int_one, _42972) & int_leq(_42972, _42893) => a(_42972, _42972) = real_one) & ! [_42941] : (int_less(int_zero, _42941) & _42893 = plus(_42890, _42941) => ! [_42972] : (int_leq(int_one, _42972) & int_leq(_42972, _42890) => a(_42972, plus(_42972, _42941)) = real_zero))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', qil)).
% 45.07/43.95 fof(plus_and_inverse, axiom, ! [_43729, _43732] : (int_less(_43729, _43732) <=> ? [_43750] : (plus(_43729, _43750) = _43732 & int_less(int_zero, _43750))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', plus_and_inverse)).
% 45.07/43.95 fof(int_leq, axiom, ! [_43957, _43960] : (int_leq(_43957, _43960) <=> int_less(_43957, _43960) | _43957 = _43960), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', int_leq)).
% 45.07/43.95 fof(lt, conjecture, ! [_44139, _44142] : (int_leq(int_one, _44139) & int_less(_44139, _44142) & int_leq(_44142, n) => a(_44139, _44142) = real_zero), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', lt)).
% 45.07/43.95 fof(int_less_transitive, axiom, ! [_44476, _44479, _44482] : (int_less(_44476, _44479) & int_less(_44479, _44482) => int_less(_44476, _44482)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', int_less_transitive)).
% 45.07/43.95 fof(int_less_irreflexive, axiom, ! [_44661, _44664] : (int_less(_44661, _44664) => (! _44661) = _44664), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', int_less_irreflexive)).
% 45.07/43.95 fof(int_less_total, axiom, ! [_44810, _44813] : (int_less(_44810, _44813) | int_leq(_44813, _44810)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', int_less_total)).
% 45.07/43.95 fof(one_successor_of_zero, axiom, ! [_44984] : (int_less(int_zero, _44984) <=> int_leq(int_one, _44984)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', one_successor_of_zero)).
% 45.07/43.95
% 45.07/43.95 cnf(1, plain, [-(4 ^ [_16661, _16474]), _16661 = plus(_16474, _18146), int_less(int_zero, _18146), -(a(_18396, plus(_18396, _18146)) = real_zero), int_leq(int_one, _18396), int_leq(_18396, _16474)], clausify(qil)).
% 45.07/43.95 cnf(2, plain, [-(3 ^ [_15632, _15573]), -(int_less(int_zero, 2 ^ [_15632, _15573]))], clausify(plus_and_inverse)).
% 45.07/43.95 cnf(3, plain, [-(3 ^ [_15632, _15573]), -(plus(_15573, 2 ^ [_15632, _15573]) = _15632)], clausify(plus_and_inverse)).
% 45.07/43.95 cnf(4, plain, [-(1 ^ [_12819, _12768]), _12768 = _12819], clausify(int_leq)).
% 45.07/43.95 cnf(5, plain, [-(1 ^ [_12819, _12768]), int_less(_12768, _12819)], clausify(int_leq)).
% 45.07/43.95 cnf(6, plain, [-(int_leq(int_one, 5 ^ []))], clausify(lt)).
% 45.07/43.95 cnf(7, plain, [-(int_less(5 ^ [], 6 ^ []))], clausify(lt)).
% 45.07/43.95 cnf(8, plain, [-(int_leq(6 ^ [], n))], clausify(lt)).
% 45.07/43.95 cnf(9, plain, [a(5 ^ [], 6 ^ []) = real_zero], clausify(lt)).
% 45.07/43.95 cnf(10, plain, [-(a(_10840, _10973) = a(_10907, _11038)), _10840 = _10907, _10973 = _11038], theory(equality)).
% 45.07/43.95 cnf(11, plain, [-(_8664 = _8664)], theory(equality)).
% 45.07/43.95 cnf(12, plain, [_8817 = _8862, -(_8862 = _8817)], theory(equality)).
% 45.07/43.95 cnf(13, plain, [-(_9096 = _9207), _9096 = _9152, _9152 = _9207], theory(equality)).
% 45.07/43.95 cnf(14, plain, [-(int_leq(_9639, _9770)), int_leq(_9572, _9705), _9572 = _9639, _9705 = _9770], theory(equality)).
% 45.07/43.95 cnf(15, plain, [-(int_leq(_12768, _12819)), 1 ^ [_12819, _12768]], clausify(int_leq)).
% 45.07/43.95 cnf(16, plain, [int_leq(_12768, _12819), -(int_less(_12768, _12819)), -(_12768 = _12819)], clausify(int_leq)).
% 45.07/43.95 cnf(17, plain, [-(int_less(_13164, _13275)), int_less(_13164, _13220), int_less(_13220, _13275)], clausify(int_less_transitive)).
% 45.07/43.95 cnf(18, plain, [int_less(_13631, _13678), _13631 = _13678], clausify(int_less_irreflexive)).
% 45.07/43.95 cnf(19, plain, [-(int_less(_13961, _14006)), -(int_leq(_14006, _13961))], clausify(int_less_total)).
% 45.07/43.95 cnf(20, plain, [int_less(_15573, _15632), 3 ^ [_15632, _15573]], clausify(plus_and_inverse)).
% 45.07/43.95 cnf(21, plain, [-(int_less(_15573, _15632)), plus(_15573, _15750) = _15632, int_less(int_zero, _15750)], clausify(plus_and_inverse)).
% 45.07/43.95 cnf(22, plain, [int_less(int_zero, _16081), -(int_leq(int_one, _16081))], clausify(one_successor_of_zero)).
% 45.07/43.95 cnf(23, plain, [-(int_less(int_zero, _16081)), int_leq(int_one, _16081)], clausify(one_successor_of_zero)).
% 45.07/43.95 cnf(24, plain, [int_leq(_16661, n), int_leq(int_one, _16661), int_leq(_16474, n), int_leq(int_one, _16474), 4 ^ [_16661, _16474]], clausify(qil)).
% 45.07/43.95
% 45.07/43.95 cnf('1',plain,[-(int_leq(int_one, 5 ^ []))],start(6)).
% 45.07/43.95 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([[_16661, _16474], [6 ^ [], 5 ^ []]]))).
% 45.07/43.95 cnf('1.1.1',plain,[-(int_leq(6 ^ [], n))],extension(8)).
% 45.07/43.95 cnf('1.1.2',plain,[-(int_leq(int_one, 6 ^ [])), int_leq(int_one, 5 ^ []), int_one = int_one, 5 ^ [] = 6 ^ []],extension(14,bind([[_9572, _9639, _9705, _9770], [int_one, int_one, 5 ^ [], 6 ^ []]]))).
% 45.07/43.95 cnf('1.1.2.1',plain,[-(int_leq(int_one, 5 ^ []))],extension(6)).
% 45.07/43.95 cnf('1.1.2.2',plain,[-(int_one = int_one)],extension(11,bind([[_8664], [int_one]]))).
% 45.07/43.95 cnf('1.1.2.3',plain,[-(5 ^ [] = 6 ^ []), 6 ^ [] = 5 ^ []],extension(12,bind([[_8817, _8862], [6 ^ [], 5 ^ []]]))).
% 45.07/43.95 cnf('1.1.2.3.1',plain,[-(6 ^ [] = 5 ^ []), int_leq(6 ^ [], 5 ^ []), -(int_less(6 ^ [], 5 ^ []))],extension(16,bind([[_12768, _12819], [6 ^ [], 5 ^ []]]))).
% 45.07/43.95 cnf('1.1.2.3.1.1',plain,[-(int_leq(6 ^ [], 5 ^ [])), -(int_less(5 ^ [], 6 ^ []))],extension(19,bind([[_13961, _14006], [5 ^ [], 6 ^ []]]))).
% 45.07/43.95 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([[_13275, _13164, _13220], [6 ^ [], int_zero, 5 ^ []]]))).
% 45.07/43.95 cnf('1.1.2.3.1.1.1.1',plain,[int_less(int_zero, 6 ^ []), -(int_leq(int_one, 6 ^ []))],extension(22,bind([[_16081], [6 ^ []]]))).
% 45.07/43.95 cnf('1.1.2.3.1.1.1.1.1',plain,[int_leq(int_one, 6 ^ [])],reduction('1.1')).
% 45.07/43.95 cnf('1.1.2.3.1.1.1.2',plain,[-(int_less(int_zero, 5 ^ [])), int_leq(int_one, 5 ^ [])],extension(23,bind([[_16081], [5 ^ []]]))).
% 45.07/43.95 cnf('1.1.2.3.1.1.1.2.1',plain,[-(int_leq(int_one, 5 ^ []))],extension(6)).
% 45.07/43.95 cnf('1.1.2.3.1.2',plain,[int_less(6 ^ [], 5 ^ []), -(int_less(6 ^ [], 6 ^ [])), int_less(5 ^ [], 6 ^ [])],extension(17,bind([[_13164, _13220, _13275], [6 ^ [], 5 ^ [], 6 ^ []]]))).
% 45.07/43.95 cnf('1.1.2.3.1.2.1',plain,[int_less(6 ^ [], 6 ^ []), 6 ^ [] = 6 ^ []],extension(18,bind([[_13631, _13678], [6 ^ [], 6 ^ []]]))).
% 45.07/43.95 cnf('1.1.2.3.1.2.1.1',plain,[-(6 ^ [] = 6 ^ [])],extension(11,bind([[_8664], [6 ^ []]]))).
% 45.07/43.95 cnf('1.1.2.3.1.2.2',plain,[-(int_less(5 ^ [], 6 ^ []))],extension(7)).
% 45.07/43.95 cnf('1.1.3',plain,[-(int_leq(5 ^ [], n)), 1 ^ [n, 5 ^ []]],extension(15,bind([[_12819, _12768], [n, 5 ^ []]]))).
% 45.07/43.95 cnf('1.1.3.1',plain,[-(1 ^ [n, 5 ^ []]), int_less(5 ^ [], n)],extension(5,bind([[_12768, _12819], [5 ^ [], n]]))).
% 45.07/43.95 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([[_15573, _15632, _15750], [5 ^ [], n, 2 ^ [6 ^ [], 5 ^ []]]]))).
% 45.07/43.95 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([[_9096, _9152, _9207], [plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]), 6 ^ [], n]]))).
% 45.07/43.95 cnf('1.1.3.1.1.1.1',plain,[-(plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]) = 6 ^ []), -(3 ^ [6 ^ [], 5 ^ []])],extension(3,bind([[_15632, _15573], [6 ^ [], 5 ^ []]]))).
% 45.07/43.95 cnf('1.1.3.1.1.1.1.1',plain,[3 ^ [6 ^ [], 5 ^ []], int_less(5 ^ [], 6 ^ [])],extension(20,bind([[_15573, _15632], [5 ^ [], 6 ^ []]]))).
% 45.07/43.95 cnf('1.1.3.1.1.1.1.1.1',plain,[-(int_less(5 ^ [], 6 ^ []))],extension(7)).
% 45.07/43.95 cnf('1.1.3.1.1.1.2',plain,[-(6 ^ [] = n), int_leq(6 ^ [], n), -(int_less(6 ^ [], n))],extension(16,bind([[_12768, _12819], [6 ^ [], n]]))).
% 45.07/43.95 cnf('1.1.3.1.1.1.2.1',plain,[-(int_leq(6 ^ [], n))],extension(8)).
% 45.07/43.95 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([[_13275, _13164, _13220], [n, 5 ^ [], 6 ^ []]]))).
% 45.07/43.95 cnf('1.1.3.1.1.1.2.2.1',plain,[int_less(5 ^ [], n)],reduction('1.1.3.1')).
% 45.07/43.95 cnf('1.1.3.1.1.1.2.2.2',plain,[-(int_less(5 ^ [], 6 ^ []))],extension(7)).
% 45.07/43.95 cnf('1.1.3.1.1.2',plain,[-(int_less(int_zero, 2 ^ [6 ^ [], 5 ^ []])), -(3 ^ [6 ^ [], 5 ^ []])],extension(2,bind([[_15632, _15573], [6 ^ [], 5 ^ []]]))).
% 45.07/43.95 cnf('1.1.3.1.1.2.1',plain,[3 ^ [6 ^ [], 5 ^ []], int_less(5 ^ [], 6 ^ [])],extension(20,bind([[_15573, _15632], [5 ^ [], 6 ^ []]]))).
% 45.07/43.95 cnf('1.1.3.1.1.2.1.1',plain,[-(int_less(5 ^ [], 6 ^ []))],extension(7)).
% 45.07/43.95 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([[_16661, _18146, _18396, _16474], [6 ^ [], 2 ^ [6 ^ [], 5 ^ []], 5 ^ [], 5 ^ []]]))).
% 45.07/43.95 cnf('1.1.4.1',plain,[-(6 ^ [] = plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []])), plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]) = 6 ^ []],extension(12,bind([[_8817, _8862], [plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]), 6 ^ []]]))).
% 45.07/43.95 cnf('1.1.4.1.1',plain,[-(plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]) = 6 ^ []), -(3 ^ [6 ^ [], 5 ^ []])],extension(3,bind([[_15632, _15573], [6 ^ [], 5 ^ []]]))).
% 45.07/43.95 cnf('1.1.4.1.1.1',plain,[3 ^ [6 ^ [], 5 ^ []], int_less(5 ^ [], 6 ^ [])],extension(20,bind([[_15573, _15632], [5 ^ [], 6 ^ []]]))).
% 45.07/43.95 cnf('1.1.4.1.1.1.1',plain,[-(int_less(5 ^ [], 6 ^ []))],extension(7)).
% 45.07/43.95 cnf('1.1.4.2',plain,[-(int_less(int_zero, 2 ^ [6 ^ [], 5 ^ []])), -(3 ^ [6 ^ [], 5 ^ []])],extension(2,bind([[_15632, _15573], [6 ^ [], 5 ^ []]]))).
% 45.07/43.95 cnf('1.1.4.2.1',plain,[3 ^ [6 ^ [], 5 ^ []], int_less(5 ^ [], 6 ^ [])],extension(20,bind([[_15573, _15632], [5 ^ [], 6 ^ []]]))).
% 45.07/43.95 cnf('1.1.4.2.1.1',plain,[-(int_less(5 ^ [], 6 ^ []))],extension(7)).
% 45.07/43.95 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([[_8862, _8817], [real_zero, a(5 ^ [], plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]))]]))).
% 45.07/43.95 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([[_9096, _9152, _9207], [real_zero, a(5 ^ [], plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []])), a(5 ^ [], 6 ^ [])]]))).
% 45.07/43.95 cnf('1.1.4.3.1.1',plain,[real_zero = a(5 ^ [], 6 ^ []), -(a(5 ^ [], 6 ^ []) = real_zero)],extension(12,bind([[_8862, _8817], [a(5 ^ [], 6 ^ []), real_zero]]))).
% 45.07/43.95 cnf('1.1.4.3.1.1.1',plain,[a(5 ^ [], 6 ^ []) = real_zero],extension(9)).
% 45.07/43.95 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([[_10840, _10907, _10973, _11038], [5 ^ [], 5 ^ [], plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]), 6 ^ []]]))).
% 45.07/43.95 cnf('1.1.4.3.1.2.1',plain,[-(5 ^ [] = 5 ^ [])],extension(11,bind([[_8664], [5 ^ []]]))).
% 45.07/43.95 cnf('1.1.4.3.1.2.2',plain,[-(plus(5 ^ [], 2 ^ [6 ^ [], 5 ^ []]) = 6 ^ []), -(3 ^ [6 ^ [], 5 ^ []])],extension(3,bind([[_15632, _15573], [6 ^ [], 5 ^ []]]))).
% 45.07/43.95 cnf('1.1.4.3.1.2.2.1',plain,[3 ^ [6 ^ [], 5 ^ []], int_less(5 ^ [], 6 ^ [])],extension(20,bind([[_15573, _15632], [5 ^ [], 6 ^ []]]))).
% 45.07/43.95 cnf('1.1.4.3.1.2.2.1.1',plain,[-(int_less(5 ^ [], 6 ^ []))],extension(7)).
% 45.07/43.95 cnf('1.1.4.4',plain,[-(int_leq(int_one, 5 ^ []))],extension(6)).
% 45.07/43.95 cnf('1.1.4.5',plain,[-(int_leq(5 ^ [], 5 ^ [])), 1 ^ [5 ^ [], 5 ^ []]],extension(15,bind([[_12819, _12768], [5 ^ [], 5 ^ []]]))).
% 45.07/43.95 cnf('1.1.4.5.1',plain,[-(1 ^ [5 ^ [], 5 ^ []]), 5 ^ [] = 5 ^ []],extension(4,bind([[_12768, _12819], [5 ^ [], 5 ^ []]]))).
% 45.07/43.95 cnf('1.1.4.5.1.1',plain,[-(5 ^ [] = 5 ^ [])],extension(11,bind([[_8664], [5 ^ []]]))).
% 45.07/43.95 %-----------------------------------------------------
% 45.07/43.95
% 45.07/43.95 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------