%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : RNG111+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n032.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 20:33:51 EDT 2022
% Result : Theorem 70.95s 69.37s
% Output : Proof 70.95s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.10 % Problem : RNG111+1 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.10 % Command : leancop_casc.sh %s %d
% 0.10/0.29 % Computer : n032.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 600
% 0.10/0.29 % DateTime : Mon May 30 21:33:28 EDT 2022
% 0.10/0.29 % CPUTime :
% 70.95/69.37 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 70.95/69.37 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 70.95/69.38
% 70.95/69.38 %-----------------------------------------------------
% 70.95/69.38 fof(m__, conjecture, ! [_98462] : (aElementOf0(_98462, xI) & (! _98462) = sz00 => ! [_98488] : (aElementOf0(_98488, xI) & (! _98488) = sz00 => iLess0(sbrdtbr0(_98488), sbrdtbr0(_98462)) => ? [_98532] : (aElementOf0(_98532, xI) & (! _98532) = sz00 & ! [_98558] : (aElementOf0(_98558, xI) & (! _98558) = sz00 => ~ iLess0(sbrdtbr0(_98558), sbrdtbr0(_98532))))) => ? [_98488] : (aElementOf0(_98488, xI) & (! _98488) = sz00 & ! [_98532] : (aElementOf0(_98532, xI) & (! _98532) = sz00 => ~ iLess0(sbrdtbr0(_98532), sbrdtbr0(_98488))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__)).
% 70.95/69.38
% 70.95/69.38 cnf(1, plain, [-(aElementOf0(22 ^ [], xI))], clausify(m__)).
% 70.95/69.38 cnf(2, plain, [22 ^ [] = sz00], clausify(m__)).
% 70.95/69.38 cnf(3, plain, [aElementOf0(_68299, xI), -(_68299 = sz00), -(aElementOf0(24 ^ [_68299], xI))], clausify(m__)).
% 70.95/69.38 cnf(4, plain, [aElementOf0(_68299, xI), -(_68299 = sz00), 24 ^ [_68299] = sz00], clausify(m__)).
% 70.95/69.38 cnf(5, plain, [aElementOf0(_68299, xI), -(_68299 = sz00), -(iLess0(sbrdtbr0(24 ^ [_68299]), sbrdtbr0(_68299)))], clausify(m__)).
% 70.95/69.38 cnf(6, plain, [-(_68223 = sz00), aElementOf0(_68223, xI), iLess0(sbrdtbr0(_68223), sbrdtbr0(22 ^ [])), -(aElementOf0(23 ^ [_68223], xI))], clausify(m__)).
% 70.95/69.38 cnf(7, plain, [-(_68223 = sz00), aElementOf0(_68223, xI), iLess0(sbrdtbr0(_68223), sbrdtbr0(22 ^ [])), 23 ^ [_68223] = sz00], clausify(m__)).
% 70.95/69.38 cnf(8, plain, [-(_68223 = sz00), aElementOf0(_68223, xI), iLess0(sbrdtbr0(_68223), sbrdtbr0(22 ^ [])), iLess0(sbrdtbr0(_68450), sbrdtbr0(23 ^ [_68223])), aElementOf0(_68450, xI), -(_68450 = sz00)], clausify(m__)).
% 70.95/69.38
% 70.95/69.38 cnf('1',plain,[22 ^ [] = sz00],start(2)).
% 70.95/69.38 cnf('1.1',plain,[-(22 ^ [] = sz00), aElementOf0(22 ^ [], xI), -(aElementOf0(24 ^ [22 ^ []], xI))],extension(3,bind([[_68299], [22 ^ []]]))).
% 70.95/69.38 cnf('1.1.1',plain,[-(aElementOf0(22 ^ [], xI))],extension(1)).
% 70.95/69.38 cnf('1.1.2',plain,[aElementOf0(24 ^ [22 ^ []], xI), -(24 ^ [22 ^ []] = sz00), iLess0(sbrdtbr0(24 ^ [22 ^ []]), sbrdtbr0(22 ^ [])), iLess0(sbrdtbr0(24 ^ [23 ^ [24 ^ [22 ^ []]]]), sbrdtbr0(23 ^ [24 ^ [22 ^ []]])), aElementOf0(24 ^ [23 ^ [24 ^ [22 ^ []]]], xI), -(24 ^ [23 ^ [24 ^ [22 ^ []]]] = sz00)],extension(8,bind([[_68223, _68450], [24 ^ [22 ^ []], 24 ^ [23 ^ [24 ^ [22 ^ []]]]]]))).
% 70.95/69.38 cnf('1.1.2.1',plain,[24 ^ [22 ^ []] = sz00, aElementOf0(22 ^ [], xI), -(22 ^ [] = sz00)],extension(4,bind([[_68299], [22 ^ []]]))).
% 70.95/69.38 cnf('1.1.2.1.1',plain,[-(aElementOf0(22 ^ [], xI))],extension(1)).
% 70.95/69.38 cnf('1.1.2.1.2',plain,[22 ^ [] = sz00],extension(2)).
% 70.95/69.38 cnf('1.1.2.2',plain,[-(iLess0(sbrdtbr0(24 ^ [22 ^ []]), sbrdtbr0(22 ^ []))), aElementOf0(22 ^ [], xI), -(22 ^ [] = sz00)],extension(5,bind([[_68299], [22 ^ []]]))).
% 70.95/69.38 cnf('1.1.2.2.1',plain,[-(aElementOf0(22 ^ [], xI))],extension(1)).
% 70.95/69.38 cnf('1.1.2.2.2',plain,[22 ^ [] = sz00],extension(2)).
% 70.95/69.38 cnf('1.1.2.3',plain,[-(iLess0(sbrdtbr0(24 ^ [23 ^ [24 ^ [22 ^ []]]]), sbrdtbr0(23 ^ [24 ^ [22 ^ []]]))), aElementOf0(23 ^ [24 ^ [22 ^ []]], xI), -(23 ^ [24 ^ [22 ^ []]] = sz00)],extension(5,bind([[_68299], [23 ^ [24 ^ [22 ^ []]]]]))).
% 70.95/69.38 cnf('1.1.2.3.1',plain,[-(aElementOf0(23 ^ [24 ^ [22 ^ []]], xI)), -(24 ^ [22 ^ []] = sz00), aElementOf0(24 ^ [22 ^ []], xI), iLess0(sbrdtbr0(24 ^ [22 ^ []]), sbrdtbr0(22 ^ []))],extension(6,bind([[_68223], [24 ^ [22 ^ []]]]))).
% 70.95/69.38 cnf('1.1.2.3.1.1',plain,[24 ^ [22 ^ []] = sz00],lemmata('1.1.2')).
% 70.95/69.38 cnf('1.1.2.3.1.2',plain,[-(aElementOf0(24 ^ [22 ^ []], xI))],reduction('1.1')).
% 70.95/69.38 cnf('1.1.2.3.1.3',plain,[-(iLess0(sbrdtbr0(24 ^ [22 ^ []]), sbrdtbr0(22 ^ [])))],lemmata('1.1.2')).
% 70.95/69.38 cnf('1.1.2.3.2',plain,[23 ^ [24 ^ [22 ^ []]] = sz00, -(24 ^ [22 ^ []] = sz00), aElementOf0(24 ^ [22 ^ []], xI), iLess0(sbrdtbr0(24 ^ [22 ^ []]), sbrdtbr0(22 ^ []))],extension(7,bind([[_68223], [24 ^ [22 ^ []]]]))).
% 70.95/69.38 cnf('1.1.2.3.2.1',plain,[24 ^ [22 ^ []] = sz00],lemmata('1.1.2')).
% 70.95/69.38 cnf('1.1.2.3.2.2',plain,[-(aElementOf0(24 ^ [22 ^ []], xI))],reduction('1.1')).
% 70.95/69.38 cnf('1.1.2.3.2.3',plain,[-(iLess0(sbrdtbr0(24 ^ [22 ^ []]), sbrdtbr0(22 ^ [])))],lemmata('1.1.2')).
% 70.95/69.38 cnf('1.1.2.4',plain,[-(aElementOf0(24 ^ [23 ^ [24 ^ [22 ^ []]]], xI)), aElementOf0(23 ^ [24 ^ [22 ^ []]], xI), -(23 ^ [24 ^ [22 ^ []]] = sz00)],extension(3,bind([[_68299], [23 ^ [24 ^ [22 ^ []]]]]))).
% 70.95/69.38 cnf('1.1.2.4.1',plain,[-(aElementOf0(23 ^ [24 ^ [22 ^ []]], xI)), -(24 ^ [22 ^ []] = sz00), aElementOf0(24 ^ [22 ^ []], xI), iLess0(sbrdtbr0(24 ^ [22 ^ []]), sbrdtbr0(22 ^ []))],extension(6,bind([[_68223], [24 ^ [22 ^ []]]]))).
% 70.95/69.38 cnf('1.1.2.4.1.1',plain,[24 ^ [22 ^ []] = sz00],lemmata('1.1.2')).
% 70.95/69.38 cnf('1.1.2.4.1.2',plain,[-(aElementOf0(24 ^ [22 ^ []], xI))],reduction('1.1')).
% 70.95/69.38 cnf('1.1.2.4.1.3',plain,[-(iLess0(sbrdtbr0(24 ^ [22 ^ []]), sbrdtbr0(22 ^ [])))],lemmata('1.1.2')).
% 70.95/69.38 cnf('1.1.2.4.2',plain,[23 ^ [24 ^ [22 ^ []]] = sz00, -(24 ^ [22 ^ []] = sz00), aElementOf0(24 ^ [22 ^ []], xI), iLess0(sbrdtbr0(24 ^ [22 ^ []]), sbrdtbr0(22 ^ []))],extension(7,bind([[_68223], [24 ^ [22 ^ []]]]))).
% 70.95/69.38 cnf('1.1.2.4.2.1',plain,[24 ^ [22 ^ []] = sz00],lemmata('1.1.2')).
% 70.95/69.38 cnf('1.1.2.4.2.2',plain,[-(aElementOf0(24 ^ [22 ^ []], xI))],reduction('1.1')).
% 70.95/69.38 cnf('1.1.2.4.2.3',plain,[-(iLess0(sbrdtbr0(24 ^ [22 ^ []]), sbrdtbr0(22 ^ [])))],lemmata('1.1.2')).
% 70.95/69.38 cnf('1.1.2.5',plain,[24 ^ [23 ^ [24 ^ [22 ^ []]]] = sz00, aElementOf0(23 ^ [24 ^ [22 ^ []]], xI), -(23 ^ [24 ^ [22 ^ []]] = sz00)],extension(4,bind([[_68299], [23 ^ [24 ^ [22 ^ []]]]]))).
% 70.95/69.38 cnf('1.1.2.5.1',plain,[-(aElementOf0(23 ^ [24 ^ [22 ^ []]], xI)), -(24 ^ [22 ^ []] = sz00), aElementOf0(24 ^ [22 ^ []], xI), iLess0(sbrdtbr0(24 ^ [22 ^ []]), sbrdtbr0(22 ^ []))],extension(6,bind([[_68223], [24 ^ [22 ^ []]]]))).
% 70.95/69.38 cnf('1.1.2.5.1.1',plain,[24 ^ [22 ^ []] = sz00],lemmata('1.1.2')).
% 70.95/69.38 cnf('1.1.2.5.1.2',plain,[-(aElementOf0(24 ^ [22 ^ []], xI))],reduction('1.1')).
% 70.95/69.38 cnf('1.1.2.5.1.3',plain,[-(iLess0(sbrdtbr0(24 ^ [22 ^ []]), sbrdtbr0(22 ^ [])))],lemmata('1.1.2')).
% 70.95/69.38 cnf('1.1.2.5.2',plain,[23 ^ [24 ^ [22 ^ []]] = sz00, -(24 ^ [22 ^ []] = sz00), aElementOf0(24 ^ [22 ^ []], xI), iLess0(sbrdtbr0(24 ^ [22 ^ []]), sbrdtbr0(22 ^ []))],extension(7,bind([[_68223], [24 ^ [22 ^ []]]]))).
% 70.95/69.38 cnf('1.1.2.5.2.1',plain,[24 ^ [22 ^ []] = sz00],lemmata('1.1.2')).
% 70.95/69.38 cnf('1.1.2.5.2.2',plain,[-(aElementOf0(24 ^ [22 ^ []], xI))],reduction('1.1')).
% 70.95/69.38 cnf('1.1.2.5.2.3',plain,[-(iLess0(sbrdtbr0(24 ^ [22 ^ []]), sbrdtbr0(22 ^ [])))],lemmata('1.1.2')).
% 70.95/69.38 %-----------------------------------------------------
% 70.95/69.38
% 70.95/69.38 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------