%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS174+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n001.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:26 EDT 2023
% Result : Theorem 0.33s 1.37s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS174+1 : TPTP v8.1.2. Released v3.1.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n001.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:32:50 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.33/1.37
% 0.33/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 ncf(matrix, plain, [(222 ^ _33547) ^ [] : [cowlThing(223 ^ []), -(cowlNothing(223 ^ [])), 235 ^ _33547 : [(236 ^ _33547) ^ [] : [-(xsd_string(232 ^ []))], (238 ^ _33547) ^ [] : [-(xsd_integer(232 ^ []))]], 239 ^ _33547 : [(240 ^ _33547) ^ [] : [xsd_integer(232 ^ [])], (242 ^ _33547) ^ [] : [xsd_string(232 ^ [])]], 246 ^ _33547 : [(247 ^ _33547) ^ [] : [-(cA_and_B(243 ^ []))], (249 ^ _33547) ^ [] : [cB(243 ^ [])], (251 ^ _33547) ^ [] : [cA(243 ^ [])]], 252 ^ _33547 : [(259 ^ _33547) ^ [] : [cA_and_B(243 ^ [])], (253 ^ _33547) ^ [] : [-(cB(243 ^ [])), -(cA(243 ^ []))]]], (2 ^ _33547) ^ [_33671] : [-(_33671 = _33671)], (4 ^ _33547) ^ [_33778, _33780] : [_33780 = _33778, -(_33778 = _33780)], (10 ^ _33547) ^ [_33982, _33984, _33986] : [-(_33986 = _33982), _33986 = _33984, _33984 = _33982], (20 ^ _33547) ^ [_34295, _34297] : [-(cowlThing(_34295)), _34297 = _34295, cowlThing(_34297)], (30 ^ _33547) ^ [_34590, _34592] : [-(cowlNothing(_34590)), _34592 = _34590, cowlNothing(_34592)], (40 ^ _33547) ^ [_34885, _34887] : [-(xsd_string(_34885)), _34887 = _34885, xsd_string(_34887)], (50 ^ _33547) ^ [_35180, _35182] : [-(xsd_integer(_35180)), _35182 = _35180, xsd_integer(_35182)], (60 ^ _33547) ^ [_35475, _35477] : [-(cA_and_B(_35475)), _35477 = _35475, cA_and_B(_35477)], (70 ^ _33547) ^ [_35770, _35772] : [-(cB(_35770)), _35772 = _35770, cB(_35772)], (80 ^ _33547) ^ [_36045, _36047] : [-(cA(_36045)), _36047 = _36045, cA(_36047)], (90 ^ _33547) ^ [_36358, _36360] : [-(cA(_36358)), _36360 = _36358, cA(_36360)], (100 ^ _33547) ^ [_36653, _36655] : [-(cA_and_B(_36653)), _36655 = _36653, cA_and_B(_36655)], (110 ^ _33547) ^ [_36948, _36950] : [-(cB(_36948)), _36950 = _36948, cB(_36950)], (120 ^ _33547) ^ [_37243, _37245] : [-(cowlNothing(_37243)), _37245 = _37243, cowlNothing(_37245)], (130 ^ _33547) ^ [_37538, _37540] : [-(cowlThing(_37538)), _37540 = _37538, cowlThing(_37540)], (140 ^ _33547) ^ [_37833, _37835] : [-(xsd_integer(_37833)), _37835 = _37833, xsd_integer(_37835)], (150 ^ _33547) ^ [_38128, _38130] : [-(xsd_string(_38128)), _38130 = _38128, xsd_string(_38130)], (160 ^ _33547) ^ [_38414] : [-(cowlThing(_38414))], (162 ^ _33547) ^ [_38456] : [cowlNothing(_38456)], (164 ^ _33547) ^ [_38579] : [xsd_string(_38579), xsd_integer(_38579)], (170 ^ _33547) ^ [_38732] : [-(xsd_integer(_38732)), -(xsd_string(_38732))], (176 ^ _33547) ^ [_38952] : [cA(_38952), -(_38952 = ia)], (182 ^ _33547) ^ [_39106] : [_39106 = ia, -(cA(_39106))], (218 ^ _33547) ^ [] : [-(cowlThing(ia))], (220 ^ _33547) ^ [] : [-(cowlThing(ib))], (206 ^ _33547) ^ [_39856] : [cB(_39856), -(_39856 = ib)], (212 ^ _33547) ^ [_40010] : [_40010 = ib, -(cB(_40010))], (198 ^ _33547) ^ [_39565] : [199 ^ _33547 : [(200 ^ _33547) ^ [] : [_39565 = ib], (202 ^ _33547) ^ [] : [_39565 = ia]], -(cA_and_B(_39565))], (188 ^ _33547) ^ [_39325] : [cA_and_B(_39325), -(_39325 = ib), -(_39325 = ia)]], input).
% 0.33/1.37 ncf('1',plain,[cowlNothing(223 ^ [])],start(162 ^ 0,bind([[_38456], [223 ^ []]]))).
% 0.33/1.37 ncf('1.1',plain,[-(cowlNothing(223 ^ [])), cowlThing(223 ^ []), 236 : -(xsd_string(232 ^ [])), 240 : xsd_integer(232 ^ []), 247 : -(cA_and_B(243 ^ [])), 253 : -(cB(243 ^ [])), 253 : -(cA(243 ^ []))],extension(222 ^ 1)).
% 0.33/1.37 ncf('1.1.1',plain,[-(cowlThing(223 ^ []))],extension(160 ^ 2,bind([[_38414], [223 ^ []]]))).
% 0.33/1.37 ncf('1.1.2',plain,[xsd_string(232 ^ []), -(xsd_string(232 ^ [])), 232 ^ [] = 232 ^ []],extension(40 ^ 4,bind([[_34885, _34887], [232 ^ [], 232 ^ []]]))).
% 0.33/1.37 ncf('1.1.2.1',plain,[xsd_string(232 ^ []), xsd_integer(232 ^ [])],extension(164 ^ 5,bind([[_38579], [232 ^ []]]))).
% 0.33/1.37 ncf('1.1.2.1.1',plain,[-(xsd_integer(232 ^ []))],extension(238 ^ 6)).
% 0.33/1.37 ncf('1.1.2.2',plain,[-(232 ^ [] = 232 ^ [])],extension(2 ^ 5,bind([[_33671], [232 ^ []]]))).
% 0.33/1.37 ncf('1.1.3',plain,[-(xsd_integer(232 ^ [])), -(xsd_string(232 ^ []))],extension(170 ^ 4,bind([[_38732], [232 ^ []]]))).
% 0.33/1.37 ncf('1.1.3.1',plain,[xsd_string(232 ^ [])],extension(242 ^ 5)).
% 0.33/1.37 ncf('1.1.4',plain,[cA_and_B(243 ^ []), -(243 ^ [] = ib), -(243 ^ [] = ia)],extension(188 ^ 4,bind([[_39325], [243 ^ []]]))).
% 0.33/1.37 ncf('1.1.4.1',plain,[243 ^ [] = ib, -(cB(243 ^ []))],extension(212 ^ 5,bind([[_40010], [243 ^ []]]))).
% 0.33/1.37 ncf('1.1.4.1.1',plain,[cB(243 ^ [])],extension(249 ^ 6)).
% 0.33/1.37 ncf('1.1.4.2',plain,[243 ^ [] = ia, -(cA(243 ^ []))],extension(182 ^ 5,bind([[_39106], [243 ^ []]]))).
% 0.33/1.37 ncf('1.1.4.2.1',plain,[cA(243 ^ [])],extension(251 ^ 6)).
% 0.33/1.37 ncf('1.1.5',plain,[cB(243 ^ []), -(243 ^ [] = ib)],extension(206 ^ 4,bind([[_39856], [243 ^ []]]))).
% 0.33/1.37 ncf('1.1.5.1',plain,[243 ^ [] = ib, -(cA_and_B(243 ^ []))],extension(198 ^ 5,bind([[_39565], [243 ^ []]]))).
% 0.33/1.37 ncf('1.1.5.1.1',plain,[cA_and_B(243 ^ [])],extension(259 ^ 6)).
% 0.33/1.37 ncf('1.1.6',plain,[cA(243 ^ []), -(243 ^ [] = ia)],extension(176 ^ 4,bind([[_38952], [243 ^ []]]))).
% 0.33/1.37 ncf('1.1.6.1',plain,[243 ^ [] = ia, -(cA_and_B(243 ^ []))],extension(198 ^ 5,bind([[_39565], [243 ^ []]]))).
% 0.33/1.37 ncf('1.1.6.1.1',plain,[cA_and_B(243 ^ [])],extension(259 ^ 6)).
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------