%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KLE007+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n019.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:09:54 EDT 2022
% Result : Theorem 149.74s 144.60s
% Output : Proof 149.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : KLE007+2 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n019.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Thu Jun 16 13:34:24 EDT 2022
% 0.13/0.34 % CPUTime :
% 149.74/144.60 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 149.74/144.61 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 149.74/144.61
% 149.74/144.61 %-----------------------------------------------------
% 149.74/144.61 fof(test_3, axiom, ! [_36888, _36891] : (test(_36888) => (c(_36888) = _36891 <=> complement(_36888, _36891))), file('/export/starexec/sandbox/benchmark/Axioms/KLE001+1.ax', test_3)).
% 149.74/144.61 fof(test_2, axiom, ! [_37060, _37063] : (complement(_37063, _37060) <=> multiplication(_37060, _37063) = zero & multiplication(_37063, _37060) = zero & addition(_37060, _37063) = one), file('/export/starexec/sandbox/benchmark/Axioms/KLE001+1.ax', test_2)).
% 149.74/144.61 fof(goals, conjecture, ! [_37300, _37303] : (test(_37303) & test(_37300) => leq(one, addition(multiplication(addition(_37300, c(_37300)), _37303), multiplication(addition(_37300, c(_37300)), c(_37303)))) & leq(addition(multiplication(addition(_37300, c(_37300)), _37303), multiplication(addition(_37300, c(_37300)), c(_37303))), one)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals)).
% 149.74/144.61 fof(additive_commutativity, axiom, ! [_37726, _37729] : addition(_37726, _37729) = addition(_37729, _37726), file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', additive_commutativity)).
% 149.74/144.61 fof(additive_idempotence, axiom, ! [_37874] : addition(_37874, _37874) = _37874, file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', additive_idempotence)).
% 149.74/144.61 fof(multiplicative_right_identity, axiom, ! [_37994] : multiplication(_37994, one) = _37994, file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', multiplicative_right_identity)).
% 149.74/144.61 fof(right_distributivity, axiom, ! [_38114, _38117, _38120] : multiplication(_38114, addition(_38117, _38120)) = addition(multiplication(_38114, _38117), multiplication(_38114, _38120)), file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', right_distributivity)).
% 149.74/144.61 fof(order, axiom, ! [_38323, _38326] : (leq(_38323, _38326) <=> addition(_38323, _38326) = _38326), file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', order)).
% 149.74/144.61
% 149.74/144.61 cnf(1, plain, [-(3 ^ [_18314, _18262]), c(_18262) = _18314, -(complement(_18262, _18314))], clausify(test_3)).
% 149.74/144.61 cnf(2, plain, [-(2 ^ [_17717, _17651]), -(addition(_17651, _17717) = one)], clausify(test_2)).
% 149.74/144.61 cnf(3, plain, [-(test(5 ^ []))], clausify(goals)).
% 149.74/144.61 cnf(4, plain, [-(test(4 ^ []))], clausify(goals)).
% 149.74/144.61 cnf(5, plain, [leq(one, addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))), leq(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), one)], clausify(goals)).
% 149.74/144.61 cnf(6, plain, [-(addition(_13306, _13351) = addition(_13351, _13306))], clausify(additive_commutativity)).
% 149.74/144.61 cnf(7, plain, [-(addition(_14297, _14297) = _14297)], clausify(additive_idempotence)).
% 149.74/144.61 cnf(8, plain, [-(multiplication(_14978, one) = _14978)], clausify(multiplicative_right_identity)).
% 149.74/144.61 cnf(9, plain, [-(multiplication(_15406, addition(_15465, _15523)) = addition(multiplication(_15406, _15465), multiplication(_15406, _15523)))], clausify(right_distributivity)).
% 149.74/144.61 cnf(10, plain, [-(leq(_16850, _16898)), addition(_16850, _16898) = _16898], clausify(order)).
% 149.74/144.61 cnf(11, plain, [complement(_17717, _17651), 2 ^ [_17717, _17651]], clausify(test_2)).
% 149.74/144.61 cnf(12, plain, [test(_18262), 3 ^ [_18314, _18262]], clausify(test_3)).
% 149.74/144.61 cnf(13, plain, [-(addition(_11663, _11796) = addition(_11730, _11861)), _11663 = _11730, _11796 = _11861], theory(equality)).
% 149.74/144.61 cnf(14, plain, [_12287 = _12336, -(c(_12287) = c(_12336))], theory(equality)).
% 149.74/144.61 cnf(15, plain, [-(multiplication(_12606, _12739) = multiplication(_12673, _12804)), _12606 = _12673, _12739 = _12804], theory(equality)).
% 149.74/144.61 cnf(16, plain, [-(_9143 = _9143)], theory(equality)).
% 149.74/144.61 cnf(17, plain, [_9296 = _9341, -(_9341 = _9296)], theory(equality)).
% 149.74/144.61 cnf(18, plain, [-(_9575 = _9686), _9575 = _9631, _9631 = _9686], theory(equality)).
% 149.74/144.61 cnf(19, plain, [-(leq(_10742, _10873)), leq(_10675, _10808), _10675 = _10742, _10808 = _10873], theory(equality)).
% 149.74/144.61
% 149.74/144.61 cnf('1',plain,[complement(5 ^ [], c(5 ^ [])), 2 ^ [5 ^ [], c(5 ^ [])]],start(11,bind([[_17717, _17651], [5 ^ [], c(5 ^ [])]]))).
% 149.74/144.61 cnf('1.1',plain,[-(complement(5 ^ [], c(5 ^ []))), -(3 ^ [c(5 ^ []), 5 ^ []]), c(5 ^ []) = c(5 ^ [])],extension(1,bind([[_18262, _18314], [5 ^ [], c(5 ^ [])]]))).
% 149.74/144.61 cnf('1.1.1',plain,[3 ^ [c(5 ^ []), 5 ^ []], test(5 ^ [])],extension(12,bind([[_18314, _18262], [c(5 ^ []), 5 ^ []]]))).
% 149.74/144.61 cnf('1.1.1.1',plain,[-(test(5 ^ []))],extension(3)).
% 149.74/144.61 cnf('1.1.2',plain,[-(c(5 ^ []) = c(5 ^ [])), 5 ^ [] = 5 ^ []],extension(14,bind([[_12287, _12336], [5 ^ [], 5 ^ []]]))).
% 149.74/144.61 cnf('1.1.2.1',plain,[-(5 ^ [] = 5 ^ [])],extension(16,bind([[_9143], [5 ^ []]]))).
% 149.74/144.61 cnf('1.2',plain,[-(2 ^ [5 ^ [], c(5 ^ [])]), -(addition(c(5 ^ []), 5 ^ []) = one)],extension(2,bind([[_17651, _17717], [c(5 ^ []), 5 ^ []]]))).
% 149.74/144.61 cnf('1.2.1',plain,[addition(c(5 ^ []), 5 ^ []) = one, -(multiplication(addition(4 ^ [], c(4 ^ [])), addition(c(5 ^ []), 5 ^ [])) = multiplication(one, one)), addition(4 ^ [], c(4 ^ [])) = one],extension(15,bind([[_12739, _12804, _12606, _12673], [addition(c(5 ^ []), 5 ^ []), one, addition(4 ^ [], c(4 ^ [])), one]]))).
% 149.74/144.61 cnf('1.2.1.1',plain,[multiplication(addition(4 ^ [], c(4 ^ [])), addition(c(5 ^ []), 5 ^ [])) = multiplication(one, one), -(multiplication(addition(4 ^ [], c(4 ^ [])), addition(c(5 ^ []), 5 ^ [])) = one), multiplication(one, one) = one],extension(18,bind([[_9575, _9631, _9686], [multiplication(addition(4 ^ [], c(4 ^ [])), addition(c(5 ^ []), 5 ^ [])), multiplication(one, one), one]]))).
% 149.74/144.61 cnf('1.2.1.1.1',plain,[multiplication(addition(4 ^ [], c(4 ^ [])), addition(c(5 ^ []), 5 ^ [])) = one, -(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))) = one), addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))) = multiplication(addition(4 ^ [], c(4 ^ [])), addition(c(5 ^ []), 5 ^ []))],extension(18,bind([[_9686, _9575, _9631], [one, addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), multiplication(addition(4 ^ [], c(4 ^ [])), addition(c(5 ^ []), 5 ^ []))]]))).
% 149.74/144.61 cnf('1.2.1.1.1.1',plain,[addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))) = one, -(leq(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), one)), leq(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))), addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))) = addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))],extension(19,bind([[_10873, _10808, _10675, _10742], [one, addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))]]))).
% 149.74/144.61 cnf('1.2.1.1.1.1.1',plain,[leq(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), one), -(leq(one, addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))))), addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))) = one, one = addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))],extension(19,bind([[_10675, _10742, _10808, _10873], [addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), one, one, addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))]]))).
% 149.74/144.61 cnf('1.2.1.1.1.1.1.1',plain,[leq(one, addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))), leq(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), one)],extension(5)).
% 149.74/144.61 cnf('1.2.1.1.1.1.1.1.1',plain,[-(leq(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), one))],reduction('1.2.1.1.1.1')).
% 149.74/144.61 cnf('1.2.1.1.1.1.1.2',plain,[-(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))) = one)],reduction('1.2.1.1.1')).
% 149.74/144.61 cnf('1.2.1.1.1.1.1.3',plain,[-(one = addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))), addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))) = one],extension(17,bind([[_9296, _9341], [addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), one]]))).
% 149.74/144.61 cnf('1.2.1.1.1.1.1.3.1',plain,[-(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))) = one)],lemmata('1.2.1.1.1.1.1')).
% 149.74/144.61 cnf('1.2.1.1.1.1.2',plain,[-(leq(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))))), addition(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))) = addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))],extension(10,bind([[_16850, _16898], [addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))]]))).
% 149.74/144.61 cnf('1.2.1.1.1.1.2.1',plain,[-(addition(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))) = addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))))],extension(7,bind([[_14297], [addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))]]))).
% 149.74/144.61 cnf('1.2.1.1.1.1.3',plain,[-(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))) = addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))), multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []) = multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])) = multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))],extension(13,bind([[_11663, _11730, _11796, _11861], [multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))]]))).
% 149.74/144.61 cnf('1.2.1.1.1.1.3.1',plain,[-(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []) = multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []))],extension(16,bind([[_9143], [multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ [])]]))).
% 149.74/144.61 cnf('1.2.1.1.1.1.3.2',plain,[-(multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])) = multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])))],extension(16,bind([[_9143], [multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))]]))).
% 149.74/144.61 cnf('1.2.1.1.1.2',plain,[-(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))) = multiplication(addition(4 ^ [], c(4 ^ [])), addition(c(5 ^ []), 5 ^ []))), addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))) = addition(multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])), multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ [])), addition(multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])), multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ [])) = multiplication(addition(4 ^ [], c(4 ^ [])), addition(c(5 ^ []), 5 ^ []))],extension(18,bind([[_9575, _9631, _9686], [addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))), addition(multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])), multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ [])), multiplication(addition(4 ^ [], c(4 ^ [])), addition(c(5 ^ []), 5 ^ []))]]))).
% 149.74/144.61 cnf('1.2.1.1.1.2.1',plain,[-(addition(multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []), multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ []))) = addition(multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])), multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ [])))],extension(6,bind([[_13351, _13306], [multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])), multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ [])]]))).
% 149.74/144.61 cnf('1.2.1.1.1.2.2',plain,[-(addition(multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])), multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ [])) = multiplication(addition(4 ^ [], c(4 ^ [])), addition(c(5 ^ []), 5 ^ []))), multiplication(addition(4 ^ [], c(4 ^ [])), addition(c(5 ^ []), 5 ^ [])) = addition(multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])), multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []))],extension(17,bind([[_9296, _9341], [multiplication(addition(4 ^ [], c(4 ^ [])), addition(c(5 ^ []), 5 ^ [])), addition(multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])), multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ []))]]))).
% 149.74/144.61 cnf('1.2.1.1.1.2.2.1',plain,[-(multiplication(addition(4 ^ [], c(4 ^ [])), addition(c(5 ^ []), 5 ^ [])) = addition(multiplication(addition(4 ^ [], c(4 ^ [])), c(5 ^ [])), multiplication(addition(4 ^ [], c(4 ^ [])), 5 ^ [])))],extension(9,bind([[_15465, _15406, _15523], [c(5 ^ []), addition(4 ^ [], c(4 ^ [])), 5 ^ []]]))).
% 149.74/144.61 cnf('1.2.1.1.2',plain,[-(multiplication(one, one) = one)],extension(8,bind([[_14978], [one]]))).
% 149.74/144.61 cnf('1.2.1.2',plain,[-(addition(4 ^ [], c(4 ^ [])) = one), addition(4 ^ [], c(4 ^ [])) = addition(c(4 ^ []), 4 ^ []), addition(c(4 ^ []), 4 ^ []) = one],extension(18,bind([[_9575, _9631, _9686], [addition(4 ^ [], c(4 ^ [])), addition(c(4 ^ []), 4 ^ []), one]]))).
% 149.74/144.61 cnf('1.2.1.2.1',plain,[-(addition(4 ^ [], c(4 ^ [])) = addition(c(4 ^ []), 4 ^ []))],extension(6,bind([[_13351, _13306], [c(4 ^ []), 4 ^ []]]))).
% 149.74/144.61 cnf('1.2.1.2.2',plain,[-(addition(c(4 ^ []), 4 ^ []) = one), -(2 ^ [4 ^ [], c(4 ^ [])])],extension(2,bind([[_17717, _17651], [4 ^ [], c(4 ^ [])]]))).
% 149.74/144.61 cnf('1.2.1.2.2.1',plain,[2 ^ [4 ^ [], c(4 ^ [])], complement(4 ^ [], c(4 ^ []))],extension(11,bind([[_17717, _17651], [4 ^ [], c(4 ^ [])]]))).
% 149.74/144.61 cnf('1.2.1.2.2.1.1',plain,[-(complement(4 ^ [], c(4 ^ []))), -(3 ^ [c(4 ^ []), 4 ^ []]), c(4 ^ []) = c(4 ^ [])],extension(1,bind([[_18262, _18314], [4 ^ [], c(4 ^ [])]]))).
% 149.74/144.61 cnf('1.2.1.2.2.1.1.1',plain,[3 ^ [c(4 ^ []), 4 ^ []], test(4 ^ [])],extension(12,bind([[_18314, _18262], [c(4 ^ []), 4 ^ []]]))).
% 149.74/144.61 cnf('1.2.1.2.2.1.1.1.1',plain,[-(test(4 ^ []))],extension(4)).
% 149.74/144.61 cnf('1.2.1.2.2.1.1.2',plain,[-(c(4 ^ []) = c(4 ^ []))],extension(16,bind([[_9143], [c(4 ^ [])]]))).
% 149.74/144.61 %-----------------------------------------------------
% 149.74/144.62
% 149.74/144.62 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------