%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUM425+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n027.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:42 EDT 2022
% Result : Theorem 0.64s 1.40s
% Output : Proof 0.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM425+3 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n027.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 : Thu Jul 7 09:13:14 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.64/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.64/1.41 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.64/1.41
% 0.64/1.41 %-----------------------------------------------------
% 0.64/1.41 fof(m__, conjecture, ? [_50135] : (aInteger0(_50135) & sdtasdt0(xq, _50135) = sdtpldt0(xa, smndt0(xb))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 0.64/1.41 fof(mIntZero, axiom, aInteger0(sz00), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mIntZero)).
% 0.64/1.41 fof(mIntNeg, axiom, ! [_50423] : (aInteger0(_50423) => aInteger0(smndt0(_50423))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mIntNeg)).
% 0.64/1.41 fof(mIntPlus, axiom, ! [_50553, _50556] : (aInteger0(_50553) & aInteger0(_50556) => aInteger0(sdtpldt0(_50553, _50556))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mIntPlus)).
% 0.64/1.41 fof(mAddZero, axiom, ! [_50725] : (aInteger0(_50725) => sdtpldt0(_50725, sz00) = _50725 & _50725 = sdtpldt0(sz00, _50725)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mAddZero)).
% 0.64/1.41 fof(mMulZero, axiom, ! [_50914] : (aInteger0(_50914) => sdtasdt0(_50914, sz00) = sz00 & sz00 = sdtasdt0(sz00, _50914)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mMulZero)).
% 0.64/1.41 fof(mZeroDiv, axiom, ! [_51097, _51100] : (aInteger0(_51097) & aInteger0(_51100) => sdtasdt0(_51097, _51100) = sz00 => _51097 = sz00 | _51100 = sz00), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mZeroDiv)).
% 0.64/1.41 fof(mDivisor, definition, ! [_51317] : (aInteger0(_51317) => ! [_51332] : (aDivisorOf0(_51332, _51317) <=> aInteger0(_51332) & (! _51332) = sz00 & ? [_51365] : (aInteger0(_51365) & sdtasdt0(_51332, _51365) = _51317))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDivisor)).
% 0.64/1.41 fof(m__704, hypothesis, aInteger0(xa) & aInteger0(xb) & aInteger0(xq) & (! xq) = sz00, file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__704)).
% 0.64/1.41 fof(m__724, hypothesis, ? [_51749] : (aInteger0(_51749) & sdtasdt0(xq, _51749) = sdtpldt0(xa, smndt0(xb))) & aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))) & sdteqdtlpzmzozddtrp0(xa, xb, xq), file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__724)).
% 0.64/1.41
% 0.64/1.41 cnf(1, plain, [aInteger0(_27895), sdtasdt0(xq, _27895) = sdtpldt0(xa, smndt0(xb))], clausify(m__)).
% 0.64/1.41 cnf(2, plain, [_16998 = _17047, -(smndt0(_16998) = smndt0(_17047))], theory(equality)).
% 0.64/1.41 cnf(3, plain, [-(sdtpldt0(_16384, _16517) = sdtpldt0(_16451, _16582)), _16384 = _16451, _16517 = _16582], theory(equality)).
% 0.64/1.41 cnf(4, plain, [-(_12839 = _12839)], theory(equality)).
% 0.64/1.41 cnf(5, plain, [-(_13271 = _13382), _13271 = _13327, _13327 = _13382], theory(equality)).
% 0.64/1.41 cnf(6, plain, [-(aDivisorOf0(_13814, _13945)), aDivisorOf0(_13747, _13880), _13747 = _13814, _13880 = _13945], theory(equality)).
% 0.64/1.41 cnf(7, plain, [-(aInteger0(_14420)), _14371 = _14420, aInteger0(_14371)], theory(equality)).
% 0.64/1.41 cnf(8, plain, [-(aInteger0(sz00))], clausify(mIntZero)).
% 0.64/1.41 cnf(9, plain, [aInteger0(_17846), -(aInteger0(smndt0(_17846)))], clausify(mIntNeg)).
% 0.64/1.41 cnf(10, plain, [-(aInteger0(sdtpldt0(_18074, _18125))), aInteger0(_18074), aInteger0(_18125)], clausify(mIntPlus)).
% 0.64/1.41 cnf(11, plain, [aInteger0(_19921), -(sdtpldt0(_19921, sz00) = _19921)], clausify(mAddZero)).
% 0.64/1.41 cnf(12, plain, [aInteger0(_23279), -(sdtasdt0(_23279, sz00) = sz00)], clausify(mMulZero)).
% 0.64/1.41 cnf(13, plain, [aInteger0(_24195), aInteger0(_24131), sdtasdt0(_24131, _24195) = sz00, -(_24131 = sz00), -(_24195 = sz00)], clausify(mZeroDiv)).
% 0.64/1.41 cnf(14, plain, [aInteger0(_24696), aDivisorOf0(_24810, _24696), -(aInteger0(_24810))], clausify(mDivisor)).
% 0.64/1.41 cnf(15, plain, [aInteger0(_24696), aDivisorOf0(_24810, _24696), _24810 = sz00], clausify(mDivisor)).
% 0.64/1.41 cnf(16, plain, [aInteger0(_24696), -(aDivisorOf0(_24810, _24696)), aInteger0(_24810), -(_24810 = sz00), aInteger0(_25053), sdtasdt0(_24810, _25053) = _24696], clausify(mDivisor)).
% 0.64/1.41 cnf(17, plain, [-(aInteger0(xa))], clausify(m__704)).
% 0.64/1.41 cnf(18, plain, [-(aInteger0(xb))], clausify(m__704)).
% 0.64/1.41 cnf(19, plain, [-(aInteger0(xq))], clausify(m__704)).
% 0.64/1.41 cnf(20, plain, [xq = sz00], clausify(m__704)).
% 0.64/1.41 cnf(21, plain, [-(aInteger0(2 ^ []))], clausify(m__724)).
% 0.64/1.41 cnf(22, plain, [-(sdtasdt0(xq, 2 ^ []) = sdtpldt0(xa, smndt0(xb)))], clausify(m__724)).
% 0.64/1.41 cnf(23, plain, [-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))))], clausify(m__724)).
% 0.64/1.41
% 0.64/1.41 cnf('1',plain,[aInteger0(sz00), aDivisorOf0(xq, sz00), xq = sz00],start(15,bind([[_24696, _24810], [sz00, xq]]))).
% 0.64/1.41 cnf('1.1',plain,[-(aInteger0(sz00))],extension(8)).
% 0.64/1.41 cnf('1.2',plain,[-(aDivisorOf0(xq, sz00)), aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))), xq = xq, sdtpldt0(xa, smndt0(xb)) = sz00],extension(6,bind([[_13747, _13814, _13880, _13945], [xq, xq, sdtpldt0(xa, smndt0(xb)), sz00]]))).
% 0.64/1.41 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([[_13747, _13814, _13880, _13945], [xq, xq, sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb))]]))).
% 0.64/1.41 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([[_13747, _13814, _13880, _13945], [xq, xq, sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb))]]))).
% 0.64/1.41 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([[_13747, _13814, _13880, _13945], [xq, xq, sdtpldt0(xa, smndt0(xb)), sdtpldt0(xa, smndt0(xb))]]))).
% 0.64/1.41 cnf('1.2.1.1.1.1',plain,[-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))))],extension(23)).
% 0.64/1.41 cnf('1.2.1.1.1.2',plain,[-(xq = xq)],extension(4,bind([[_12839], [xq]]))).
% 0.64/1.41 cnf('1.2.1.1.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb)))],extension(4,bind([[_12839], [sdtpldt0(xa, smndt0(xb))]]))).
% 0.64/1.41 cnf('1.2.1.1.2',plain,[-(xq = xq)],extension(4,bind([[_12839], [xq]]))).
% 0.64/1.41 cnf('1.2.1.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))), xa = xa, smndt0(xb) = smndt0(xb)],extension(3,bind([[_16384, _16451, _16517, _16582], [xa, xa, smndt0(xb), smndt0(xb)]]))).
% 0.64/1.41 cnf('1.2.1.1.3.1',plain,[-(xa = xa)],extension(4,bind([[_12839], [xa]]))).
% 0.64/1.41 cnf('1.2.1.1.3.2',plain,[-(smndt0(xb) = smndt0(xb))],extension(4,bind([[_12839], [smndt0(xb)]]))).
% 0.64/1.41 cnf('1.2.1.2',plain,[-(xq = xq)],extension(4,bind([[_12839], [xq]]))).
% 0.64/1.41 cnf('1.2.1.3',plain,[-(sdtpldt0(xa, smndt0(xb)) = sdtpldt0(xa, smndt0(xb))), xa = xa, smndt0(xb) = smndt0(xb)],extension(3,bind([[_16384, _16451, _16517, _16582], [xa, xa, smndt0(xb), smndt0(xb)]]))).
% 0.64/1.41 cnf('1.2.1.3.1',plain,[-(xa = xa)],extension(4,bind([[_12839], [xa]]))).
% 0.64/1.41 cnf('1.2.1.3.2',plain,[-(smndt0(xb) = smndt0(xb)), xb = xb],extension(2,bind([[_16998, _17047], [xb, xb]]))).
% 0.64/1.41 cnf('1.2.1.3.2.1',plain,[-(xb = xb)],extension(4,bind([[_12839], [xb]]))).
% 0.64/1.41 cnf('1.2.2',plain,[-(xq = xq)],extension(4,bind([[_12839], [xq]]))).
% 0.64/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(13,bind([[_24131, _24195], [sdtpldt0(xa, smndt0(xb)), sz00]]))).
% 0.64/1.41 cnf('1.2.3.1',plain,[-(aInteger0(sz00))],extension(8)).
% 0.64/1.41 cnf('1.2.3.2',plain,[-(aInteger0(sdtpldt0(xa, smndt0(xb)))), aInteger0(xa), aInteger0(smndt0(xb))],extension(10,bind([[_18074, _18125], [xa, smndt0(xb)]]))).
% 0.64/1.41 cnf('1.2.3.2.1',plain,[-(aInteger0(xa))],extension(17)).
% 0.64/1.41 cnf('1.2.3.2.2',plain,[-(aInteger0(smndt0(xb))), aInteger0(xb)],extension(9,bind([[_17846], [xb]]))).
% 0.64/1.41 cnf('1.2.3.2.2.1',plain,[-(aInteger0(xb))],extension(18)).
% 0.64/1.41 cnf('1.2.3.3',plain,[-(sdtasdt0(sdtpldt0(xa, smndt0(xb)), sz00) = sz00), aInteger0(sdtpldt0(xa, smndt0(xb)))],extension(12,bind([[_23279], [sdtpldt0(xa, smndt0(xb))]]))).
% 0.64/1.41 cnf('1.2.3.3.1',plain,[-(aInteger0(sdtpldt0(xa, smndt0(xb))))],lemmata('1.2.3')).
% 0.64/1.41 cnf('1.2.3.4',plain,[sz00 = sz00, -(aInteger0(sz00)), aInteger0(sz00)],extension(7,bind([[_14420, _14371], [sz00, sz00]]))).
% 0.64/1.41 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([[_24810, _25053, _24696], [xq, sz00, sz00]]))).
% 0.64/1.41 cnf('1.2.3.4.1.1',plain,[aDivisorOf0(xq, sz00)],reduction('1')).
% 0.64/1.41 cnf('1.2.3.4.1.2',plain,[-(aInteger0(xq))],extension(19)).
% 0.64/1.41 cnf('1.2.3.4.1.3',plain,[xq = sz00, -(xq = sz00), sz00 = sz00],extension(5,bind([[_13271, _13327, _13382], [xq, sz00, sz00]]))).
% 0.64/1.41 cnf('1.2.3.4.1.3.1',plain,[xq = sz00],extension(20)).
% 0.64/1.41 cnf('1.2.3.4.1.3.2',plain,[-(sz00 = sz00)],extension(4,bind([[_12839], [sz00]]))).
% 0.64/1.41 cnf('1.2.3.4.1.4',plain,[-(aInteger0(sz00))],extension(8)).
% 0.64/1.41 cnf('1.2.3.4.1.5',plain,[-(sdtasdt0(xq, sz00) = sz00), aInteger0(xq)],extension(12,bind([[_23279], [xq]]))).
% 0.64/1.41 cnf('1.2.3.4.1.5.1',plain,[-(aInteger0(xq))],extension(19)).
% 0.64/1.41 cnf('1.2.3.4.2',plain,[-(aInteger0(sz00))],extension(8)).
% 0.64/1.41 cnf('1.3',plain,[-(xq = sz00), aInteger0(sz00), aInteger0(xq), sdtasdt0(xq, sz00) = sz00, -(sz00 = sz00)],extension(13,bind([[_24131, _24195], [xq, sz00]]))).
% 0.64/1.41 cnf('1.3.1',plain,[-(aInteger0(sz00))],extension(8)).
% 0.64/1.41 cnf('1.3.2',plain,[-(aInteger0(xq)), aInteger0(sz00), aDivisorOf0(xq, sz00)],extension(14,bind([[_24810, _24696], [xq, sz00]]))).
% 0.64/1.41 cnf('1.3.2.1',plain,[-(aInteger0(sz00))],extension(8)).
% 0.64/1.41 cnf('1.3.2.2',plain,[-(aDivisorOf0(xq, sz00))],lemmata('1')).
% 0.64/1.41 cnf('1.3.3',plain,[-(sdtasdt0(xq, sz00) = sz00), aInteger0(xq)],extension(12,bind([[_23279], [xq]]))).
% 0.64/1.41 cnf('1.3.3.1',plain,[-(aInteger0(xq))],extension(19)).
% 0.64/1.41 cnf('1.3.4',plain,[sz00 = sz00, -(aInteger0(sz00)), aInteger0(sz00)],extension(7,bind([[_14420, _14371], [sz00, sz00]]))).
% 0.64/1.41 cnf('1.3.4.1',plain,[aInteger0(sz00), -(aInteger0(sdtpldt0(2 ^ [], sz00))), aInteger0(2 ^ [])],extension(10,bind([[_18125, _18074], [sz00, 2 ^ []]]))).
% 0.64/1.41 cnf('1.3.4.1.1',plain,[aInteger0(sdtpldt0(2 ^ [], sz00)), -(aInteger0(2 ^ [])), sdtpldt0(2 ^ [], sz00) = 2 ^ []],extension(7,bind([[_14371, _14420], [sdtpldt0(2 ^ [], sz00), 2 ^ []]]))).
% 0.64/1.41 cnf('1.3.4.1.1.1',plain,[aInteger0(2 ^ []), sdtasdt0(xq, 2 ^ []) = sdtpldt0(xa, smndt0(xb))],extension(1,bind([[_27895], [2 ^ []]]))).
% 0.64/1.41 cnf('1.3.4.1.1.1.1',plain,[-(sdtasdt0(xq, 2 ^ []) = sdtpldt0(xa, smndt0(xb)))],extension(22)).
% 0.64/1.41 cnf('1.3.4.1.1.2',plain,[-(sdtpldt0(2 ^ [], sz00) = 2 ^ []), aInteger0(2 ^ [])],extension(11,bind([[_19921], [2 ^ []]]))).
% 0.64/1.41 cnf('1.3.4.1.1.2.1',plain,[-(aInteger0(2 ^ []))],extension(21)).
% 0.64/1.41 cnf('1.3.4.1.2',plain,[-(aInteger0(2 ^ []))],extension(21)).
% 0.64/1.41 cnf('1.3.4.2',plain,[-(aInteger0(sz00))],extension(8)).
% 0.64/1.41 %-----------------------------------------------------
% 0.72/1.42
% 0.72/1.42 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------