%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS175+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n027.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.34s 1.37s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS175+1 : TPTP v8.1.2. Released v3.1.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n027.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:21:05 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.34/1.37
% 0.34/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.34/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 ncf(matrix, plain, [(222 ^ _34493) ^ [] : [cowlThing(223 ^ []), -(cowlNothing(223 ^ [])), 235 ^ _34493 : [(236 ^ _34493) ^ [] : [-(xsd_string(232 ^ []))], (238 ^ _34493) ^ [] : [-(xsd_integer(232 ^ []))]], 239 ^ _34493 : [(240 ^ _34493) ^ [] : [xsd_integer(232 ^ [])], (242 ^ _34493) ^ [] : [xsd_string(232 ^ [])]], cowlThing(ia), cowlThing(ib), 248 ^ _34493 : [(249 ^ _34493) ^ [] : [-(cA_and_B(245 ^ []))], (251 ^ _34493) ^ [] : [245 ^ [] = ib], (253 ^ _34493) ^ [] : [245 ^ [] = ia]], 254 ^ _34493 : [(261 ^ _34493) ^ [] : [cA_and_B(245 ^ [])], (255 ^ _34493) ^ [] : [-(245 ^ [] = ib), -(245 ^ [] = ia)]]], (2 ^ _34493) ^ [_34617] : [-(_34617 = _34617)], (4 ^ _34493) ^ [_34724, _34726] : [_34726 = _34724, -(_34724 = _34726)], (10 ^ _34493) ^ [_34928, _34930, _34932] : [-(_34932 = _34928), _34932 = _34930, _34930 = _34928], (20 ^ _34493) ^ [_35241, _35243] : [-(cA(_35241)), _35243 = _35241, cA(_35243)], (30 ^ _34493) ^ [_35536, _35538] : [-(cB(_35536)), _35538 = _35536, cB(_35538)], (40 ^ _34493) ^ [_35831, _35833] : [-(cowlNothing(_35831)), _35833 = _35831, cowlNothing(_35833)], (50 ^ _34493) ^ [_36126, _36128] : [-(xsd_string(_36126)), _36128 = _36126, xsd_string(_36128)], (60 ^ _34493) ^ [_36421, _36423] : [-(xsd_integer(_36421)), _36423 = _36421, xsd_integer(_36423)], (70 ^ _34493) ^ [_36716, _36718] : [-(cA_and_B(_36716)), _36718 = _36716, cA_and_B(_36718)], (80 ^ _34493) ^ [_36991, _36993] : [-(cowlThing(_36991)), _36993 = _36991, cowlThing(_36993)], (90 ^ _34493) ^ [_37304, _37306] : [-(cA(_37304)), _37306 = _37304, cA(_37306)], (100 ^ _34493) ^ [_37599, _37601] : [-(cA_and_B(_37599)), _37601 = _37599, cA_and_B(_37601)], (110 ^ _34493) ^ [_37894, _37896] : [-(cB(_37894)), _37896 = _37894, cB(_37896)], (120 ^ _34493) ^ [_38189, _38191] : [-(cowlNothing(_38189)), _38191 = _38189, cowlNothing(_38191)], (130 ^ _34493) ^ [_38484, _38486] : [-(cowlThing(_38484)), _38486 = _38484, cowlThing(_38486)], (140 ^ _34493) ^ [_38779, _38781] : [-(xsd_integer(_38779)), _38781 = _38779, xsd_integer(_38781)], (150 ^ _34493) ^ [_39074, _39076] : [-(xsd_string(_39074)), _39076 = _39074, xsd_string(_39076)], (160 ^ _34493) ^ [_39360] : [-(cowlThing(_39360))], (162 ^ _34493) ^ [_39402] : [cowlNothing(_39402)], (164 ^ _34493) ^ [_39525] : [xsd_string(_39525), xsd_integer(_39525)], (170 ^ _34493) ^ [_39678] : [-(xsd_integer(_39678)), -(xsd_string(_39678))], (176 ^ _34493) ^ [_39898] : [cA(_39898), -(_39898 = ia)], (182 ^ _34493) ^ [_40052] : [_40052 = ia, -(cA(_40052))], (218 ^ _34493) ^ [] : [-(cowlThing(ia))], (220 ^ _34493) ^ [] : [-(cowlThing(ib))], (206 ^ _34493) ^ [_40794] : [cB(_40794), -(_40794 = ib)], (212 ^ _34493) ^ [_40948] : [_40948 = ib, -(cB(_40948))], (198 ^ _34493) ^ [_40507] : [199 ^ _34493 : [(200 ^ _34493) ^ [] : [cA(_40507)], (202 ^ _34493) ^ [] : [cB(_40507)]], -(cA_and_B(_40507))], (188 ^ _34493) ^ [_40271] : [cA_and_B(_40271), -(cA(_40271)), -(cB(_40271))]], input).
% 0.34/1.37 ncf('1',plain,[cowlNothing(223 ^ [])],start(162 ^ 0,bind([[_39402], [223 ^ []]]))).
% 0.34/1.37 ncf('1.1',plain,[-(cowlNothing(223 ^ [])), cowlThing(223 ^ []), 236 : -(xsd_string(232 ^ [])), 240 : xsd_integer(232 ^ []), 240 : cowlThing(ia), 240 : cowlThing(ib), 249 : -(cA_and_B(245 ^ [])), 255 : -(245 ^ [] = ib), 255 : -(245 ^ [] = ia)],extension(222 ^ 1)).
% 0.34/1.37 ncf('1.1.1',plain,[-(cowlThing(223 ^ []))],extension(160 ^ 2,bind([[_39360], [223 ^ []]]))).
% 0.34/1.37 ncf('1.1.2',plain,[xsd_string(232 ^ []), -(xsd_string(232 ^ [])), 232 ^ [] = 232 ^ []],extension(50 ^ 4,bind([[_36126, _36128], [232 ^ [], 232 ^ []]]))).
% 0.34/1.37 ncf('1.1.2.1',plain,[xsd_string(232 ^ []), xsd_integer(232 ^ [])],extension(164 ^ 5,bind([[_39525], [232 ^ []]]))).
% 0.34/1.37 ncf('1.1.2.1.1',plain,[-(xsd_integer(232 ^ []))],extension(238 ^ 6)).
% 0.34/1.37 ncf('1.1.2.2',plain,[-(232 ^ [] = 232 ^ [])],extension(2 ^ 5,bind([[_34617], [232 ^ []]]))).
% 0.34/1.37 ncf('1.1.3',plain,[-(xsd_integer(232 ^ [])), -(xsd_string(232 ^ []))],extension(170 ^ 4,bind([[_39678], [232 ^ []]]))).
% 0.34/1.37 ncf('1.1.3.1',plain,[xsd_string(232 ^ [])],extension(242 ^ 5)).
% 0.34/1.37 ncf('1.1.4',plain,[-(cowlThing(ia))],extension(160 ^ 2,bind([[_39360], [ia]]))).
% 0.34/1.37 ncf('1.1.5',plain,[-(cowlThing(ib))],extension(160 ^ 2,bind([[_39360], [ib]]))).
% 0.34/1.37 ncf('1.1.6',plain,[cA_and_B(245 ^ []), -(cA(245 ^ [])), -(cB(245 ^ []))],extension(188 ^ 4,bind([[_40271], [245 ^ []]]))).
% 0.34/1.37 ncf('1.1.6.1',plain,[cA(245 ^ []), -(245 ^ [] = ia)],extension(176 ^ 5,bind([[_39898], [245 ^ []]]))).
% 0.34/1.37 ncf('1.1.6.1.1',plain,[245 ^ [] = ia],extension(253 ^ 6)).
% 0.34/1.37 ncf('1.1.6.2',plain,[cB(245 ^ []), -(245 ^ [] = ib)],extension(206 ^ 5,bind([[_40794], [245 ^ []]]))).
% 0.34/1.37 ncf('1.1.6.2.1',plain,[245 ^ [] = ib],extension(251 ^ 6)).
% 0.34/1.37 ncf('1.1.7',plain,[245 ^ [] = ib, -(cB(245 ^ []))],extension(212 ^ 4,bind([[_40948], [245 ^ []]]))).
% 0.34/1.37 ncf('1.1.7.1',plain,[cB(245 ^ []), -(cA_and_B(245 ^ []))],extension(198 ^ 5,bind([[_40507], [245 ^ []]]))).
% 0.34/1.37 ncf('1.1.7.1.1',plain,[cA_and_B(245 ^ [])],extension(261 ^ 6)).
% 0.34/1.37 ncf('1.1.8',plain,[245 ^ [] = ia, -(cA(245 ^ []))],extension(182 ^ 4,bind([[_40052], [245 ^ []]]))).
% 0.34/1.37 ncf('1.1.8.1',plain,[cA(245 ^ []), -(cA_and_B(245 ^ []))],extension(198 ^ 5,bind([[_40507], [245 ^ []]]))).
% 0.34/1.37 ncf('1.1.8.1.1',plain,[cA_and_B(245 ^ [])],extension(261 ^ 6)).
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------