%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KLE021+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n017.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 02:10:00 EDT 2022
% Result : Theorem 148.70s 143.48s
% Output : Proof 148.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.14 % Problem : KLE021+2 : TPTP v8.1.0. Released v4.0.0.
% 0.13/0.14 % Command : leancop_casc.sh %s %d
% 0.14/0.36 % Computer : n017.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 600
% 0.14/0.36 % DateTime : Thu Jun 16 12:13:25 EDT 2022
% 0.14/0.36 % CPUTime :
% 148.70/143.48 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 148.70/143.49 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 148.70/143.50
% 148.70/143.50 %-----------------------------------------------------
% 148.70/143.50 fof(test_3, axiom, ! [_33404, _33407] : (test(_33404) => (c(_33404) = _33407 <=> complement(_33404, _33407))), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+1.ax', test_3)).
% 148.70/143.50 fof(test_2, axiom, ! [_33576, _33579] : (complement(_33579, _33576) <=> multiplication(_33576, _33579) = zero & multiplication(_33579, _33576) = zero & addition(_33576, _33579) = one), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+1.ax', test_2)).
% 148.70/143.50 fof(goals, conjecture, ! [_33816, _33819] : (test(_33819) => leq(_33816, addition(multiplication(_33819, _33816), multiplication(c(_33819), _33816))) & leq(addition(multiplication(_33819, _33816), multiplication(c(_33819), _33816)), _33816)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals)).
% 148.70/143.50 fof(additive_commutativity, axiom, ! [_34109, _34112] : addition(_34109, _34112) = addition(_34112, _34109), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax', additive_commutativity)).
% 148.70/143.50 fof(additive_idempotence, axiom, ! [_34257] : addition(_34257, _34257) = _34257, file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax', additive_idempotence)).
% 148.70/143.50 fof(multiplicative_left_identity, axiom, ! [_34378] : multiplication(one, _34378) = _34378, file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax', multiplicative_left_identity)).
% 148.70/143.50 fof(left_distributivity, axiom, ! [_34498, _34501, _34504] : multiplication(addition(_34498, _34501), _34504) = addition(multiplication(_34498, _34504), multiplication(_34501, _34504)), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax', left_distributivity)).
% 148.70/143.50 fof(order, axiom, ! [_34706, _34709] : (leq(_34706, _34709) <=> addition(_34706, _34709) = _34709), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax', order)).
% 148.70/143.50
% 148.70/143.50 cnf(1, plain, [-(3 ^ [_17998, _17946]), c(_17946) = _17998, -(complement(_17946, _17998))], clausify(test_3)).
% 148.70/143.50 cnf(2, plain, [-(2 ^ [_17401, _17335]), -(addition(_17335, _17401) = one)], clausify(test_2)).
% 148.70/143.50 cnf(3, plain, [-(test(5 ^ []))], clausify(goals)).
% 148.70/143.50 cnf(4, plain, [leq(4 ^ [], addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []))), leq(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), 4 ^ [])], clausify(goals)).
% 148.70/143.50 cnf(5, plain, [-(addition(_12990, _13035) = addition(_13035, _12990))], clausify(additive_commutativity)).
% 148.70/143.50 cnf(6, plain, [-(addition(_13981, _13981) = _13981)], clausify(additive_idempotence)).
% 148.70/143.50 cnf(7, plain, [-(multiplication(one, _14876) = _14876)], clausify(multiplicative_left_identity)).
% 148.70/143.50 cnf(8, plain, [-(multiplication(addition(_15603, _15662), _15720) = addition(multiplication(_15603, _15720), multiplication(_15662, _15720)))], clausify(left_distributivity)).
% 148.70/143.50 cnf(9, plain, [-(leq(_16534, _16582)), addition(_16534, _16582) = _16582], clausify(order)).
% 148.70/143.50 cnf(10, plain, [complement(_17401, _17335), 2 ^ [_17401, _17335]], clausify(test_2)).
% 148.70/143.50 cnf(11, plain, [test(_17946), 3 ^ [_17998, _17946]], clausify(test_3)).
% 148.70/143.50 cnf(12, plain, [-(addition(_11347, _11480) = addition(_11414, _11545)), _11347 = _11414, _11480 = _11545], theory(equality)).
% 148.70/143.50 cnf(13, plain, [_11971 = _12020, -(c(_11971) = c(_12020))], theory(equality)).
% 148.70/143.50 cnf(14, plain, [-(multiplication(_12290, _12423) = multiplication(_12357, _12488)), _12290 = _12357, _12423 = _12488], theory(equality)).
% 148.70/143.50 cnf(15, plain, [-(_8827 = _8827)], theory(equality)).
% 148.70/143.50 cnf(16, plain, [_8980 = _9025, -(_9025 = _8980)], theory(equality)).
% 148.70/143.50 cnf(17, plain, [-(_9259 = _9370), _9259 = _9315, _9315 = _9370], theory(equality)).
% 148.70/143.50 cnf(18, plain, [-(leq(_10426, _10557)), leq(_10359, _10492), _10359 = _10426, _10492 = _10557], theory(equality)).
% 148.70/143.50
% 148.70/143.50 cnf('1',plain,[complement(5 ^ [], c(5 ^ [])), 2 ^ [5 ^ [], c(5 ^ [])]],start(10,bind([[_17401, _17335], [5 ^ [], c(5 ^ [])]]))).
% 148.70/143.50 cnf('1.1',plain,[-(complement(5 ^ [], c(5 ^ []))), -(3 ^ [c(5 ^ []), 5 ^ []]), c(5 ^ []) = c(5 ^ [])],extension(1,bind([[_17946, _17998], [5 ^ [], c(5 ^ [])]]))).
% 148.70/143.50 cnf('1.1.1',plain,[3 ^ [c(5 ^ []), 5 ^ []], test(5 ^ [])],extension(11,bind([[_17998, _17946], [c(5 ^ []), 5 ^ []]]))).
% 148.70/143.50 cnf('1.1.1.1',plain,[-(test(5 ^ []))],extension(3)).
% 148.70/143.50 cnf('1.1.2',plain,[-(c(5 ^ []) = c(5 ^ [])), 5 ^ [] = 5 ^ []],extension(13,bind([[_11971, _12020], [5 ^ [], 5 ^ []]]))).
% 148.70/143.50 cnf('1.1.2.1',plain,[-(5 ^ [] = 5 ^ [])],extension(15,bind([[_8827], [5 ^ []]]))).
% 148.70/143.50 cnf('1.2',plain,[-(2 ^ [5 ^ [], c(5 ^ [])]), -(addition(c(5 ^ []), 5 ^ []) = one)],extension(2,bind([[_17335, _17401], [c(5 ^ []), 5 ^ []]]))).
% 148.70/143.50 cnf('1.2.1',plain,[addition(c(5 ^ []), 5 ^ []) = one, -(multiplication(addition(c(5 ^ []), 5 ^ []), 4 ^ []) = multiplication(one, 4 ^ [])), 4 ^ [] = 4 ^ []],extension(14,bind([[_12290, _12357, _12423, _12488], [addition(c(5 ^ []), 5 ^ []), one, 4 ^ [], 4 ^ []]]))).
% 148.70/143.50 cnf('1.2.1.1',plain,[multiplication(addition(c(5 ^ []), 5 ^ []), 4 ^ []) = multiplication(one, 4 ^ []), -(multiplication(addition(c(5 ^ []), 5 ^ []), 4 ^ []) = 4 ^ []), multiplication(one, 4 ^ []) = 4 ^ []],extension(17,bind([[_9259, _9315, _9370], [multiplication(addition(c(5 ^ []), 5 ^ []), 4 ^ []), multiplication(one, 4 ^ []), 4 ^ []]]))).
% 148.70/143.50 cnf('1.2.1.1.1',plain,[multiplication(addition(c(5 ^ []), 5 ^ []), 4 ^ []) = 4 ^ [], -(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])) = 4 ^ []), addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])) = multiplication(addition(c(5 ^ []), 5 ^ []), 4 ^ [])],extension(17,bind([[_9370, _9259, _9315], [4 ^ [], addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), multiplication(addition(c(5 ^ []), 5 ^ []), 4 ^ [])]]))).
% 148.70/143.50 cnf('1.2.1.1.1.1',plain,[addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])) = 4 ^ [], -(leq(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), 4 ^ [])), leq(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []))), addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])) = addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []))],extension(18,bind([[_10557, _10492, _10359, _10426], [4 ^ [], addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []))]]))).
% 148.70/143.50 cnf('1.2.1.1.1.1.1',plain,[leq(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), 4 ^ []), -(leq(4 ^ [], addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])))), addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])) = 4 ^ [], 4 ^ [] = addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []))],extension(18,bind([[_10359, _10426, _10492, _10557], [addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), 4 ^ [], 4 ^ [], addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []))]]))).
% 148.70/143.50 cnf('1.2.1.1.1.1.1.1',plain,[leq(4 ^ [], addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []))), leq(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), 4 ^ [])],extension(4)).
% 148.70/143.50 cnf('1.2.1.1.1.1.1.1.1',plain,[-(leq(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), 4 ^ []))],reduction('1.2.1.1.1.1')).
% 148.70/143.50 cnf('1.2.1.1.1.1.1.2',plain,[-(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])) = 4 ^ [])],reduction('1.2.1.1.1')).
% 148.70/143.50 cnf('1.2.1.1.1.1.1.3',plain,[-(4 ^ [] = addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []))), addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])) = 4 ^ []],extension(16,bind([[_8980, _9025], [addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), 4 ^ []]]))).
% 148.70/143.50 cnf('1.2.1.1.1.1.1.3.1',plain,[-(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])) = 4 ^ [])],lemmata('1.2.1.1.1.1.1')).
% 148.70/143.50 cnf('1.2.1.1.1.1.2',plain,[-(leq(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])))), addition(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []))) = addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []))],extension(9,bind([[_16534, _16582], [addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []))]]))).
% 148.70/143.50 cnf('1.2.1.1.1.1.2.1',plain,[-(addition(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []))) = addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])))],extension(6,bind([[_13981], [addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []))]]))).
% 148.70/143.50 cnf('1.2.1.1.1.1.3',plain,[-(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])) = addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []))), multiplication(5 ^ [], 4 ^ []) = multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []) = multiplication(c(5 ^ []), 4 ^ [])],extension(12,bind([[_11347, _11414, _11480, _11545], [multiplication(5 ^ [], 4 ^ []), multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])]]))).
% 148.70/143.50 cnf('1.2.1.1.1.1.3.1',plain,[-(multiplication(5 ^ [], 4 ^ []) = multiplication(5 ^ [], 4 ^ []))],extension(15,bind([[_8827], [multiplication(5 ^ [], 4 ^ [])]]))).
% 148.70/143.50 cnf('1.2.1.1.1.1.3.2',plain,[-(multiplication(c(5 ^ []), 4 ^ []) = multiplication(c(5 ^ []), 4 ^ []))],extension(15,bind([[_8827], [multiplication(c(5 ^ []), 4 ^ [])]]))).
% 148.70/143.50 cnf('1.2.1.1.1.2',plain,[-(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])) = multiplication(addition(c(5 ^ []), 5 ^ []), 4 ^ [])), addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])) = addition(multiplication(c(5 ^ []), 4 ^ []), multiplication(5 ^ [], 4 ^ [])), addition(multiplication(c(5 ^ []), 4 ^ []), multiplication(5 ^ [], 4 ^ [])) = multiplication(addition(c(5 ^ []), 5 ^ []), 4 ^ [])],extension(17,bind([[_9259, _9315, _9370], [addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])), addition(multiplication(c(5 ^ []), 4 ^ []), multiplication(5 ^ [], 4 ^ [])), multiplication(addition(c(5 ^ []), 5 ^ []), 4 ^ [])]]))).
% 148.70/143.50 cnf('1.2.1.1.1.2.1',plain,[-(addition(multiplication(5 ^ [], 4 ^ []), multiplication(c(5 ^ []), 4 ^ [])) = addition(multiplication(c(5 ^ []), 4 ^ []), multiplication(5 ^ [], 4 ^ [])))],extension(5,bind([[_13035, _12990], [multiplication(c(5 ^ []), 4 ^ []), multiplication(5 ^ [], 4 ^ [])]]))).
% 148.70/143.50 cnf('1.2.1.1.1.2.2',plain,[-(addition(multiplication(c(5 ^ []), 4 ^ []), multiplication(5 ^ [], 4 ^ [])) = multiplication(addition(c(5 ^ []), 5 ^ []), 4 ^ [])), multiplication(addition(c(5 ^ []), 5 ^ []), 4 ^ []) = addition(multiplication(c(5 ^ []), 4 ^ []), multiplication(5 ^ [], 4 ^ []))],extension(16,bind([[_8980, _9025], [multiplication(addition(c(5 ^ []), 5 ^ []), 4 ^ []), addition(multiplication(c(5 ^ []), 4 ^ []), multiplication(5 ^ [], 4 ^ []))]]))).
% 148.70/143.50 cnf('1.2.1.1.1.2.2.1',plain,[-(multiplication(addition(c(5 ^ []), 5 ^ []), 4 ^ []) = addition(multiplication(c(5 ^ []), 4 ^ []), multiplication(5 ^ [], 4 ^ [])))],extension(8,bind([[_15603, _15662, _15720], [c(5 ^ []), 5 ^ [], 4 ^ []]]))).
% 148.70/143.50 cnf('1.2.1.1.2',plain,[-(multiplication(one, 4 ^ []) = 4 ^ [])],extension(7,bind([[_14876], [4 ^ []]]))).
% 148.70/143.50 cnf('1.2.1.2',plain,[-(4 ^ [] = 4 ^ [])],extension(15,bind([[_8827], [4 ^ []]]))).
% 148.70/143.50 %-----------------------------------------------------
% 148.70/143.50
% 148.70/143.50 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------