%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUM432+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n003.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:46 EDT 2022
% Result : Theorem 4.37s 4.49s
% Output : Proof 4.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM432+3 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n003.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 : Wed Jul 6 03:24:56 EDT 2022
% 0.12/0.33 % CPUTime :
% 4.37/4.49 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.37/4.50 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.37/4.50
% 4.37/4.50 %-----------------------------------------------------
% 4.37/4.50 fof(m__, conjecture, ? [_68666] : (aInteger0(_68666) & sdtasdt0(xq, _68666) = sdtpldt0(xa, smndt0(xc))) | aDivisorOf0(xq, sdtpldt0(xa, smndt0(xc))) | sdteqdtlpzmzozddtrp0(xa, xc, xq), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 4.37/4.50 fof(mIntZero, axiom, aInteger0(sz00), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mIntZero)).
% 4.37/4.50 fof(mIntNeg, axiom, ! [_69064] : (aInteger0(_69064) => aInteger0(smndt0(_69064))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mIntNeg)).
% 4.37/4.50 fof(mIntPlus, axiom, ! [_69194, _69197] : (aInteger0(_69194) & aInteger0(_69197) => aInteger0(sdtpldt0(_69194, _69197))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mIntPlus)).
% 4.37/4.50 fof(mIntMult, axiom, ! [_69363, _69366] : (aInteger0(_69363) & aInteger0(_69366) => aInteger0(sdtasdt0(_69363, _69366))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mIntMult)).
% 4.37/4.50 fof(mAddZero, axiom, ! [_69534] : (aInteger0(_69534) => sdtpldt0(_69534, sz00) = _69534 & _69534 = sdtpldt0(sz00, _69534)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mAddZero)).
% 4.37/4.50 fof(mAddNeg, axiom, ! [_69715] : (aInteger0(_69715) => sdtpldt0(_69715, smndt0(_69715)) = sz00 & sz00 = sdtpldt0(smndt0(_69715), _69715)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mAddNeg)).
% 4.37/4.50 fof(mMulZero, axiom, ! [_69920] : (aInteger0(_69920) => sdtasdt0(_69920, sz00) = sz00 & sz00 = sdtasdt0(sz00, _69920)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mMulZero)).
% 4.37/4.50 fof(mZeroDiv, axiom, ! [_70103, _70106] : (aInteger0(_70103) & aInteger0(_70106) => sdtasdt0(_70103, _70106) = sz00 => _70103 = sz00 | _70106 = sz00), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mZeroDiv)).
% 4.37/4.50 fof(mDivisor, definition, ! [_70323] : (aInteger0(_70323) => ! [_70338] : (aDivisorOf0(_70338, _70323) <=> aInteger0(_70338) & (! _70338) = sz00 & ? [_70371] : (aInteger0(_70371) & sdtasdt0(_70338, _70371) = _70323))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDivisor)).
% 4.37/4.50 fof(mEquMod, definition, ! [_70650, _70653, _70656] : (aInteger0(_70650) & aInteger0(_70653) & aInteger0(_70656) & (! _70656) = sz00 => (sdteqdtlpzmzozddtrp0(_70650, _70653, _70656) <=> aDivisorOf0(_70656, sdtpldt0(_70650, smndt0(_70653))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mEquMod)).
% 4.37/4.50 fof(mEquModRef, axiom, ! [_70934, _70937] : (aInteger0(_70934) & aInteger0(_70937) & (! _70937) = sz00 => sdteqdtlpzmzozddtrp0(_70934, _70934, _70937)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mEquModRef)).
% 4.37/4.50 fof(m__818, hypothesis, aInteger0(xa) & aInteger0(xb) & aInteger0(xq) & (! xq) = sz00 & aInteger0(xc), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__818)).
% 4.37/4.50 fof(m__853, hypothesis, ? [_71247] : (aInteger0(_71247) & sdtasdt0(xq, _71247) = sdtpldt0(xa, smndt0(xb))) & aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))) & sdteqdtlpzmzozddtrp0(xa, xb, xq) & ? [_71247] : (aInteger0(_71247) & sdtasdt0(xq, _71247) = sdtpldt0(xb, smndt0(xc))) & aDivisorOf0(xq, sdtpldt0(xb, smndt0(xc))) & sdteqdtlpzmzozddtrp0(xb, xc, xq), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__853)).
% 4.37/4.50 fof(m__876, hypothesis, aInteger0(xn) & sdtasdt0(xq, xn) = sdtpldt0(xa, smndt0(xb)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__876)).
% 4.37/4.50 fof(m__899, hypothesis, aInteger0(xm) & sdtasdt0(xq, xm) = sdtpldt0(xb, smndt0(xc)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__899)).
% 4.37/4.50 fof(m__924, hypothesis, sdtasdt0(xq, sdtpldt0(xn, xm)) = sdtpldt0(xa, smndt0(xc)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__924)).
% 4.37/4.50
% 4.37/4.50 cnf(1, plain, [aInteger0(_32317), sdtasdt0(xq, _32317) = sdtpldt0(xa, smndt0(xc))], clausify(m__)).
% 4.37/4.50 cnf(2, plain, [-(sdtasdt0(_17960, _18093) = sdtasdt0(_18027, _18158)), _17960 = _18027, _18093 = _18158], theory(equality)).
% 4.37/4.50 cnf(3, plain, [_19198 = _19247, -(smndt0(_19198) = smndt0(_19247))], theory(equality)).
% 4.37/4.50 cnf(4, plain, [-(sdtpldt0(_18584, _18717) = sdtpldt0(_18651, _18782)), _18584 = _18651, _18717 = _18782], theory(equality)).
% 4.37/4.50 cnf(5, plain, [-(_15039 = _15039)], theory(equality)).
% 4.37/4.50 cnf(6, plain, [_15192 = _15237, -(_15237 = _15192)], theory(equality)).
% 4.37/4.50 cnf(7, plain, [-(_15471 = _15582), _15471 = _15527, _15527 = _15582], theory(equality)).
% 4.37/4.50 cnf(8, plain, [-(aDivisorOf0(_16014, _16145)), aDivisorOf0(_15947, _16080), _15947 = _16014, _16080 = _16145], theory(equality)).
% 4.37/4.50 cnf(9, plain, [-(aInteger0(_16620)), _16571 = _16620, aInteger0(_16571)], theory(equality)).
% 4.37/4.50 cnf(10, plain, [-(aInteger0(sz00))], clausify(mIntZero)).
% 4.37/4.50 cnf(11, plain, [aInteger0(_20046), -(aInteger0(smndt0(_20046)))], clausify(mIntNeg)).
% 4.37/4.50 cnf(12, plain, [-(aInteger0(sdtpldt0(_20274, _20325))), aInteger0(_20274), aInteger0(_20325)], clausify(mIntPlus)).
% 4.37/4.50 cnf(13, plain, [-(aInteger0(sdtasdt0(_20644, _20695))), aInteger0(_20644), aInteger0(_20695)], clausify(mIntMult)).
% 4.37/4.50 cnf(14, plain, [aInteger0(_22121), -(sdtpldt0(_22121, sz00) = _22121)], clausify(mAddZero)).
% 4.37/4.50 cnf(15, plain, [aInteger0(_22513), -(sdtpldt0(_22513, smndt0(_22513)) = sz00)], clausify(mAddNeg)).
% 4.37/4.50 cnf(16, plain, [aInteger0(_25479), -(sdtasdt0(_25479, sz00) = sz00)], clausify(mMulZero)).
% 4.37/4.50 cnf(17, plain, [aInteger0(_26395), aInteger0(_26331), sdtasdt0(_26331, _26395) = sz00, -(_26331 = sz00), -(_26395 = sz00)], clausify(mZeroDiv)).
% 4.37/4.50 cnf(18, plain, [aInteger0(_26896), aDivisorOf0(_27010, _26896), -(aInteger0(_27010))], clausify(mDivisor)).
% 4.37/4.50 cnf(19, plain, [aInteger0(_26896), aDivisorOf0(_27010, _26896), _27010 = sz00], clausify(mDivisor)).
% 4.37/4.50 cnf(20, plain, [aInteger0(_26896), -(aDivisorOf0(_27010, _26896)), aInteger0(_27010), -(_27010 = sz00), aInteger0(_27253), sdtasdt0(_27010, _27253) = _26896], clausify(mDivisor)).
% 4.37/4.50 cnf(21, plain, [-(_27764 = sz00), aInteger0(_27764), aInteger0(_27686), aInteger0(_27607), sdteqdtlpzmzozddtrp0(_27607, _27686, _27764), -(aDivisorOf0(_27764, sdtpldt0(_27607, smndt0(_27686))))], clausify(mEquMod)).
% 4.37/4.50 cnf(22, plain, [-(sdteqdtlpzmzozddtrp0(_28411, _28411, _28469)), aInteger0(_28411), aInteger0(_28469), -(_28469 = sz00)], clausify(mEquModRef)).
% 4.37/4.50 cnf(23, plain, [-(aInteger0(xa))], clausify(m__818)).
% 4.37/4.50 cnf(24, plain, [-(aInteger0(xb))], clausify(m__818)).
% 4.37/4.50 cnf(25, plain, [-(aInteger0(xq))], clausify(m__818)).
% 4.37/4.50 cnf(26, plain, [xq = sz00], clausify(m__818)).
% 4.37/4.50 cnf(27, plain, [-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))))], clausify(m__853)).
% 4.37/4.50 cnf(28, plain, [-(aInteger0(xn))], clausify(m__876)).
% 4.37/4.50 cnf(29, plain, [-(aInteger0(xm))], clausify(m__899)).
% 4.37/4.50 cnf(30, plain, [-(sdtasdt0(xq, sdtpldt0(xn, xm)) = sdtpldt0(xa, smndt0(xc)))], clausify(m__924)).
% 4.37/4.50
% 4.37/4.50 cnf('1',plain,[aInteger0(sz00), aDivisorOf0(xq, sz00), xq = sz00],start(19,bind([[_26896, _27010], [sz00, xq]]))).
% 4.37/4.50 cnf('1.1',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.2',plain,[-(aDivisorOf0(xq, sz00)), aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))), xq = xq, sdtpldt0(xa, smndt0(xb)) = sz00],extension(8,bind([[_15947, _16014, _16080, _16145], [xq, xq, sdtpldt0(xa, smndt0(xb)), sz00]]))).
% 4.37/4.50 cnf('1.2.1',plain,[-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb)))), aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))), xq = xq, sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))],extension(8,bind([[_15947, _16014, _16080, _16145], [xq, xq, sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb))]]))).
% 4.37/4.50 cnf('1.2.1.1',plain,[-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb)))), aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))), xq = xq, sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))],extension(8,bind([[_15947, _16014, _16080, _16145], [xq, xq, sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb))]]))).
% 4.37/4.50 cnf('1.2.1.1.1',plain,[-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb)))), aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))), xq = xq, sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))],extension(8,bind([[_15947, _16014, _16080, _16145], [xq, xq, sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb))]]))).
% 4.37/4.50 cnf('1.2.1.1.1.1',plain,[-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb)))), aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))), xq = xq, sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))],extension(8,bind([[_15947, _16014, _16080, _16145], [xq, xq, sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb))]]))).
% 4.37/4.50 cnf('1.2.1.1.1.1.1',plain,[-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))))],extension(27)).
% 4.37/4.50 cnf('1.2.1.1.1.1.2',plain,[-(xq = xq)],extension(5,bind([[_15039], [xq]]))).
% 4.37/4.50 cnf('1.2.1.1.1.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb)))],extension(5,bind([[_15039], [sdtpldt0(xa, smndt0(xb))]]))).
% 4.37/4.50 cnf('1.2.1.1.1.2',plain,[-(xq = xq)],extension(5,bind([[_15039], [xq]]))).
% 4.37/4.50 cnf('1.2.1.1.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))), xa = xa, smndt0(xb) = smndt0(xb)],extension(4,bind([[_18584, _18651, _18717, _18782], [xa, xa, smndt0(xb), smndt0(xb)]]))).
% 4.37/4.50 cnf('1.2.1.1.1.3.1',plain,[-(xa = xa)],extension(5,bind([[_15039], [xa]]))).
% 4.37/4.50 cnf('1.2.1.1.1.3.2',plain,[-(smndt0(xb) = smndt0(xb))],extension(5,bind([[_15039], [smndt0(xb)]]))).
% 4.37/4.50 cnf('1.2.1.1.2',plain,[-(xq = xq)],extension(5,bind([[_15039], [xq]]))).
% 4.37/4.50 cnf('1.2.1.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))), xa = xa, smndt0(xb) = smndt0(xb)],extension(4,bind([[_18584, _18651, _18717, _18782], [xa, xa, smndt0(xb), smndt0(xb)]]))).
% 4.37/4.50 cnf('1.2.1.1.3.1',plain,[-(xa = xa)],extension(5,bind([[_15039], [xa]]))).
% 4.37/4.50 cnf('1.2.1.1.3.2',plain,[-(smndt0(xb) = smndt0(xb)), xb = xb],extension(3,bind([[_19198, _19247], [xb, xb]]))).
% 4.37/4.50 cnf('1.2.1.1.3.2.1',plain,[-(xb = xb)],extension(5,bind([[_15039], [xb]]))).
% 4.37/4.50 cnf('1.2.1.2',plain,[-(xq = xq)],extension(5,bind([[_15039], [xq]]))).
% 4.37/4.50 cnf('1.2.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))), xa = xa, smndt0(xb) = smndt0(xb)],extension(4,bind([[_18584, _18651, _18717, _18782], [xa, xa, smndt0(xb), smndt0(xb)]]))).
% 4.37/4.50 cnf('1.2.1.3.1',plain,[-(xa = xa)],extension(5,bind([[_15039], [xa]]))).
% 4.37/4.50 cnf('1.2.1.3.2',plain,[-(smndt0(xb) = smndt0(xb)), xb = xb],extension(3,bind([[_19198, _19247], [xb, xb]]))).
% 4.37/4.50 cnf('1.2.1.3.2.1',plain,[-(xb = xb)],extension(5,bind([[_15039], [xb]]))).
% 4.37/4.50 cnf('1.2.2',plain,[-(xq = xq)],extension(5,bind([[_15039], [xq]]))).
% 4.37/4.50 cnf('1.2.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sz00), aInteger0(sz00), aInteger0(sdtpldt0(xa, smndt0(xb))), sdtasdt0(sdtpldt0(xa, smndt0(xb)), sz00) = sz00, -(sz00 = sz00)],extension(17,bind([[_26331, _26395], [sdtpldt0(xa, smndt0(xb)), sz00]]))).
% 4.37/4.50 cnf('1.2.3.1',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.2.3.2',plain,[-(aInteger0(sdtpldt0(xa, smndt0(xb)))), aInteger0(xa), aInteger0(smndt0(xb))],extension(12,bind([[_20274, _20325], [xa, smndt0(xb)]]))).
% 4.37/4.50 cnf('1.2.3.2.1',plain,[-(aInteger0(xa))],extension(23)).
% 4.37/4.50 cnf('1.2.3.2.2',plain,[-(aInteger0(smndt0(xb))), aInteger0(xb)],extension(11,bind([[_20046], [xb]]))).
% 4.37/4.50 cnf('1.2.3.2.2.1',plain,[-(aInteger0(xb))],extension(24)).
% 4.37/4.50 cnf('1.2.3.3',plain,[-(sdtasdt0(sdtpldt0(xa, smndt0(xb)), sz00) = sz00), aInteger0(sdtpldt0(xa, smndt0(xb)))],extension(16,bind([[_25479], [sdtpldt0(xa, smndt0(xb))]]))).
% 4.37/4.50 cnf('1.2.3.3.1',plain,[-(aInteger0(sdtpldt0(xa, smndt0(xb))))],lemmata('1.2.3')).
% 4.37/4.50 cnf('1.2.3.4',plain,[sz00 = sz00, -(sdtasdt0(xq, sz00) = sdtasdt0(sz00, sz00)), xq = sz00],extension(2,bind([[_18093, _18158, _17960, _18027], [sz00, sz00, xq, sz00]]))).
% 4.37/4.50 cnf('1.2.3.4.1',plain,[sdtasdt0(xq, sz00) = sdtasdt0(sz00, sz00), -(aDivisorOf0(sdtasdt0(sz00, sz00), sz00)), aDivisorOf0(sdtasdt0(xq, sz00), sdtpldt0(sdtasdt0(sz00, sz00), smndt0(sdtasdt0(sz00, sz00)))), sdtpldt0(sdtasdt0(sz00, sz00), smndt0(sdtasdt0(sz00, sz00))) = sz00],extension(8,bind([[_16014, _15947, _16080, _16145], [sdtasdt0(sz00, sz00), sdtasdt0(xq, sz00), sdtpldt0(sdtasdt0(sz00, sz00), smndt0(sdtasdt0(sz00, sz00))), sz00]]))).
% 4.37/4.50 cnf('1.2.3.4.1.1',plain,[aDivisorOf0(sdtasdt0(sz00, sz00), sz00), aInteger0(sz00), sdtasdt0(sz00, sz00) = sz00],extension(19,bind([[_26896, _27010], [sz00, sdtasdt0(sz00, sz00)]]))).
% 4.37/4.50 cnf('1.2.3.4.1.1.1',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.2.3.4.1.1.2',plain,[-(sdtasdt0(sz00, sz00) = sz00), aInteger0(sz00)],extension(16,bind([[_25479], [sz00]]))).
% 4.37/4.50 cnf('1.2.3.4.1.1.2.1',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.2.3.4.1.2',plain,[-(aDivisorOf0(sdtasdt0(xq, sz00), sdtpldt0(sdtasdt0(sz00, sz00), smndt0(sdtasdt0(sz00, sz00))))), -(sdtasdt0(xq, sz00) = sz00), aInteger0(sdtasdt0(xq, sz00)), aInteger0(sdtasdt0(sz00, sz00)), aInteger0(sdtasdt0(sz00, sz00)), sdteqdtlpzmzozddtrp0(sdtasdt0(sz00, sz00), sdtasdt0(sz00, sz00), sdtasdt0(xq, sz00))],extension(21,bind([[_27607, _27686, _27764], [sdtasdt0(sz00, sz00), sdtasdt0(sz00, sz00), sdtasdt0(xq, sz00)]]))).
% 4.37/4.50 cnf('1.2.3.4.1.2.1',plain,[sdtasdt0(xq, sz00) = sz00, aInteger0(sz00), -(aDivisorOf0(xq, sz00)), aInteger0(xq), -(xq = sz00), aInteger0(sz00)],extension(20,bind([[_26896, _27010, _27253], [sz00, xq, sz00]]))).
% 4.37/4.50 cnf('1.2.3.4.1.2.1.1',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.2.3.4.1.2.1.2',plain,[aDivisorOf0(xq, sz00)],reduction('1')).
% 4.37/4.50 cnf('1.2.3.4.1.2.1.3',plain,[-(aInteger0(xq))],extension(25)).
% 4.37/4.50 cnf('1.2.3.4.1.2.1.4',plain,[xq = sz00],extension(26)).
% 4.37/4.50 cnf('1.2.3.4.1.2.1.5',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.2.3.4.1.2.2',plain,[-(aInteger0(sdtasdt0(xq, sz00))), aInteger0(xq), aInteger0(sz00)],extension(13,bind([[_20644, _20695], [xq, sz00]]))).
% 4.37/4.50 cnf('1.2.3.4.1.2.2.1',plain,[-(aInteger0(xq))],extension(25)).
% 4.37/4.50 cnf('1.2.3.4.1.2.2.2',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.2.3.4.1.2.3',plain,[-(aInteger0(sdtasdt0(sz00, sz00))), sdtasdt0(xq, sz00) = sdtasdt0(sz00, sz00), aInteger0(sdtasdt0(xq, sz00))],extension(9,bind([[_16620, _16571], [sdtasdt0(sz00, sz00), sdtasdt0(xq, sz00)]]))).
% 4.37/4.50 cnf('1.2.3.4.1.2.3.1',plain,[-(sdtasdt0(xq, sz00) = sdtasdt0(sz00, sz00))],reduction('1.2.3.4')).
% 4.37/4.50 cnf('1.2.3.4.1.2.3.2',plain,[-(aInteger0(sdtasdt0(xq, sz00)))],lemmata('1.2.3.4.1.2')).
% 4.37/4.50 cnf('1.2.3.4.1.2.4',plain,[-(aInteger0(sdtasdt0(sz00, sz00))), sdtasdt0(xq, sz00) = sdtasdt0(sz00, sz00), aInteger0(sdtasdt0(xq, sz00))],extension(9,bind([[_16620, _16571], [sdtasdt0(sz00, sz00), sdtasdt0(xq, sz00)]]))).
% 4.37/4.50 cnf('1.2.3.4.1.2.4.1',plain,[-(sdtasdt0(xq, sz00) = sdtasdt0(sz00, sz00))],reduction('1.2.3.4')).
% 4.37/4.50 cnf('1.2.3.4.1.2.4.2',plain,[-(aInteger0(sdtasdt0(xq, sz00)))],lemmata('1.2.3.4.1.2')).
% 4.37/4.50 cnf('1.2.3.4.1.2.5',plain,[-(sdteqdtlpzmzozddtrp0(sdtasdt0(sz00, sz00), sdtasdt0(sz00, sz00), sdtasdt0(xq, sz00))), aInteger0(sdtasdt0(sz00, sz00)), aInteger0(sdtasdt0(xq, sz00)), -(sdtasdt0(xq, sz00) = sz00)],extension(22,bind([[_28411, _28469], [sdtasdt0(sz00, sz00), sdtasdt0(xq, sz00)]]))).
% 4.37/4.50 cnf('1.2.3.4.1.2.5.1',plain,[-(aInteger0(sdtasdt0(sz00, sz00)))],lemmata('1.2.3.4.1.2')).
% 4.37/4.50 cnf('1.2.3.4.1.2.5.2',plain,[-(aInteger0(sdtasdt0(xq, sz00)))],lemmata('1.2.3.4.1.2')).
% 4.37/4.50 cnf('1.2.3.4.1.2.5.3',plain,[sdtasdt0(xq, sz00) = sz00],lemmata('1.2.3.4.1.2')).
% 4.37/4.50 cnf('1.2.3.4.1.3',plain,[-(sdtpldt0(sdtasdt0(sz00, sz00), smndt0(sdtasdt0(sz00, sz00))) = sz00), aInteger0(sdtasdt0(sz00, sz00))],extension(15,bind([[_22513], [sdtasdt0(sz00, sz00)]]))).
% 4.37/4.50 cnf('1.2.3.4.1.3.1',plain,[-(aInteger0(sdtasdt0(sz00, sz00))), aInteger0(sz00), aInteger0(sz00)],extension(13,bind([[_20644, _20695], [sz00, sz00]]))).
% 4.37/4.50 cnf('1.2.3.4.1.3.1.1',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.2.3.4.1.3.1.2',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.2.3.4.2',plain,[-(xq = sz00), aInteger0(sz00), -(aDivisorOf0(xq, sz00)), aInteger0(xq), aInteger0(sz00), sdtasdt0(xq, sz00) = sz00],extension(20,bind([[_27010, _27253, _26896], [xq, sz00, sz00]]))).
% 4.37/4.50 cnf('1.2.3.4.2.1',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.2.3.4.2.2',plain,[aDivisorOf0(xq, sz00)],reduction('1')).
% 4.37/4.50 cnf('1.2.3.4.2.3',plain,[-(aInteger0(xq))],extension(25)).
% 4.37/4.50 cnf('1.2.3.4.2.4',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.2.3.4.2.5',plain,[-(sdtasdt0(xq, sz00) = sz00), aInteger0(xq)],extension(16,bind([[_25479], [xq]]))).
% 4.37/4.50 cnf('1.2.3.4.2.5.1',plain,[-(aInteger0(xq))],extension(25)).
% 4.37/4.50 cnf('1.3',plain,[-(xq = sz00), aInteger0(sz00), aInteger0(xq), sdtasdt0(xq, sz00) = sz00, -(sz00 = sz00)],extension(17,bind([[_26331, _26395], [xq, sz00]]))).
% 4.37/4.50 cnf('1.3.1',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.3.2',plain,[-(aInteger0(xq)), aInteger0(sz00), aDivisorOf0(xq, sz00)],extension(18,bind([[_27010, _26896], [xq, sz00]]))).
% 4.37/4.50 cnf('1.3.2.1',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.3.2.2',plain,[-(aDivisorOf0(xq, sz00))],lemmata('1')).
% 4.37/4.50 cnf('1.3.3',plain,[-(sdtasdt0(xq, sz00) = sz00), aInteger0(xq)],extension(16,bind([[_25479], [xq]]))).
% 4.37/4.50 cnf('1.3.3.1',plain,[-(aInteger0(xq))],extension(25)).
% 4.37/4.50 cnf('1.3.4',plain,[sz00 = sz00, -(sdtpldt0(sdtpldt0(xn, xm), sz00) = sdtpldt0(sz00, sz00)), sdtpldt0(xn, xm) = sz00],extension(4,bind([[_18717, _18782, _18584, _18651], [sz00, sz00, sdtpldt0(xn, xm), sz00]]))).
% 4.37/4.50 cnf('1.3.4.1',plain,[sdtpldt0(sdtpldt0(xn, xm), sz00) = sdtpldt0(sz00, sz00), -(sdtpldt0(sz00, sz00) = sdtpldt0(sdtpldt0(xn, xm), sz00))],extension(6,bind([[_15237, _15192], [sdtpldt0(sz00, sz00), sdtpldt0(sdtpldt0(xn, xm), sz00)]]))).
% 4.37/4.50 cnf('1.3.4.1.1',plain,[sdtpldt0(sz00, sz00) = sdtpldt0(sdtpldt0(xn, xm), sz00), -(sdtpldt0(sz00, sz00) = sdtpldt0(xn, xm)), sdtpldt0(sdtpldt0(xn, xm), sz00) = sdtpldt0(xn, xm)],extension(7,bind([[_15471, _15527, _15582], [sdtpldt0(sz00, sz00), sdtpldt0(sdtpldt0(xn, xm), sz00), sdtpldt0(xn, xm)]]))).
% 4.37/4.50 cnf('1.3.4.1.1.1',plain,[sdtpldt0(sz00, sz00) = sdtpldt0(xn, xm), -(aInteger0(sdtpldt0(xn, xm))), aInteger0(sdtpldt0(sz00, sz00))],extension(9,bind([[_16620, _16571], [sdtpldt0(xn, xm), sdtpldt0(sz00, sz00)]]))).
% 4.37/4.50 cnf('1.3.4.1.1.1.1',plain,[aInteger0(sdtpldt0(xn, xm)), sdtasdt0(xq, sdtpldt0(xn, xm)) = sdtpldt0(xa, smndt0(xc))],extension(1,bind([[_32317], [sdtpldt0(xn, xm)]]))).
% 4.37/4.50 cnf('1.3.4.1.1.1.1.1',plain,[-(sdtasdt0(xq, sdtpldt0(xn, xm)) = sdtpldt0(xa, smndt0(xc)))],extension(30)).
% 4.37/4.50 cnf('1.3.4.1.1.1.2',plain,[-(aInteger0(sdtpldt0(sz00, sz00))), aInteger0(sz00), aInteger0(sz00)],extension(12,bind([[_20274, _20325], [sz00, sz00]]))).
% 4.37/4.50 cnf('1.3.4.1.1.1.2.1',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.3.4.1.1.1.2.2',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.3.4.1.1.2',plain,[-(sdtpldt0(sdtpldt0(xn, xm), sz00) = sdtpldt0(xn, xm)), aInteger0(sdtpldt0(xn, xm))],extension(14,bind([[_22121], [sdtpldt0(xn, xm)]]))).
% 4.37/4.50 cnf('1.3.4.1.1.2.1',plain,[-(aInteger0(sdtpldt0(xn, xm))), aInteger0(xn), aInteger0(xm)],extension(12,bind([[_20274, _20325], [xn, xm]]))).
% 4.37/4.50 cnf('1.3.4.1.1.2.1.1',plain,[-(aInteger0(xn))],extension(28)).
% 4.37/4.50 cnf('1.3.4.1.1.2.1.2',plain,[-(aInteger0(xm))],extension(29)).
% 4.37/4.50 cnf('1.3.4.2',plain,[-(sdtpldt0(xn, xm) = sz00), aInteger0(sz00), -(aDivisorOf0(sdtpldt0(xn, xm), sz00)), aInteger0(sdtpldt0(xn, xm)), aInteger0(sz00), sdtasdt0(sdtpldt0(xn, xm), sz00) = sz00],extension(20,bind([[_27010, _27253, _26896], [sdtpldt0(xn, xm), sz00, sz00]]))).
% 4.37/4.50 cnf('1.3.4.2.1',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.3.4.2.2',plain,[aDivisorOf0(sdtpldt0(xn, xm), sz00), aInteger0(sz00), -(aInteger0(sdtpldt0(xn, xm)))],extension(18,bind([[_26896, _27010], [sz00, sdtpldt0(xn, xm)]]))).
% 4.37/4.50 cnf('1.3.4.2.2.1',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.3.4.2.2.2',plain,[aInteger0(sdtpldt0(xn, xm)), sdtasdt0(xq, sdtpldt0(xn, xm)) = sdtpldt0(xa, smndt0(xc))],extension(1,bind([[_32317], [sdtpldt0(xn, xm)]]))).
% 4.37/4.50 cnf('1.3.4.2.2.2.1',plain,[-(sdtasdt0(xq, sdtpldt0(xn, xm)) = sdtpldt0(xa, smndt0(xc)))],extension(30)).
% 4.37/4.50 cnf('1.3.4.2.3',plain,[-(aInteger0(sdtpldt0(xn, xm))), aInteger0(xn), aInteger0(xm)],extension(12,bind([[_20274, _20325], [xn, xm]]))).
% 4.37/4.50 cnf('1.3.4.2.3.1',plain,[-(aInteger0(xn))],extension(28)).
% 4.37/4.50 cnf('1.3.4.2.3.2',plain,[-(aInteger0(xm))],extension(29)).
% 4.37/4.50 cnf('1.3.4.2.4',plain,[-(aInteger0(sz00))],extension(10)).
% 4.37/4.50 cnf('1.3.4.2.5',plain,[-(sdtasdt0(sdtpldt0(xn, xm), sz00) = sz00), aInteger0(sdtpldt0(xn, xm))],extension(16,bind([[_25479], [sdtpldt0(xn, xm)]]))).
% 4.37/4.50 cnf('1.3.4.2.5.1',plain,[-(aInteger0(sdtpldt0(xn, xm)))],lemmata('1.3.4.2')).
% 4.37/4.50 %-----------------------------------------------------
% 4.37/4.51
% 4.37/4.51 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------