%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS131+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.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 : 300s
% DateTime : Fri May 19 11:26:20 EDT 2023
% Result : Theorem 0.33s 1.38s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS131+1 : TPTP v8.1.2. Released v3.1.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n004.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 22:58:09 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.33/1.38
% 0.33/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.33/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 ncf(matrix, plain, [(69 ^ _14811) ^ [] : [cowlThing(70 ^ []), -(cowlNothing(70 ^ [])), 82 ^ _14811 : [(83 ^ _14811) ^ [] : [-(xsd_string(79 ^ []))], (85 ^ _14811) ^ [] : [-(xsd_integer(79 ^ []))]], 86 ^ _14811 : [(87 ^ _14811) ^ [] : [xsd_integer(79 ^ [])], (89 ^ _14811) ^ [] : [xsd_string(79 ^ [])]], 93 ^ _14811 : [(94 ^ _14811) ^ [] : [-(cnotA(90 ^ []))], (96 ^ _14811) ^ [] : [-(cA(90 ^ []))]], 97 ^ _14811 : [(98 ^ _14811) ^ [] : [cA(90 ^ [])], (100 ^ _14811) ^ [] : [cnotA(90 ^ [])]]], (2 ^ _14811) ^ [_14915] : [-(cowlThing(_14915))], (4 ^ _14811) ^ [_14957] : [cowlNothing(_14957)], (6 ^ _14811) ^ [_15080] : [xsd_string(_15080), xsd_integer(_15080)], (12 ^ _14811) ^ [_15233] : [-(xsd_integer(_15233)), -(xsd_string(_15233))], (18 ^ _14811) ^ [_15453] : [cA(_15453), 22 ^ _14811 : [(23 ^ _14811) ^ [] : [-(rq(_15453, 21 ^ [_15453]))], (25 ^ _14811) ^ [] : [-(cowlThing(21 ^ [_15453]))]]], (27 ^ _14811) ^ [_15739] : [-(cA(_15739)), 28 ^ _14811 : [(29 ^ _14811) ^ [_15827] : [rq(_15739, _15827), cowlThing(_15827)]]], (37 ^ _14811) ^ [_16072] : [cNothing(_16072), 40 ^ _14811 : [(41 ^ _14811) ^ [_16183] : [rp(_16072, _16183)]]], (43 ^ _14811) ^ [_16283] : [cNothing(_16283), -(rp(_16283, 46 ^ [_16283]))], (60 ^ _14811) ^ [_16828] : [62 ^ _14811 : [(63 ^ _14811) ^ [] : [-(rq(_16828, 61 ^ [_16828]))], (65 ^ _14811) ^ [] : [cNothing(61 ^ [_16828])]], -(cnotA(_16828))], (50 ^ _14811) ^ [_16531] : [cnotA(_16531), 53 ^ _14811 : [(54 ^ _14811) ^ [_16661] : [rq(_16531, _16661), -(cNothing(_16661))]]]], input).
% 0.33/1.38 ncf('1',plain,[cowlNothing(70 ^ [])],start(4 ^ 0,bind([[_14957], [70 ^ []]]))).
% 0.33/1.38 ncf('1.1',plain,[-(cowlNothing(70 ^ [])), cowlThing(70 ^ []), 83 : -(xsd_string(79 ^ [])), 87 : xsd_integer(79 ^ []), 94 : -(cnotA(90 ^ [])), 98 : cA(90 ^ [])],extension(69 ^ 1)).
% 0.33/1.38 ncf('1.1.1',plain,[-(cowlThing(70 ^ []))],extension(2 ^ 2,bind([[_14915], [70 ^ []]]))).
% 0.33/1.38 ncf('1.1.2',plain,[xsd_string(79 ^ []), xsd_integer(79 ^ [])],extension(6 ^ 4,bind([[_15080], [79 ^ []]]))).
% 0.33/1.38 ncf('1.1.2.1',plain,[-(xsd_integer(79 ^ []))],extension(85 ^ 5)).
% 0.33/1.38 ncf('1.1.3',plain,[-(xsd_integer(79 ^ [])), -(xsd_string(79 ^ []))],extension(12 ^ 4,bind([[_15233], [79 ^ []]]))).
% 0.33/1.38 ncf('1.1.3.1',plain,[xsd_string(79 ^ [])],extension(89 ^ 5)).
% 0.33/1.38 ncf('1.1.4',plain,[cnotA(90 ^ []), 54 : rq(90 ^ [], 21 ^ [90 ^ []]), 54 : -(cNothing(21 ^ [90 ^ []]))],extension(50 ^ 4,bind([[_16531, _16661], [90 ^ [], 21 ^ [90 ^ []]]]))).
% 0.33/1.38 ncf('1.1.4.1',plain,[-(rq(90 ^ [], 21 ^ [90 ^ []])), cA(90 ^ [])],extension(18 ^ 7,bind([[_15453], [90 ^ []]]))).
% 0.33/1.38 ncf('1.1.4.1.1',plain,[-(cA(90 ^ []))],extension(96 ^ 8)).
% 0.33/1.38 ncf('1.1.4.2',plain,[cNothing(21 ^ [90 ^ []]), 41 : rp(21 ^ [90 ^ []], 46 ^ [21 ^ [90 ^ []]])],extension(37 ^ 7,bind([[_16072, _16183], [21 ^ [90 ^ []], 46 ^ [21 ^ [90 ^ []]]]]))).
% 0.33/1.38 ncf('1.1.4.2.1',plain,[-(rp(21 ^ [90 ^ []], 46 ^ [21 ^ [90 ^ []]])), cNothing(21 ^ [90 ^ []])],extension(43 ^ 10,bind([[_16283], [21 ^ [90 ^ []]]]))).
% 0.33/1.38 ncf('1.1.4.2.1.1',plain,[-(cNothing(21 ^ [90 ^ []]))],reduction('1.1.4')).
% 0.33/1.38 ncf('1.1.5',plain,[-(cA(90 ^ [])), 29 : rq(90 ^ [], 61 ^ [90 ^ []]), 29 : cowlThing(61 ^ [90 ^ []])],extension(27 ^ 4,bind([[_15739, _15827], [90 ^ [], 61 ^ [90 ^ []]]]))).
% 0.33/1.38 ncf('1.1.5.1',plain,[-(rq(90 ^ [], 61 ^ [90 ^ []])), -(cnotA(90 ^ []))],extension(60 ^ 7,bind([[_16828], [90 ^ []]]))).
% 0.33/1.38 ncf('1.1.5.1.1',plain,[cnotA(90 ^ [])],extension(100 ^ 8)).
% 0.33/1.38 ncf('1.1.5.2',plain,[-(cowlThing(61 ^ [90 ^ []]))],extension(2 ^ 7,bind([[_14915], [61 ^ [90 ^ []]]]))).
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------