%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUM434+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n025.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:47 EDT 2022
% Result : Theorem 0.89s 1.40s
% Output : Proof 0.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM434+3 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n025.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 20:52:27 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.89/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.89/1.41 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.89/1.41
% 0.89/1.41 %-----------------------------------------------------
% 0.89/1.41 fof(m__, conjecture, ? [_58235] : (aInteger0(_58235) & sdtasdt0(sdtasdt0(xp, xq), _58235) = sdtpldt0(xa, smndt0(xb))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 0.89/1.41 fof(mIntZero, axiom, aInteger0(sz00), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mIntZero)).
% 0.89/1.41 fof(mIntNeg, axiom, ! [_58550] : (aInteger0(_58550) => aInteger0(smndt0(_58550))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mIntNeg)).
% 0.89/1.41 fof(mIntPlus, axiom, ! [_58680, _58683] : (aInteger0(_58680) & aInteger0(_58683) => aInteger0(sdtpldt0(_58680, _58683))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mIntPlus)).
% 0.89/1.41 fof(mIntMult, axiom, ! [_58849, _58852] : (aInteger0(_58849) & aInteger0(_58852) => aInteger0(sdtasdt0(_58849, _58852))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mIntMult)).
% 0.89/1.41 fof(mAddZero, axiom, ! [_59020] : (aInteger0(_59020) => sdtpldt0(_59020, sz00) = _59020 & _59020 = sdtpldt0(sz00, _59020)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mAddZero)).
% 0.89/1.41 fof(mMulZero, axiom, ! [_59209] : (aInteger0(_59209) => sdtasdt0(_59209, sz00) = sz00 & sz00 = sdtasdt0(sz00, _59209)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mMulZero)).
% 0.89/1.41 fof(mZeroDiv, axiom, ! [_59392, _59395] : (aInteger0(_59392) & aInteger0(_59395) => sdtasdt0(_59392, _59395) = sz00 => _59392 = sz00 | _59395 = sz00), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mZeroDiv)).
% 0.89/1.41 fof(mDivisor, definition, ! [_59613] : (aInteger0(_59613) => ! [_59628] : (aDivisorOf0(_59628, _59613) <=> aInteger0(_59628) & (! _59628) = sz00 & ? [_59661] : (aInteger0(_59661) & sdtasdt0(_59628, _59661) = _59613))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDivisor)).
% 0.89/1.41 fof(m__979, hypothesis, aInteger0(xa) & aInteger0(xb) & aInteger0(xp) & (! xp) = sz00 & aInteger0(xq) & (! xq) = sz00, file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__979)).
% 0.89/1.41 fof(m__1003, hypothesis, (! sdtasdt0(xp, xq)) = sz00 & ? [_60069] : (aInteger0(_60069) & sdtasdt0(sdtasdt0(xp, xq), _60069) = sdtpldt0(xa, smndt0(xb))) & aDivisorOf0(sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb))) & sdteqdtlpzmzozddtrp0(xa, xb, sdtasdt0(xp, xq)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__1003)).
% 0.89/1.41
% 0.89/1.41 cnf(1, plain, [aInteger0(_32063), sdtasdt0(sdtasdt0(xp, xq), _32063) = sdtpldt0(xa, smndt0(xb))], clausify(m__)).
% 0.89/1.41 cnf(2, plain, [-(sdtasdt0(_17645, _17778) = sdtasdt0(_17712, _17843)), _17645 = _17712, _17778 = _17843], theory(equality)).
% 0.89/1.41 cnf(3, plain, [_18883 = _18932, -(smndt0(_18883) = smndt0(_18932))], theory(equality)).
% 0.89/1.41 cnf(4, plain, [-(sdtpldt0(_18269, _18402) = sdtpldt0(_18336, _18467)), _18269 = _18336, _18402 = _18467], theory(equality)).
% 0.89/1.41 cnf(5, plain, [-(_14724 = _14724)], theory(equality)).
% 0.89/1.41 cnf(6, plain, [-(_15156 = _15267), _15156 = _15212, _15212 = _15267], theory(equality)).
% 0.89/1.41 cnf(7, plain, [-(aDivisorOf0(_15699, _15830)), aDivisorOf0(_15632, _15765), _15632 = _15699, _15765 = _15830], theory(equality)).
% 0.89/1.41 cnf(8, plain, [-(aInteger0(_16305)), _16256 = _16305, aInteger0(_16256)], theory(equality)).
% 0.89/1.41 cnf(9, plain, [-(aInteger0(sz00))], clausify(mIntZero)).
% 0.89/1.41 cnf(10, plain, [aInteger0(_19731), -(aInteger0(smndt0(_19731)))], clausify(mIntNeg)).
% 0.89/1.41 cnf(11, plain, [-(aInteger0(sdtpldt0(_19959, _20010))), aInteger0(_19959), aInteger0(_20010)], clausify(mIntPlus)).
% 0.89/1.41 cnf(12, plain, [-(aInteger0(sdtasdt0(_20329, _20380))), aInteger0(_20329), aInteger0(_20380)], clausify(mIntMult)).
% 0.89/1.41 cnf(13, plain, [aInteger0(_21806), -(sdtpldt0(_21806, sz00) = _21806)], clausify(mAddZero)).
% 0.89/1.41 cnf(14, plain, [aInteger0(_25164), -(sdtasdt0(_25164, sz00) = sz00)], clausify(mMulZero)).
% 0.89/1.41 cnf(15, plain, [aInteger0(_26080), aInteger0(_26016), sdtasdt0(_26016, _26080) = sz00, -(_26016 = sz00), -(_26080 = sz00)], clausify(mZeroDiv)).
% 0.89/1.41 cnf(16, plain, [aInteger0(_26581), aDivisorOf0(_26695, _26581), _26695 = sz00], clausify(mDivisor)).
% 0.89/1.41 cnf(17, plain, [aInteger0(_26581), -(aDivisorOf0(_26695, _26581)), aInteger0(_26695), -(_26695 = sz00), aInteger0(_26938), sdtasdt0(_26695, _26938) = _26581], clausify(mDivisor)).
% 0.89/1.41 cnf(18, plain, [-(aInteger0(xa))], clausify(m__979)).
% 0.89/1.41 cnf(19, plain, [-(aInteger0(xb))], clausify(m__979)).
% 0.89/1.41 cnf(20, plain, [-(aInteger0(xp))], clausify(m__979)).
% 0.89/1.41 cnf(21, plain, [-(aInteger0(xq))], clausify(m__979)).
% 0.89/1.41 cnf(22, plain, [sdtasdt0(xp, xq) = sz00], clausify(m__1003)).
% 0.89/1.41 cnf(23, plain, [-(aInteger0(2 ^ []))], clausify(m__1003)).
% 0.89/1.41 cnf(24, plain, [-(sdtasdt0(sdtasdt0(xp, xq), 2 ^ []) = sdtpldt0(xa, smndt0(xb)))], clausify(m__1003)).
% 0.89/1.41 cnf(25, plain, [-(aDivisorOf0(sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb))))], clausify(m__1003)).
% 0.89/1.41
% 0.89/1.41 cnf('1',plain,[aInteger0(sz00), aDivisorOf0(sdtasdt0(xp, xq), sz00), sdtasdt0(xp, xq) = sz00],start(16,bind([[_26581, _26695], [sz00, sdtasdt0(xp, xq)]]))).
% 0.89/1.41 cnf('1.1',plain,[-(aInteger0(sz00))],extension(9)).
% 0.89/1.41 cnf('1.2',plain,[-(aDivisorOf0(sdtasdt0(xp, xq), sz00)), aDivisorOf0(sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb))), sdtasdt0(xp, xq) = sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb)) = sz00],extension(7,bind([[_15632, _15699, _15765, _15830], [sdtasdt0(xp, xq), sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb)), sz00]]))).
% 0.89/1.41 cnf('1.2.1',plain,[-(aDivisorOf0(sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb)))), aDivisorOf0(sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb))), sdtasdt0(xp, xq) = sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))],extension(7,bind([[_15632, _15699, _15765, _15830], [sdtasdt0(xp, xq), sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb))]]))).
% 0.89/1.41 cnf('1.2.1.1',plain,[-(aDivisorOf0(sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb)))), aDivisorOf0(sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb))), sdtasdt0(xp, xq) = sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))],extension(7,bind([[_15632, _15699, _15765, _15830], [sdtasdt0(xp, xq), sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb))]]))).
% 0.89/1.41 cnf('1.2.1.1.1',plain,[-(aDivisorOf0(sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb)))), aDivisorOf0(sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb))), sdtasdt0(xp, xq) = sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))],extension(7,bind([[_15632, _15699, _15765, _15830], [sdtasdt0(xp, xq), sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb))]]))).
% 0.89/1.41 cnf('1.2.1.1.1.1',plain,[-(aDivisorOf0(sdtasdt0(xp, xq), sdtpldt0(xa, smndt0(xb))))],extension(25)).
% 0.89/1.41 cnf('1.2.1.1.1.2',plain,[-(sdtasdt0(xp, xq) = sdtasdt0(xp, xq))],extension(5,bind([[_14724], [sdtasdt0(xp, xq)]]))).
% 0.89/1.41 cnf('1.2.1.1.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb)))],extension(5,bind([[_14724], [sdtpldt0(xa, smndt0(xb))]]))).
% 0.89/1.41 cnf('1.2.1.1.2',plain,[-(sdtasdt0(xp, xq) = sdtasdt0(xp, xq)), xp = xp, xq = xq],extension(2,bind([[_17645, _17712, _17778, _17843], [xp, xp, xq, xq]]))).
% 0.89/1.41 cnf('1.2.1.1.2.1',plain,[-(xp = xp)],extension(5,bind([[_14724], [xp]]))).
% 0.89/1.41 cnf('1.2.1.1.2.2',plain,[-(xq = xq)],extension(5,bind([[_14724], [xq]]))).
% 0.89/1.41 cnf('1.2.1.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))), xa = xa, smndt0(xb) = smndt0(xb)],extension(4,bind([[_18269, _18336, _18402, _18467], [xa, xa, smndt0(xb), smndt0(xb)]]))).
% 0.89/1.41 cnf('1.2.1.1.3.1',plain,[-(xa = xa)],extension(5,bind([[_14724], [xa]]))).
% 0.89/1.41 cnf('1.2.1.1.3.2',plain,[-(smndt0(xb) = smndt0(xb))],extension(5,bind([[_14724], [smndt0(xb)]]))).
% 0.89/1.41 cnf('1.2.1.2',plain,[-(sdtasdt0(xp, xq) = sdtasdt0(xp, xq)), xp = xp, xq = xq],extension(2,bind([[_17645, _17712, _17778, _17843], [xp, xp, xq, xq]]))).
% 0.89/1.41 cnf('1.2.1.2.1',plain,[-(xp = xp)],extension(5,bind([[_14724], [xp]]))).
% 0.89/1.41 cnf('1.2.1.2.2',plain,[-(xq = xq)],extension(5,bind([[_14724], [xq]]))).
% 0.89/1.41 cnf('1.2.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))), xa = xa, smndt0(xb) = smndt0(xb)],extension(4,bind([[_18269, _18336, _18402, _18467], [xa, xa, smndt0(xb), smndt0(xb)]]))).
% 0.89/1.41 cnf('1.2.1.3.1',plain,[-(xa = xa)],extension(5,bind([[_14724], [xa]]))).
% 0.89/1.41 cnf('1.2.1.3.2',plain,[-(smndt0(xb) = smndt0(xb)), xb = xb],extension(3,bind([[_18883, _18932], [xb, xb]]))).
% 0.89/1.41 cnf('1.2.1.3.2.1',plain,[-(xb = xb)],extension(5,bind([[_14724], [xb]]))).
% 0.89/1.41 cnf('1.2.2',plain,[-(sdtasdt0(xp, xq) = sdtasdt0(xp, xq)), xp = xp, xq = xq],extension(2,bind([[_17645, _17712, _17778, _17843], [xp, xp, xq, xq]]))).
% 0.89/1.41 cnf('1.2.2.1',plain,[-(xp = xp)],extension(5,bind([[_14724], [xp]]))).
% 0.89/1.41 cnf('1.2.2.2',plain,[-(xq = xq)],extension(5,bind([[_14724], [xq]]))).
% 0.89/1.41 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(15,bind([[_26016, _26080], [sdtpldt0(xa, smndt0(xb)), sz00]]))).
% 0.89/1.41 cnf('1.2.3.1',plain,[-(aInteger0(sz00))],extension(9)).
% 0.89/1.41 cnf('1.2.3.2',plain,[-(aInteger0(sdtpldt0(xa, smndt0(xb)))), aInteger0(xa), aInteger0(smndt0(xb))],extension(11,bind([[_19959, _20010], [xa, smndt0(xb)]]))).
% 0.89/1.41 cnf('1.2.3.2.1',plain,[-(aInteger0(xa))],extension(18)).
% 0.89/1.41 cnf('1.2.3.2.2',plain,[-(aInteger0(smndt0(xb))), aInteger0(xb)],extension(10,bind([[_19731], [xb]]))).
% 0.89/1.41 cnf('1.2.3.2.2.1',plain,[-(aInteger0(xb))],extension(19)).
% 0.89/1.41 cnf('1.2.3.3',plain,[-(sdtasdt0(sdtpldt0(xa, smndt0(xb)), sz00) = sz00), aInteger0(sdtpldt0(xa, smndt0(xb)))],extension(14,bind([[_25164], [sdtpldt0(xa, smndt0(xb))]]))).
% 0.89/1.41 cnf('1.2.3.3.1',plain,[-(aInteger0(sdtpldt0(xa, smndt0(xb))))],lemmata('1.2.3')).
% 0.89/1.41 cnf('1.2.3.4',plain,[sz00 = sz00, -(aInteger0(sz00)), aInteger0(sz00)],extension(8,bind([[_16305, _16256], [sz00, sz00]]))).
% 0.89/1.41 cnf('1.2.3.4.1',plain,[aInteger0(sz00), -(aDivisorOf0(sdtasdt0(xp, xq), sz00)), aInteger0(sdtasdt0(xp, xq)), -(sdtasdt0(xp, xq) = sz00), aInteger0(sz00), sdtasdt0(sdtasdt0(xp, xq), sz00) = sz00],extension(17,bind([[_26695, _26938, _26581], [sdtasdt0(xp, xq), sz00, sz00]]))).
% 0.89/1.41 cnf('1.2.3.4.1.1',plain,[aDivisorOf0(sdtasdt0(xp, xq), sz00)],reduction('1')).
% 0.89/1.41 cnf('1.2.3.4.1.2',plain,[-(aInteger0(sdtasdt0(xp, xq))), aInteger0(xp), aInteger0(xq)],extension(12,bind([[_20329, _20380], [xp, xq]]))).
% 0.89/1.41 cnf('1.2.3.4.1.2.1',plain,[-(aInteger0(xp))],extension(20)).
% 0.89/1.41 cnf('1.2.3.4.1.2.2',plain,[-(aInteger0(xq))],extension(21)).
% 0.89/1.41 cnf('1.2.3.4.1.3',plain,[sdtasdt0(xp, xq) = sz00, -(sdtasdt0(xp, xq) = sz00), sz00 = sz00],extension(6,bind([[_15156, _15212, _15267], [sdtasdt0(xp, xq), sz00, sz00]]))).
% 0.89/1.41 cnf('1.2.3.4.1.3.1',plain,[sdtasdt0(xp, xq) = sz00],extension(22)).
% 0.89/1.41 cnf('1.2.3.4.1.3.2',plain,[-(sz00 = sz00)],extension(5,bind([[_14724], [sz00]]))).
% 0.89/1.41 cnf('1.2.3.4.1.4',plain,[-(aInteger0(sz00))],extension(9)).
% 0.89/1.41 cnf('1.2.3.4.1.5',plain,[-(sdtasdt0(sdtasdt0(xp, xq), sz00) = sz00), aInteger0(sdtasdt0(xp, xq))],extension(14,bind([[_25164], [sdtasdt0(xp, xq)]]))).
% 0.89/1.41 cnf('1.2.3.4.1.5.1',plain,[-(aInteger0(sdtasdt0(xp, xq)))],lemmata('1.2.3.4.1')).
% 0.89/1.41 cnf('1.2.3.4.2',plain,[-(aInteger0(sz00))],extension(9)).
% 0.89/1.41 cnf('1.3',plain,[-(sdtasdt0(xp, xq) = sz00), aInteger0(sz00), aInteger0(sdtasdt0(xp, xq)), sdtasdt0(sdtasdt0(xp, xq), sz00) = sz00, -(sz00 = sz00)],extension(15,bind([[_26016, _26080], [sdtasdt0(xp, xq), sz00]]))).
% 0.89/1.41 cnf('1.3.1',plain,[-(aInteger0(sz00))],extension(9)).
% 0.89/1.41 cnf('1.3.2',plain,[-(aInteger0(sdtasdt0(xp, xq))), aInteger0(xp), aInteger0(xq)],extension(12,bind([[_20329, _20380], [xp, xq]]))).
% 0.89/1.41 cnf('1.3.2.1',plain,[-(aInteger0(xp))],extension(20)).
% 0.89/1.41 cnf('1.3.2.2',plain,[-(aInteger0(xq))],extension(21)).
% 0.89/1.41 cnf('1.3.3',plain,[-(sdtasdt0(sdtasdt0(xp, xq), sz00) = sz00), aInteger0(sdtasdt0(xp, xq))],extension(14,bind([[_25164], [sdtasdt0(xp, xq)]]))).
% 0.89/1.41 cnf('1.3.3.1',plain,[-(aInteger0(sdtasdt0(xp, xq)))],lemmata('1.3')).
% 0.89/1.41 cnf('1.3.4',plain,[sz00 = sz00, -(aInteger0(sz00)), aInteger0(sz00)],extension(8,bind([[_16305, _16256], [sz00, sz00]]))).
% 0.89/1.41 cnf('1.3.4.1',plain,[aInteger0(sz00), -(aInteger0(sdtpldt0(2 ^ [], sz00))), aInteger0(2 ^ [])],extension(11,bind([[_20010, _19959], [sz00, 2 ^ []]]))).
% 0.89/1.41 cnf('1.3.4.1.1',plain,[aInteger0(sdtpldt0(2 ^ [], sz00)), -(aInteger0(2 ^ [])), sdtpldt0(2 ^ [], sz00) = 2 ^ []],extension(8,bind([[_16256, _16305], [sdtpldt0(2 ^ [], sz00), 2 ^ []]]))).
% 0.89/1.41 cnf('1.3.4.1.1.1',plain,[aInteger0(2 ^ []), sdtasdt0(sdtasdt0(xp, xq), 2 ^ []) = sdtpldt0(xa, smndt0(xb))],extension(1,bind([[_32063], [2 ^ []]]))).
% 0.89/1.41 cnf('1.3.4.1.1.1.1',plain,[-(sdtasdt0(sdtasdt0(xp, xq), 2 ^ []) = sdtpldt0(xa, smndt0(xb)))],extension(24)).
% 0.89/1.41 cnf('1.3.4.1.1.2',plain,[-(sdtpldt0(2 ^ [], sz00) = 2 ^ []), aInteger0(2 ^ [])],extension(13,bind([[_21806], [2 ^ []]]))).
% 0.89/1.41 cnf('1.3.4.1.1.2.1',plain,[-(aInteger0(2 ^ []))],extension(23)).
% 0.89/1.41 cnf('1.3.4.1.2',plain,[-(aInteger0(2 ^ []))],extension(23)).
% 0.89/1.41 cnf('1.3.4.2',plain,[-(aInteger0(sz00))],extension(9)).
% 0.89/1.41 %-----------------------------------------------------
% 0.89/1.42
% 0.89/1.42 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------