%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUM430+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n004.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:45 EDT 2022
% Result : Theorem 0.73s 1.45s
% Output : Proof 0.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : NUM430+3 : TPTP v8.1.0. Released v4.0.0.
% 0.04/0.15 % Command : leancop_casc.sh %s %d
% 0.15/0.36 % Computer : n004.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 600
% 0.15/0.36 % DateTime : Tue Jul 5 22:20:07 EDT 2022
% 0.15/0.36 % CPUTime :
% 0.73/1.45 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.78/1.46 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.78/1.46
% 0.78/1.46 %-----------------------------------------------------
% 0.78/1.46 fof(m__, conjecture, ? [_54173] : (aInteger0(_54173) & sdtasdt0(xq, _54173) = sdtpldt0(xb, smndt0(xc))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 0.78/1.46 fof(mIntZero, axiom, aInteger0(sz00), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mIntZero)).
% 0.78/1.46 fof(mIntNeg, axiom, ! [_54461] : (aInteger0(_54461) => aInteger0(smndt0(_54461))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mIntNeg)).
% 0.78/1.46 fof(mIntPlus, axiom, ! [_54591, _54594] : (aInteger0(_54591) & aInteger0(_54594) => aInteger0(sdtpldt0(_54591, _54594))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mIntPlus)).
% 0.78/1.46 fof(mAddZero, axiom, ! [_54763] : (aInteger0(_54763) => sdtpldt0(_54763, sz00) = _54763 & _54763 = sdtpldt0(sz00, _54763)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mAddZero)).
% 0.78/1.46 fof(mMulZero, axiom, ! [_54952] : (aInteger0(_54952) => sdtasdt0(_54952, sz00) = sz00 & sz00 = sdtasdt0(sz00, _54952)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mMulZero)).
% 0.78/1.46 fof(mZeroDiv, axiom, ! [_55135, _55138] : (aInteger0(_55135) & aInteger0(_55138) => sdtasdt0(_55135, _55138) = sz00 => _55135 = sz00 | _55138 = sz00), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mZeroDiv)).
% 0.78/1.46 fof(mDivisor, definition, ! [_55355] : (aInteger0(_55355) => ! [_55370] : (aDivisorOf0(_55370, _55355) <=> aInteger0(_55370) & (! _55370) = sz00 & ? [_55403] : (aInteger0(_55403) & sdtasdt0(_55370, _55403) = _55355))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDivisor)).
% 0.78/1.46 fof(m__818, hypothesis, aInteger0(xa) & aInteger0(xb) & aInteger0(xq) & (! xq) = sz00 & aInteger0(xc), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__818)).
% 0.78/1.46 fof(m__853, hypothesis, ? [_55800] : (aInteger0(_55800) & sdtasdt0(xq, _55800) = sdtpldt0(xa, smndt0(xb))) & aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))) & sdteqdtlpzmzozddtrp0(xa, xb, xq) & ? [_55800] : (aInteger0(_55800) & sdtasdt0(xq, _55800) = sdtpldt0(xb, smndt0(xc))) & aDivisorOf0(xq, sdtpldt0(xb, smndt0(xc))) & sdteqdtlpzmzozddtrp0(xb, xc, xq), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__853)).
% 0.78/1.46
% 0.78/1.46 cnf(1, plain, [aInteger0(_31041), sdtasdt0(xq, _31041) = sdtpldt0(xb, smndt0(xc))], clausify(m__)).
% 0.78/1.46 cnf(2, plain, [_18498 = _18547, -(smndt0(_18498) = smndt0(_18547))], theory(equality)).
% 0.78/1.46 cnf(3, plain, [-(sdtpldt0(_17884, _18017) = sdtpldt0(_17951, _18082)), _17884 = _17951, _18017 = _18082], theory(equality)).
% 0.78/1.46 cnf(4, plain, [-(_14339 = _14339)], theory(equality)).
% 0.78/1.46 cnf(5, plain, [-(_14771 = _14882), _14771 = _14827, _14827 = _14882], theory(equality)).
% 0.78/1.46 cnf(6, plain, [-(aDivisorOf0(_15314, _15445)), aDivisorOf0(_15247, _15380), _15247 = _15314, _15380 = _15445], theory(equality)).
% 0.78/1.46 cnf(7, plain, [-(aInteger0(_15920)), _15871 = _15920, aInteger0(_15871)], theory(equality)).
% 0.78/1.46 cnf(8, plain, [-(aInteger0(sz00))], clausify(mIntZero)).
% 0.78/1.46 cnf(9, plain, [aInteger0(_19346), -(aInteger0(smndt0(_19346)))], clausify(mIntNeg)).
% 0.78/1.46 cnf(10, plain, [-(aInteger0(sdtpldt0(_19574, _19625))), aInteger0(_19574), aInteger0(_19625)], clausify(mIntPlus)).
% 0.78/1.47 cnf(11, plain, [aInteger0(_21421), -(sdtpldt0(_21421, sz00) = _21421)], clausify(mAddZero)).
% 0.78/1.47 cnf(12, plain, [aInteger0(_24779), -(sdtasdt0(_24779, sz00) = sz00)], clausify(mMulZero)).
% 0.78/1.47 cnf(13, plain, [aInteger0(_25695), aInteger0(_25631), sdtasdt0(_25631, _25695) = sz00, -(_25631 = sz00), -(_25695 = sz00)], clausify(mZeroDiv)).
% 0.78/1.47 cnf(14, plain, [aInteger0(_26196), aDivisorOf0(_26310, _26196), -(aInteger0(_26310))], clausify(mDivisor)).
% 0.78/1.47 cnf(15, plain, [aInteger0(_26196), aDivisorOf0(_26310, _26196), _26310 = sz00], clausify(mDivisor)).
% 0.78/1.47 cnf(16, plain, [aInteger0(_26196), -(aDivisorOf0(_26310, _26196)), aInteger0(_26310), -(_26310 = sz00), aInteger0(_26553), sdtasdt0(_26310, _26553) = _26196], clausify(mDivisor)).
% 0.78/1.47 cnf(17, plain, [-(aInteger0(xa))], clausify(m__818)).
% 0.78/1.47 cnf(18, plain, [-(aInteger0(xb))], clausify(m__818)).
% 0.78/1.47 cnf(19, plain, [-(aInteger0(xq))], clausify(m__818)).
% 0.78/1.47 cnf(20, plain, [xq = sz00], clausify(m__818)).
% 0.78/1.47 cnf(21, plain, [-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))))], clausify(m__853)).
% 0.78/1.47 cnf(22, plain, [-(aInteger0(3 ^ []))], clausify(m__853)).
% 0.78/1.47 cnf(23, plain, [-(sdtasdt0(xq, 3 ^ []) = sdtpldt0(xb, smndt0(xc)))], clausify(m__853)).
% 0.78/1.47
% 0.78/1.47 cnf('1',plain,[aInteger0(sz00), aDivisorOf0(xq, sz00), xq = sz00],start(15,bind([[_26196, _26310], [sz00, xq]]))).
% 0.78/1.47 cnf('1.1',plain,[-(aInteger0(sz00))],extension(8)).
% 0.78/1.47 cnf('1.2',plain,[-(aDivisorOf0(xq, sz00)), aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))), xq = xq, sdtpldt0(xa, smndt0(xb)) = sz00],extension(6,bind([[_15247, _15314, _15380, _15445], [xq, xq, sdtpldt0(xa, smndt0(xb)), sz00]]))).
% 0.78/1.47 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(6,bind([[_15247, _15314, _15380, _15445], [xq, xq, sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb))]]))).
% 0.78/1.47 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(6,bind([[_15247, _15314, _15380, _15445], [xq, xq, sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb))]]))).
% 0.78/1.47 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(6,bind([[_15247, _15314, _15380, _15445], [xq, xq, sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb))]]))).
% 0.78/1.47 cnf('1.2.1.1.1.1',plain,[-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))))],extension(21)).
% 0.78/1.47 cnf('1.2.1.1.1.2',plain,[-(xq = xq)],extension(4,bind([[_14339], [xq]]))).
% 0.78/1.47 cnf('1.2.1.1.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb)))],extension(4,bind([[_14339], [sdtpldt0(xa, smndt0(xb))]]))).
% 0.78/1.47 cnf('1.2.1.1.2',plain,[-(xq = xq)],extension(4,bind([[_14339], [xq]]))).
% 0.78/1.47 cnf('1.2.1.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))), xa = xa, smndt0(xb) = smndt0(xb)],extension(3,bind([[_17884, _17951, _18017, _18082], [xa, xa, smndt0(xb), smndt0(xb)]]))).
% 0.78/1.47 cnf('1.2.1.1.3.1',plain,[-(xa = xa)],extension(4,bind([[_14339], [xa]]))).
% 0.78/1.47 cnf('1.2.1.1.3.2',plain,[-(smndt0(xb) = smndt0(xb))],extension(4,bind([[_14339], [smndt0(xb)]]))).
% 0.78/1.47 cnf('1.2.1.2',plain,[-(xq = xq)],extension(4,bind([[_14339], [xq]]))).
% 0.78/1.47 cnf('1.2.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))), xa = xa, smndt0(xb) = smndt0(xb)],extension(3,bind([[_17884, _17951, _18017, _18082], [xa, xa, smndt0(xb), smndt0(xb)]]))).
% 0.78/1.47 cnf('1.2.1.3.1',plain,[-(xa = xa)],extension(4,bind([[_14339], [xa]]))).
% 0.78/1.47 cnf('1.2.1.3.2',plain,[-(smndt0(xb) = smndt0(xb)), xb = xb],extension(2,bind([[_18498, _18547], [xb, xb]]))).
% 0.78/1.47 cnf('1.2.1.3.2.1',plain,[-(xb = xb)],extension(4,bind([[_14339], [xb]]))).
% 0.78/1.47 cnf('1.2.2',plain,[-(xq = xq)],extension(4,bind([[_14339], [xq]]))).
% 0.78/1.47 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(13,bind([[_25631, _25695], [sdtpldt0(xa, smndt0(xb)), sz00]]))).
% 0.78/1.47 cnf('1.2.3.1',plain,[-(aInteger0(sz00))],extension(8)).
% 0.78/1.47 cnf('1.2.3.2',plain,[-(aInteger0(sdtpldt0(xa, smndt0(xb)))), aInteger0(xa), aInteger0(smndt0(xb))],extension(10,bind([[_19574, _19625], [xa, smndt0(xb)]]))).
% 0.78/1.47 cnf('1.2.3.2.1',plain,[-(aInteger0(xa))],extension(17)).
% 0.78/1.47 cnf('1.2.3.2.2',plain,[-(aInteger0(smndt0(xb))), aInteger0(xb)],extension(9,bind([[_19346], [xb]]))).
% 0.78/1.47 cnf('1.2.3.2.2.1',plain,[-(aInteger0(xb))],extension(18)).
% 0.78/1.47 cnf('1.2.3.3',plain,[-(sdtasdt0(sdtpldt0(xa, smndt0(xb)), sz00) = sz00), aInteger0(sdtpldt0(xa, smndt0(xb)))],extension(12,bind([[_24779], [sdtpldt0(xa, smndt0(xb))]]))).
% 0.78/1.47 cnf('1.2.3.3.1',plain,[-(aInteger0(sdtpldt0(xa, smndt0(xb))))],lemmata('1.2.3')).
% 0.78/1.47 cnf('1.2.3.4',plain,[sz00 = sz00, -(aInteger0(sz00)), aInteger0(sz00)],extension(7,bind([[_15920, _15871], [sz00, sz00]]))).
% 0.78/1.47 cnf('1.2.3.4.1',plain,[aInteger0(sz00), -(aDivisorOf0(xq, sz00)), aInteger0(xq), -(xq = sz00), aInteger0(sz00), sdtasdt0(xq, sz00) = sz00],extension(16,bind([[_26310, _26553, _26196], [xq, sz00, sz00]]))).
% 0.78/1.47 cnf('1.2.3.4.1.1',plain,[aDivisorOf0(xq, sz00)],reduction('1')).
% 0.78/1.47 cnf('1.2.3.4.1.2',plain,[-(aInteger0(xq))],extension(19)).
% 0.78/1.47 cnf('1.2.3.4.1.3',plain,[xq = sz00, -(xq = sz00), sz00 = sz00],extension(5,bind([[_14771, _14827, _14882], [xq, sz00, sz00]]))).
% 0.78/1.47 cnf('1.2.3.4.1.3.1',plain,[xq = sz00],extension(20)).
% 0.78/1.47 cnf('1.2.3.4.1.3.2',plain,[-(sz00 = sz00)],extension(4,bind([[_14339], [sz00]]))).
% 0.78/1.47 cnf('1.2.3.4.1.4',plain,[-(aInteger0(sz00))],extension(8)).
% 0.78/1.47 cnf('1.2.3.4.1.5',plain,[-(sdtasdt0(xq, sz00) = sz00), aInteger0(xq)],extension(12,bind([[_24779], [xq]]))).
% 0.78/1.47 cnf('1.2.3.4.1.5.1',plain,[-(aInteger0(xq))],extension(19)).
% 0.78/1.47 cnf('1.2.3.4.2',plain,[-(aInteger0(sz00))],extension(8)).
% 0.78/1.47 cnf('1.3',plain,[-(xq = sz00), aInteger0(sz00), aInteger0(xq), sdtasdt0(xq, sz00) = sz00, -(sz00 = sz00)],extension(13,bind([[_25631, _25695], [xq, sz00]]))).
% 0.78/1.47 cnf('1.3.1',plain,[-(aInteger0(sz00))],extension(8)).
% 0.78/1.47 cnf('1.3.2',plain,[-(aInteger0(xq)), aInteger0(sz00), aDivisorOf0(xq, sz00)],extension(14,bind([[_26310, _26196], [xq, sz00]]))).
% 0.78/1.47 cnf('1.3.2.1',plain,[-(aInteger0(sz00))],extension(8)).
% 0.78/1.47 cnf('1.3.2.2',plain,[-(aDivisorOf0(xq, sz00))],lemmata('1')).
% 0.78/1.47 cnf('1.3.3',plain,[-(sdtasdt0(xq, sz00) = sz00), aInteger0(xq)],extension(12,bind([[_24779], [xq]]))).
% 0.78/1.47 cnf('1.3.3.1',plain,[-(aInteger0(xq))],extension(19)).
% 0.78/1.47 cnf('1.3.4',plain,[sz00 = sz00, -(aInteger0(sz00)), aInteger0(sz00)],extension(7,bind([[_15920, _15871], [sz00, sz00]]))).
% 0.78/1.47 cnf('1.3.4.1',plain,[aInteger0(sz00), -(aInteger0(sdtpldt0(3 ^ [], sz00))), aInteger0(3 ^ [])],extension(10,bind([[_19625, _19574], [sz00, 3 ^ []]]))).
% 0.78/1.47 cnf('1.3.4.1.1',plain,[aInteger0(sdtpldt0(3 ^ [], sz00)), -(aInteger0(3 ^ [])), sdtpldt0(3 ^ [], sz00) = 3 ^ []],extension(7,bind([[_15871, _15920], [sdtpldt0(3 ^ [], sz00), 3 ^ []]]))).
% 0.78/1.47 cnf('1.3.4.1.1.1',plain,[aInteger0(3 ^ []), sdtasdt0(xq, 3 ^ []) = sdtpldt0(xb, smndt0(xc))],extension(1,bind([[_31041], [3 ^ []]]))).
% 0.78/1.47 cnf('1.3.4.1.1.1.1',plain,[-(sdtasdt0(xq, 3 ^ []) = sdtpldt0(xb, smndt0(xc)))],extension(23)).
% 0.78/1.47 cnf('1.3.4.1.1.2',plain,[-(sdtpldt0(3 ^ [], sz00) = 3 ^ []), aInteger0(3 ^ [])],extension(11,bind([[_21421], [3 ^ []]]))).
% 0.78/1.47 cnf('1.3.4.1.1.2.1',plain,[-(aInteger0(3 ^ []))],extension(22)).
% 0.78/1.47 cnf('1.3.4.1.2',plain,[-(aInteger0(3 ^ []))],extension(22)).
% 0.78/1.47 cnf('1.3.4.2',plain,[-(aInteger0(sz00))],extension(8)).
% 0.78/1.47 %-----------------------------------------------------
% 0.78/1.47
% 0.78/1.47 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------