%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS163+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n023.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 : 300s
% DateTime : Fri May 19 11:26:24 EDT 2023
% Result : Theorem 0.32s 1.37s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : KRS163+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n023.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 : 300
% 0.12/0.33 % DateTime : Thu May 18 23:23:29 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.32/1.37
% 0.32/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.32/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.32/1.37 %-----------------------------------------------------
% 0.32/1.37 ncf(matrix, plain, [(170 ^ _25670) ^ [] : [cowlThing(171 ^ []), -(cowlNothing(171 ^ [])), 183 ^ _25670 : [(184 ^ _25670) ^ [] : [-(xsd_string(180 ^ []))], (186 ^ _25670) ^ [] : [-(xsd_integer(180 ^ []))]], 187 ^ _25670 : [(188 ^ _25670) ^ [] : [xsd_integer(180 ^ [])], (190 ^ _25670) ^ [] : [xsd_string(180 ^ [])]], cowlThing(ia), cowlThing(ib), -(ia = ib)], (2 ^ _25670) ^ [_25794] : [-(_25794 = _25794)], (4 ^ _25670) ^ [_25901, _25903] : [_25903 = _25901, -(_25901 = _25903)], (10 ^ _25670) ^ [_26105, _26107, _26109] : [-(_26109 = _26105), _26109 = _26107, _26107 = _26105], (20 ^ _25670) ^ [_26418, _26420] : [-(cB(_26418)), _26420 = _26418, cB(_26420)], (30 ^ _25670) ^ [_26713, _26715] : [-(cA(_26713)), _26715 = _26713, cA(_26715)], (40 ^ _25670) ^ [_27008, _27010] : [-(cowlNothing(_27008)), _27010 = _27008, cowlNothing(_27010)], (50 ^ _25670) ^ [_27303, _27305] : [-(xsd_string(_27303)), _27305 = _27303, xsd_string(_27305)], (60 ^ _25670) ^ [_27598, _27600] : [-(xsd_integer(_27598)), _27600 = _27598, xsd_integer(_27600)], (70 ^ _25670) ^ [_27873, _27875] : [-(cowlThing(_27873)), _27875 = _27873, cowlThing(_27875)], (80 ^ _25670) ^ [_28184, _28186] : [-(cA(_28184)), _28186 = _28184, cA(_28186)], (90 ^ _25670) ^ [_28479, _28481] : [-(cB(_28479)), _28481 = _28479, cB(_28481)], (100 ^ _25670) ^ [_28774, _28776] : [-(cowlNothing(_28774)), _28776 = _28774, cowlNothing(_28776)], (110 ^ _25670) ^ [_29069, _29071] : [-(cowlThing(_29069)), _29071 = _29069, cowlThing(_29071)], (120 ^ _25670) ^ [_29364, _29366] : [-(xsd_integer(_29364)), _29366 = _29364, xsd_integer(_29366)], (130 ^ _25670) ^ [_29659, _29661] : [-(xsd_string(_29659)), _29661 = _29659, xsd_string(_29661)], (140 ^ _25670) ^ [_29945] : [-(cowlThing(_29945))], (142 ^ _25670) ^ [_29987] : [cowlNothing(_29987)], (156 ^ _25670) ^ [] : [-(cA(ia))], (158 ^ _25670) ^ [] : [-(cowlThing(ia))], (160 ^ _25670) ^ [] : [-(cB(ib))], (162 ^ _25670) ^ [] : [-(cowlThing(ib))], (164 ^ _25670) ^ [_30646] : [cB(_30646), cA(_30646)], (144 ^ _25670) ^ [_30110] : [xsd_string(_30110), xsd_integer(_30110)], (150 ^ _25670) ^ [_30263] : [-(xsd_integer(_30263)), -(xsd_string(_30263))]], input).
% 0.32/1.37 ncf('1',plain,[cowlNothing(171 ^ [])],start(142 ^ 0,bind([[_29987], [171 ^ []]]))).
% 0.32/1.37 ncf('1.1',plain,[-(cowlNothing(171 ^ [])), cowlThing(171 ^ []), 184 : -(xsd_string(180 ^ [])), 188 : xsd_integer(180 ^ []), 188 : cowlThing(ia), 188 : cowlThing(ib), 188 : -(ia = ib)],extension(170 ^ 1)).
% 0.32/1.37 ncf('1.1.1',plain,[-(cowlThing(171 ^ []))],extension(140 ^ 2,bind([[_29945], [171 ^ []]]))).
% 0.32/1.37 ncf('1.1.2',plain,[xsd_string(180 ^ []), -(xsd_string(180 ^ [])), 180 ^ [] = 180 ^ []],extension(50 ^ 4,bind([[_27303, _27305], [180 ^ [], 180 ^ []]]))).
% 0.32/1.37 ncf('1.1.2.1',plain,[xsd_string(180 ^ []), xsd_integer(180 ^ [])],extension(144 ^ 5,bind([[_30110], [180 ^ []]]))).
% 0.32/1.37 ncf('1.1.2.1.1',plain,[-(xsd_integer(180 ^ []))],extension(186 ^ 6)).
% 0.32/1.37 ncf('1.1.2.2',plain,[-(180 ^ [] = 180 ^ [])],extension(2 ^ 5,bind([[_25794], [180 ^ []]]))).
% 0.32/1.37 ncf('1.1.3',plain,[-(xsd_integer(180 ^ [])), -(xsd_string(180 ^ []))],extension(150 ^ 4,bind([[_30263], [180 ^ []]]))).
% 0.32/1.37 ncf('1.1.3.1',plain,[xsd_string(180 ^ [])],extension(190 ^ 5)).
% 0.32/1.37 ncf('1.1.4',plain,[-(cowlThing(ia))],extension(140 ^ 2,bind([[_29945], [ia]]))).
% 0.32/1.37 ncf('1.1.5',plain,[-(cowlThing(ib))],extension(140 ^ 2,bind([[_29945], [ib]]))).
% 0.32/1.37 ncf('1.1.6',plain,[ia = ib, -(cA(ib)), cA(ia)],extension(30 ^ 2,bind([[_26713, _26715], [ib, ia]]))).
% 0.32/1.37 ncf('1.1.6.1',plain,[cA(ib), cB(ib)],extension(164 ^ 3,bind([[_30646], [ib]]))).
% 0.32/1.37 ncf('1.1.6.1.1',plain,[-(cB(ib))],extension(160 ^ 4)).
% 0.32/1.37 ncf('1.1.6.2',plain,[-(cA(ia))],extension(156 ^ 3)).
% 0.32/1.37 %-----------------------------------------------------
% 0.32/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------