%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUM335+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n006.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 : Mon Jul 18 11:40:06 EDT 2022
% Result : Theorem 0.33s 1.40s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : NUM335+1 : TPTP v8.1.0. Released v3.1.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n006.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 Jul 5 16:04:22 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.33/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.40 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.41
% 0.33/1.41 %-----------------------------------------------------
% 0.33/1.41 fof(diff_n5_n3_only_n2, conjecture, ! [_275682] : (difference(n5, n3, _275682) => _275682 = n2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', diff_n5_n3_only_n2)).
% 0.33/1.41 fof(rdn2, axiom, rdn_translate(n2, rdn_pos(rdnn(n2))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax', rdn2)).
% 0.33/1.41 fof(rdn3, axiom, rdn_translate(n3, rdn_pos(rdnn(n3))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax', rdn3)).
% 0.33/1.41 fof(rdn5, axiom, rdn_translate(n5, rdn_pos(rdnn(n5))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax', rdn5)).
% 0.33/1.41 fof(sum_entry_point_pos_pos, axiom, ! [_276331, _276334, _276337, _276340, _276343, _276346] : (rdn_translate(_276331, rdn_pos(_276340)) & rdn_translate(_276334, rdn_pos(_276343)) & rdn_add_with_carry(rdnn(n0), _276340, _276343, _276346) & rdn_translate(_276337, rdn_pos(_276346)) => sum(_276331, _276334, _276337)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+2.ax', sum_entry_point_pos_pos)).
% 0.33/1.41 fof(unique_RHS, axiom, ! [_276669, _276672, _276675, _276678] : (sum(_276669, _276672, _276678) & sum(_276669, _276675, _276678) => _276672 = _276675), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+2.ax', unique_RHS)).
% 0.33/1.41 fof(minus_entry_point, axiom, ! [_276876, _276879, _276882] : (sum(_276879, _276882, _276876) <=> difference(_276876, _276879, _276882)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+2.ax', minus_entry_point)).
% 0.33/1.41 fof(add_digit_digit_digit, axiom, ! [_277047, _277050, _277053, _277056, _277059] : (rdn_digit_add(rdnn(_277050), rdnn(_277053), rdnn(_277059), rdnn(n0)) & rdn_digit_add(rdnn(_277059), rdnn(_277047), rdnn(_277056), rdnn(n0)) => rdn_add_with_carry(rdnn(_277047), rdnn(_277050), rdnn(_277053), rdnn(_277056))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+2.ax', add_digit_digit_digit)).
% 0.33/1.41 fof(rdn_digit_add_n3_n2_n5_n0, axiom, rdn_digit_add(rdnn(n3), rdnn(n2), rdnn(n5), rdnn(n0)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+2.ax', rdn_digit_add_n3_n2_n5_n0)).
% 0.33/1.41 fof(rdn_digit_add_n5_n0_n5_n0, axiom, rdn_digit_add(rdnn(n5), rdnn(n0), rdnn(n5), rdnn(n0)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+2.ax', rdn_digit_add_n5_n0_n5_n0)).
% 0.33/1.41
% 0.33/1.41 cnf(1, plain, [-(difference(n5, n3, 1 ^ []))], clausify(diff_n5_n3_only_n2)).
% 0.33/1.41 cnf(2, plain, [1 ^ [] = n2], clausify(diff_n5_n3_only_n2)).
% 0.33/1.41 cnf(3, plain, [-(_96559 = _96559)], theory(equality)).
% 0.33/1.41 cnf(4, plain, [-(sum(_104709, _104876, _105039)), sum(_104624, _104793, _104958), _104624 = _104709, _104793 = _104876, _104958 = _105039], theory(equality)).
% 0.33/1.41 cnf(5, plain, [-(rdn_translate(n2, rdn_pos(rdnn(n2))))], clausify(rdn2)).
% 0.33/1.41 cnf(6, plain, [-(rdn_translate(n3, rdn_pos(rdnn(n3))))], clausify(rdn3)).
% 0.33/1.41 cnf(7, plain, [-(rdn_translate(n5, rdn_pos(rdnn(n5))))], clausify(rdn5)).
% 0.33/1.41 cnf(8, plain, [-(sum(_178354, _178446, _178537)), rdn_translate(_178354, rdn_pos(_178627)), rdn_translate(_178446, rdn_pos(_178716)), rdn_add_with_carry(rdnn(n0), _178627, _178716, _178804), rdn_translate(_178537, rdn_pos(_178804))], clausify(sum_entry_point_pos_pos)).
% 0.33/1.41 cnf(9, plain, [-(_186111 = _186173), sum(_186048, _186111, _186234), sum(_186048, _186173, _186234)], clausify(unique_RHS)).
% 0.33/1.41 cnf(10, plain, [-(sum(_186735, _186786, _186683)), difference(_186683, _186735, _186786)], clausify(minus_entry_point)).
% 0.33/1.41 cnf(11, plain, [-(rdn_add_with_carry(rdnn(_187144), rdnn(_187236), rdnn(_187327), rdnn(_187417))), rdn_digit_add(rdnn(_187236), rdnn(_187327), rdnn(_187506), rdnn(n0)), rdn_digit_add(rdnn(_187506), rdnn(_187144), rdnn(_187417), rdnn(n0))], clausify(add_digit_digit_digit)).
% 0.33/1.41 cnf(12, plain, [-(rdn_digit_add(rdnn(n3), rdnn(n2), rdnn(n5), rdnn(n0)))], clausify(rdn_digit_add_n3_n2_n5_n0)).
% 0.33/1.41 cnf(13, plain, [-(rdn_digit_add(rdnn(n5), rdnn(n0), rdnn(n5), rdnn(n0)))], clausify(rdn_digit_add_n5_n0_n5_n0)).
% 0.33/1.41
% 0.33/1.41 cnf('1',plain,[1 ^ [] = n2],start(2)).
% 0.33/1.41 cnf('1.1',plain,[-(1 ^ [] = n2), sum(n3, 1 ^ [], n5), sum(n3, n2, n5)],extension(9,bind([[_186111, _186048, _186173, _186234], [1 ^ [], n3, n2, n5]]))).
% 0.33/1.41 cnf('1.1.1',plain,[-(sum(n3, 1 ^ [], n5)), sum(n3, 1 ^ [], n5), n3 = n3, 1 ^ [] = 1 ^ [], n5 = n5],extension(4,bind([[_104624, _104709, _104793, _104876, _104958, _105039], [n3, n3, 1 ^ [], 1 ^ [], n5, n5]]))).
% 0.33/1.41 cnf('1.1.1.1',plain,[-(sum(n3, 1 ^ [], n5)), difference(n5, n3, 1 ^ [])],extension(10,bind([[_186683, _186735, _186786], [n5, n3, 1 ^ []]]))).
% 0.33/1.41 cnf('1.1.1.1.1',plain,[-(difference(n5, n3, 1 ^ []))],extension(1)).
% 0.33/1.41 cnf('1.1.1.2',plain,[-(n3 = n3)],extension(3,bind([[_96559], [n3]]))).
% 0.33/1.41 cnf('1.1.1.3',plain,[-(1 ^ [] = 1 ^ [])],extension(3,bind([[_96559], [1 ^ []]]))).
% 0.33/1.41 cnf('1.1.1.4',plain,[-(n5 = n5)],extension(3,bind([[_96559], [n5]]))).
% 0.33/1.41 cnf('1.1.2',plain,[-(sum(n3, n2, n5)), rdn_translate(n3, rdn_pos(rdnn(n3))), rdn_translate(n2, rdn_pos(rdnn(n2))), rdn_add_with_carry(rdnn(n0), rdnn(n3), rdnn(n2), rdnn(n5)), rdn_translate(n5, rdn_pos(rdnn(n5)))],extension(8,bind([[_178354, _178446, _178627, _178716, _178537, _178804], [n3, n2, rdnn(n3), rdnn(n2), n5, rdnn(n5)]]))).
% 0.33/1.41 cnf('1.1.2.1',plain,[-(rdn_translate(n3, rdn_pos(rdnn(n3))))],extension(6)).
% 0.33/1.41 cnf('1.1.2.2',plain,[-(rdn_translate(n2, rdn_pos(rdnn(n2))))],extension(5)).
% 0.33/1.41 cnf('1.1.2.3',plain,[-(rdn_add_with_carry(rdnn(n0), rdnn(n3), rdnn(n2), rdnn(n5))), rdn_digit_add(rdnn(n3), rdnn(n2), rdnn(n5), rdnn(n0)), rdn_digit_add(rdnn(n5), rdnn(n0), rdnn(n5), rdnn(n0))],extension(11,bind([[_187236, _187327, _187506, _187144, _187417], [n3, n2, n5, n0, n5]]))).
% 0.33/1.41 cnf('1.1.2.3.1',plain,[-(rdn_digit_add(rdnn(n3), rdnn(n2), rdnn(n5), rdnn(n0)))],extension(12)).
% 0.33/1.41 cnf('1.1.2.3.2',plain,[-(rdn_digit_add(rdnn(n5), rdnn(n0), rdnn(n5), rdnn(n0)))],extension(13)).
% 0.33/1.41 cnf('1.1.2.4',plain,[-(rdn_translate(n5, rdn_pos(rdnn(n5))))],extension(7)).
% 0.33/1.41 %-----------------------------------------------------
% 0.33/1.41
% 0.33/1.42 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------