%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS132+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n010.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:20 EDT 2023
% Result : Theorem 0.31s 1.37s
% Output : Proof 0.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : KRS132+1 : TPTP v8.1.2. Released v3.1.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.11/0.33 % Computer : n010.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Thu May 18 22:53:27 EDT 2023
% 0.11/0.33 % CPUTime :
% 0.31/1.37
% 0.31/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.31/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.31/1.37 %-----------------------------------------------------
% 0.31/1.37 ncf(matrix, plain, [(163 ^ _27313) ^ [] : [cowlThing(164 ^ []), -(cowlNothing(164 ^ [])), 176 ^ _27313 : [(177 ^ _27313) ^ [] : [-(xsd_string(173 ^ []))], (179 ^ _27313) ^ [] : [-(xsd_integer(173 ^ []))]], 180 ^ _27313 : [(181 ^ _27313) ^ [] : [xsd_integer(173 ^ [])], (183 ^ _27313) ^ [] : [xsd_string(173 ^ [])]], 187 ^ _27313 : [(188 ^ _27313) ^ [] : [-(cAorB(184 ^ []))], (190 ^ _27313) ^ [] : [cB(184 ^ [])], (192 ^ _27313) ^ [] : [cA(184 ^ [])]], 193 ^ _27313 : [(200 ^ _27313) ^ [] : [cAorB(184 ^ [])], (194 ^ _27313) ^ [] : [-(cB(184 ^ [])), -(cA(184 ^ []))]]], (2 ^ _27313) ^ [_27417] : [-(cowlThing(_27417))], (4 ^ _27313) ^ [_27459] : [cowlNothing(_27459)], (6 ^ _27313) ^ [_27582] : [xsd_string(_27582), xsd_integer(_27582)], (12 ^ _27313) ^ [_27735] : [-(xsd_integer(_27735)), -(xsd_string(_27735))], (18 ^ _27313) ^ [_27955] : [cA(_27955), 22 ^ _27313 : [(23 ^ _27313) ^ [] : [-(rq(_27955, 21 ^ [_27955]))], (25 ^ _27313) ^ [] : [-(cowlThing(21 ^ [_27955]))]]], (27 ^ _27313) ^ [_28241] : [-(cA(_28241)), 28 ^ _27313 : [(29 ^ _27313) ^ [_28329] : [rq(_28241, _28329), cowlThing(_28329)]]], (37 ^ _27313) ^ [_28603] : [cAorB(_28603), 41 ^ _27313 : [(42 ^ _27313) ^ [] : [-(rs(_28603, 40 ^ [_28603]))], (44 ^ _27313) ^ [] : [-(cowlThing(40 ^ [_28603]))]]], (46 ^ _27313) ^ [_28889] : [-(cAorB(_28889)), 47 ^ _27313 : [(48 ^ _27313) ^ [_28977] : [rs(_28889, _28977), cowlThing(_28977)]]], (56 ^ _27313) ^ [_29251] : [cB(_29251), 60 ^ _27313 : [(61 ^ _27313) ^ [] : [-(rr(_29251, 59 ^ [_29251]))], (63 ^ _27313) ^ [] : [-(cowlThing(59 ^ [_29251]))]]], (65 ^ _27313) ^ [_29537] : [-(cB(_29537)), 66 ^ _27313 : [(67 ^ _27313) ^ [_29625] : [rr(_29537, _29625), cowlThing(_29625)]]], (75 ^ _27313) ^ [_29870] : [cNothing(_29870), -(rp(_29870, 78 ^ [_29870]))], (82 ^ _27313) ^ [_30109] : [cNothing(_30109), 85 ^ _27313 : [(86 ^ _27313) ^ [_30220] : [rp(_30109, _30220)]]], (98 ^ _27313) ^ [_30646] : [100 ^ _27313 : [(101 ^ _27313) ^ [] : [-(rq(_30646, 99 ^ [_30646]))], (103 ^ _27313) ^ [] : [cNothing(99 ^ [_30646])]], -(cnotA(_30646))], (88 ^ _27313) ^ [_30349] : [cnotA(_30349), 91 ^ _27313 : [(92 ^ _27313) ^ [_30479] : [rq(_30349, _30479), -(cNothing(_30479))]]], (117 ^ _27313) ^ [_31294] : [119 ^ _27313 : [(120 ^ _27313) ^ [] : [-(rs(_31294, 118 ^ [_31294]))], (122 ^ _27313) ^ [] : [cNothing(118 ^ [_31294])]], -(cnotAorB(_31294))], (107 ^ _27313) ^ [_30997] : [cnotAorB(_30997), 110 ^ _27313 : [(111 ^ _27313) ^ [_31127] : [rs(_30997, _31127), -(cNothing(_31127))]]], (126 ^ _27313) ^ [_31645] : [cnotAorB(_31645), 129 ^ _27313 : [(130 ^ _27313) ^ [] : [-(cnotB(_31645))], (132 ^ _27313) ^ [] : [-(cnotA(_31645))]]], (134 ^ _27313) ^ [_31868] : [-(cnotAorB(_31868)), cnotB(_31868), cnotA(_31868)], (154 ^ _27313) ^ [_32445] : [156 ^ _27313 : [(157 ^ _27313) ^ [] : [-(rr(_32445, 155 ^ [_32445]))], (159 ^ _27313) ^ [] : [cNothing(155 ^ [_32445])]], -(cnotB(_32445))], (144 ^ _27313) ^ [_32148] : [cnotB(_32148), 147 ^ _27313 : [(148 ^ _27313) ^ [_32278] : [rr(_32148, _32278), -(cNothing(_32278))]]]], input).
% 0.31/1.37 ncf('1',plain,[cowlNothing(164 ^ [])],start(4 ^ 0,bind([[_27459], [164 ^ []]]))).
% 0.31/1.37 ncf('1.1',plain,[-(cowlNothing(164 ^ [])), cowlThing(164 ^ []), 177 : -(xsd_string(173 ^ [])), 181 : xsd_integer(173 ^ []), 188 : -(cAorB(184 ^ [])), 194 : -(cB(184 ^ [])), 194 : -(cA(184 ^ []))],extension(163 ^ 1)).
% 0.31/1.37 ncf('1.1.1',plain,[-(cowlThing(164 ^ []))],extension(2 ^ 2,bind([[_27417], [164 ^ []]]))).
% 0.31/1.37 ncf('1.1.2',plain,[xsd_string(173 ^ []), xsd_integer(173 ^ [])],extension(6 ^ 4,bind([[_27582], [173 ^ []]]))).
% 0.31/1.37 ncf('1.1.2.1',plain,[-(xsd_integer(173 ^ []))],extension(179 ^ 5)).
% 0.31/1.37 ncf('1.1.3',plain,[-(xsd_integer(173 ^ [])), -(xsd_string(173 ^ []))],extension(12 ^ 4,bind([[_27735], [173 ^ []]]))).
% 0.31/1.37 ncf('1.1.3.1',plain,[xsd_string(173 ^ [])],extension(183 ^ 5)).
% 0.31/1.37 ncf('1.1.4',plain,[cAorB(184 ^ []), 42 : -(rs(184 ^ [], 40 ^ [184 ^ []]))],extension(37 ^ 4,bind([[_28603], [184 ^ []]]))).
% 0.31/1.37 ncf('1.1.4.1',plain,[rs(184 ^ [], 40 ^ [184 ^ []]), 111 : -(cNothing(40 ^ [184 ^ []])), 111 : cnotAorB(184 ^ [])],extension(107 ^ 7,bind([[_30997, _31127], [184 ^ [], 40 ^ [184 ^ []]]]))).
% 0.31/1.37 ncf('1.1.4.1.1',plain,[cNothing(40 ^ [184 ^ []]), -(rp(40 ^ [184 ^ []], 78 ^ [40 ^ [184 ^ []]]))],extension(75 ^ 10,bind([[_29870], [40 ^ [184 ^ []]]]))).
% 0.31/1.37 ncf('1.1.4.1.1.1',plain,[rp(40 ^ [184 ^ []], 78 ^ [40 ^ [184 ^ []]]), cNothing(40 ^ [184 ^ []])],extension(82 ^ 11,bind([[_30109, _30220], [40 ^ [184 ^ []], 78 ^ [40 ^ [184 ^ []]]]]))).
% 0.31/1.37 ncf('1.1.4.1.1.1.1',plain,[-(cNothing(40 ^ [184 ^ []]))],reduction('1.1.4.1')).
% 0.31/1.37 ncf('1.1.4.1.2',plain,[-(cnotAorB(184 ^ [])), cnotB(184 ^ []), cnotA(184 ^ [])],extension(134 ^ 8,bind([[_31868], [184 ^ []]]))).
% 0.31/1.37 ncf('1.1.4.1.2.1',plain,[-(cnotB(184 ^ [])), 157 : -(rr(184 ^ [], 155 ^ [184 ^ []]))],extension(154 ^ 9,bind([[_32445], [184 ^ []]]))).
% 0.31/1.37 ncf('1.1.4.1.2.1.1',plain,[rr(184 ^ [], 155 ^ [184 ^ []]), 67 : cowlThing(155 ^ [184 ^ []]), 67 : -(cB(184 ^ []))],extension(65 ^ 12,bind([[_29537, _29625], [184 ^ [], 155 ^ [184 ^ []]]]))).
% 0.31/1.37 ncf('1.1.4.1.2.1.1.1',plain,[-(cowlThing(155 ^ [184 ^ []]))],extension(2 ^ 15,bind([[_27417], [155 ^ [184 ^ []]]]))).
% 0.31/1.37 ncf('1.1.4.1.2.1.1.2',plain,[cB(184 ^ [])],extension(190 ^ 13)).
% 0.31/1.37 ncf('1.1.4.1.2.2',plain,[-(cnotA(184 ^ [])), 101 : -(rq(184 ^ [], 99 ^ [184 ^ []]))],extension(98 ^ 9,bind([[_30646], [184 ^ []]]))).
% 0.31/1.37 ncf('1.1.4.1.2.2.1',plain,[rq(184 ^ [], 99 ^ [184 ^ []]), 29 : cowlThing(99 ^ [184 ^ []]), 29 : -(cA(184 ^ []))],extension(27 ^ 12,bind([[_28241, _28329], [184 ^ [], 99 ^ [184 ^ []]]]))).
% 0.31/1.37 ncf('1.1.4.1.2.2.1.1',plain,[-(cowlThing(99 ^ [184 ^ []]))],extension(2 ^ 15,bind([[_27417], [99 ^ [184 ^ []]]]))).
% 0.31/1.37 ncf('1.1.4.1.2.2.1.2',plain,[cA(184 ^ [])],extension(192 ^ 13)).
% 0.31/1.37 ncf('1.1.5',plain,[cB(184 ^ []), 61 : -(rr(184 ^ [], 59 ^ [184 ^ []]))],extension(56 ^ 4,bind([[_29251], [184 ^ []]]))).
% 0.31/1.37 ncf('1.1.5.1',plain,[rr(184 ^ [], 59 ^ [184 ^ []]), 148 : -(cNothing(59 ^ [184 ^ []])), 148 : cnotB(184 ^ [])],extension(144 ^ 7,bind([[_32148, _32278], [184 ^ [], 59 ^ [184 ^ []]]]))).
% 0.31/1.37 ncf('1.1.5.1.1',plain,[cNothing(59 ^ [184 ^ []]), -(rp(59 ^ [184 ^ []], 78 ^ [59 ^ [184 ^ []]]))],extension(75 ^ 10,bind([[_29870], [59 ^ [184 ^ []]]]))).
% 0.31/1.37 ncf('1.1.5.1.1.1',plain,[rp(59 ^ [184 ^ []], 78 ^ [59 ^ [184 ^ []]]), cNothing(59 ^ [184 ^ []])],extension(82 ^ 11,bind([[_30109, _30220], [59 ^ [184 ^ []], 78 ^ [59 ^ [184 ^ []]]]]))).
% 0.31/1.37 ncf('1.1.5.1.1.1.1',plain,[-(cNothing(59 ^ [184 ^ []]))],reduction('1.1.5.1')).
% 0.31/1.37 ncf('1.1.5.1.2',plain,[-(cnotB(184 ^ [])), cnotAorB(184 ^ [])],extension(126 ^ 8,bind([[_31645], [184 ^ []]]))).
% 0.31/1.37 ncf('1.1.5.1.2.1',plain,[-(cnotAorB(184 ^ [])), 120 : -(rs(184 ^ [], 118 ^ [184 ^ []]))],extension(117 ^ 9,bind([[_31294], [184 ^ []]]))).
% 0.31/1.37 ncf('1.1.5.1.2.1.1',plain,[rs(184 ^ [], 118 ^ [184 ^ []]), 48 : cowlThing(118 ^ [184 ^ []]), 48 : -(cAorB(184 ^ []))],extension(46 ^ 12,bind([[_28889, _28977], [184 ^ [], 118 ^ [184 ^ []]]]))).
% 0.31/1.37 ncf('1.1.5.1.2.1.1.1',plain,[-(cowlThing(118 ^ [184 ^ []]))],extension(2 ^ 15,bind([[_27417], [118 ^ [184 ^ []]]]))).
% 0.31/1.37 ncf('1.1.5.1.2.1.1.2',plain,[cAorB(184 ^ [])],extension(200 ^ 13)).
% 0.31/1.37 ncf('1.1.6',plain,[cA(184 ^ []), 23 : -(rq(184 ^ [], 21 ^ [184 ^ []]))],extension(18 ^ 4,bind([[_27955], [184 ^ []]]))).
% 0.31/1.37 ncf('1.1.6.1',plain,[rq(184 ^ [], 21 ^ [184 ^ []]), 92 : -(cNothing(21 ^ [184 ^ []])), 92 : cnotA(184 ^ [])],extension(88 ^ 7,bind([[_30349, _30479], [184 ^ [], 21 ^ [184 ^ []]]]))).
% 0.31/1.37 ncf('1.1.6.1.1',plain,[cNothing(21 ^ [184 ^ []]), -(rp(21 ^ [184 ^ []], 78 ^ [21 ^ [184 ^ []]]))],extension(75 ^ 10,bind([[_29870], [21 ^ [184 ^ []]]]))).
% 0.31/1.37 ncf('1.1.6.1.1.1',plain,[rp(21 ^ [184 ^ []], 78 ^ [21 ^ [184 ^ []]]), cNothing(21 ^ [184 ^ []])],extension(82 ^ 11,bind([[_30109, _30220], [21 ^ [184 ^ []], 78 ^ [21 ^ [184 ^ []]]]]))).
% 0.31/1.37 ncf('1.1.6.1.1.1.1',plain,[-(cNothing(21 ^ [184 ^ []]))],reduction('1.1.6.1')).
% 0.31/1.37 ncf('1.1.6.1.2',plain,[-(cnotA(184 ^ [])), cnotAorB(184 ^ [])],extension(126 ^ 8,bind([[_31645], [184 ^ []]]))).
% 0.31/1.37 ncf('1.1.6.1.2.1',plain,[-(cnotAorB(184 ^ [])), 120 : -(rs(184 ^ [], 118 ^ [184 ^ []]))],extension(117 ^ 9,bind([[_31294], [184 ^ []]]))).
% 0.31/1.37 ncf('1.1.6.1.2.1.1',plain,[rs(184 ^ [], 118 ^ [184 ^ []]), 48 : cowlThing(118 ^ [184 ^ []]), 48 : -(cAorB(184 ^ []))],extension(46 ^ 12,bind([[_28889, _28977], [184 ^ [], 118 ^ [184 ^ []]]]))).
% 0.31/1.37 ncf('1.1.6.1.2.1.1.1',plain,[-(cowlThing(118 ^ [184 ^ []]))],extension(2 ^ 15,bind([[_27417], [118 ^ [184 ^ []]]]))).
% 0.31/1.37 ncf('1.1.6.1.2.1.1.2',plain,[cAorB(184 ^ [])],extension(200 ^ 13)).
% 0.31/1.37 %-----------------------------------------------------
% 0.31/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------