%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS158+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:24 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 : KRS158+1 : TPTP v8.1.2. Released v3.1.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n010.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 22:53:57 EDT 2023
% 0.13/0.34 % 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, [(296 ^ _34199) ^ [] : [cowlThing(297 ^ []), -(cowlNothing(297 ^ [])), 309 ^ _34199 : [(310 ^ _34199) ^ [] : [-(xsd_string(306 ^ []))], (312 ^ _34199) ^ [] : [-(xsd_integer(306 ^ []))]], 313 ^ _34199 : [(314 ^ _34199) ^ [] : [xsd_integer(306 ^ [])], (316 ^ _34199) ^ [] : [xsd_string(306 ^ [])]], cC18(iV16560), cC14(iV16560), cC8(iV16560), cC16(iV16560), cowlThing(iV16560), cC6(iV16561), cowlThing(iV16561), cC12(iV16562), cowlThing(iV16562)], (2 ^ _34199) ^ [_34303] : [-(cowlThing(_34303))], (4 ^ _34199) ^ [_34345] : [cowlNothing(_34345)], (6 ^ _34199) ^ [_34468] : [xsd_string(_34468), xsd_integer(_34468)], (12 ^ _34199) ^ [_34621] : [-(xsd_integer(_34621)), -(xsd_string(_34621))], (18 ^ _34199) ^ [_34841] : [cC10(_34841), -(ra_Px3(_34841, 21 ^ [_34841]))], (25 ^ _34199) ^ [_35046] : [26 ^ _34199 : [(27 ^ _34199) ^ [_35113] : [ra_Px3(_35046, _35113)]], -(cC10(_35046))], (31 ^ _34199) ^ [_35287] : [cC10(_35287), 35 ^ _34199 : [(36 ^ _34199) ^ [] : [-(rR1(_35287, 34 ^ [_35287]))], (38 ^ _34199) ^ [] : [-(cC2xcomp(34 ^ [_35287]))]]], (40 ^ _34199) ^ [_35573] : [-(cC10(_35573)), 41 ^ _34199 : [(42 ^ _34199) ^ [_35661] : [rR1(_35573, _35661), cC2xcomp(_35661)]]], (50 ^ _34199) ^ [_35935] : [cC10xcomp(_35935), 53 ^ _34199 : [(54 ^ _34199) ^ [_36046] : [ra_Px3(_35935, _36046)]]], (56 ^ _34199) ^ [_36112] : [-(ra_Px3(_36112, 57 ^ [_36112])), -(cC10xcomp(_36112))], (63 ^ _34199) ^ [_36385] : [cC12(_36385), 66 ^ _34199 : [(67 ^ _34199) ^ [] : [-(cC10xcomp(_36385))], (69 ^ _34199) ^ [] : [-(cC2xcomp(_36385))]]], (71 ^ _34199) ^ [_36608] : [-(cC12(_36608)), cC10xcomp(_36608), cC2xcomp(_36608)], (81 ^ _34199) ^ [_36908] : [cC14(_36908), 85 ^ _34199 : [(86 ^ _34199) ^ [] : [-(rR1(_36908, 84 ^ [_36908]))], (88 ^ _34199) ^ [] : [-(cC12(84 ^ [_36908]))]]], (90 ^ _34199) ^ [_37194] : [-(cC14(_37194)), 91 ^ _34199 : [(92 ^ _34199) ^ [_37282] : [rR1(_37194, _37282), cC12(_37282)]]], (100 ^ _34199) ^ [_37556] : [cC16(_37556), 103 ^ _34199 : [(104 ^ _34199) ^ [] : [-(cC14(_37556))], (106 ^ _34199) ^ [] : [-(cC8(_37556))]]], (108 ^ _34199) ^ [_37779] : [-(cC16(_37779)), cC14(_37779), cC8(_37779)], (118 ^ _34199) ^ [_38079] : [cC18(_38079), 121 ^ _34199 : [(122 ^ _34199) ^ [] : [-(cTOP(_38079))], (124 ^ _34199) ^ [] : [-(cC16(_38079))]]], (126 ^ _34199) ^ [_38302] : [-(cC18(_38302)), cTOP(_38302), cC16(_38302)], (136 ^ _34199) ^ [_38602] : [cC2(_38602), 139 ^ _34199 : [(140 ^ _34199) ^ [_38713] : [ra_Px1(_38602, _38713)]]], (142 ^ _34199) ^ [_38779] : [-(ra_Px1(_38779, 143 ^ [_38779])), -(cC2(_38779))], (149 ^ _34199) ^ [_39052] : [cC2xcomp(_39052), -(ra_Px1(_39052, 152 ^ [_39052]))], (156 ^ _34199) ^ [_39257] : [157 ^ _34199 : [(158 ^ _34199) ^ [_39324] : [ra_Px1(_39257, _39324)]], -(cC2xcomp(_39257))], (162 ^ _34199) ^ [_39498] : [cC4(_39498), -(ra_Px6(_39498, 165 ^ [_39498]))], (169 ^ _34199) ^ [_39703] : [170 ^ _34199 : [(171 ^ _34199) ^ [_39770] : [ra_Px6(_39703, _39770)]], -(cC4(_39703))], (175 ^ _34199) ^ [_39944] : [cC4(_39944), 179 ^ _34199 : [(180 ^ _34199) ^ [] : [-(rR1(_39944, 178 ^ [_39944]))], (182 ^ _34199) ^ [] : [-(cC2xcomp(178 ^ [_39944]))]]], (184 ^ _34199) ^ [_40230] : [-(cC4(_40230)), 185 ^ _34199 : [(186 ^ _34199) ^ [_40318] : [rR1(_40230, _40318), cC2xcomp(_40318)]]], (194 ^ _34199) ^ [_40592] : [cC4xcomp(_40592), 197 ^ _34199 : [(198 ^ _34199) ^ [_40703] : [ra_Px6(_40592, _40703)]]], (200 ^ _34199) ^ [_40769] : [-(ra_Px6(_40769, 201 ^ [_40769])), -(cC4xcomp(_40769))], (207 ^ _34199) ^ [_41042] : [cC6(_41042), 210 ^ _34199 : [(211 ^ _34199) ^ [] : [-(cC4xcomp(_41042))], (213 ^ _34199) ^ [] : [-(cC2xcomp(_41042))]]], (215 ^ _34199) ^ [_41265] : [-(cC6(_41265)), cC4xcomp(_41265), cC2xcomp(_41265)], (225 ^ _34199) ^ [_41565] : [cC8(_41565), 229 ^ _34199 : [(230 ^ _34199) ^ [] : [-(rR1(_41565, 228 ^ [_41565]))], (232 ^ _34199) ^ [] : [-(cC6(228 ^ [_41565]))]]], (234 ^ _34199) ^ [_41851] : [-(cC8(_41851)), 235 ^ _34199 : [(236 ^ _34199) ^ [_41939] : [rR1(_41851, _41939), cC6(_41939)]]], (262 ^ _34199) ^ [] : [-(cowlThing(iV16560))], (264 ^ _34199) ^ [] : [-(cTEST(iV16560))], (266 ^ _34199) ^ [] : [-(cTOP(iV16560))], (268 ^ _34199) ^ [] : [-(rR1(iV16560, iV16562))], (270 ^ _34199) ^ [] : [-(rR1(iV16560, iV16561))], (272 ^ _34199) ^ [] : [-(cowlThing(iV16561))], (274 ^ _34199) ^ [_43025] : [rR1(iV16561, _43025), -(cC2(_43025))], (280 ^ _34199) ^ [] : [-(cC4xcomp(iV16561))], (282 ^ _34199) ^ [] : [-(cC2xcomp(iV16561))], (284 ^ _34199) ^ [] : [-(cowlThing(iV16562))], (292 ^ _34199) ^ [] : [-(cC10xcomp(iV16562))], (294 ^ _34199) ^ [] : [-(cC2xcomp(iV16562))], (286 ^ _34199) ^ [_43372] : [rR1(iV16562, _43372), -(cC2(_43372))], (244 ^ _34199) ^ [_42213] : [cTEST(_42213), 247 ^ _34199 : [(248 ^ _34199) ^ [] : [-(cTOP(_42213))], (250 ^ _34199) ^ [] : [-(cC18(_42213))]]], (252 ^ _34199) ^ [_42436] : [-(cTEST(_42436)), cTOP(_42436), cC18(_42436)]], input).
% 0.33/1.38 ncf('1',plain,[cowlNothing(297 ^ [])],start(4 ^ 0,bind([[_34345], [297 ^ []]]))).
% 0.33/1.38 ncf('1.1',plain,[-(cowlNothing(297 ^ [])), cowlThing(297 ^ []), 310 : -(xsd_string(306 ^ [])), 314 : xsd_integer(306 ^ []), 314 : cC18(iV16560), 314 : cC14(iV16560), 314 : cC8(iV16560), 314 : cC16(iV16560), 314 : cowlThing(iV16560), 314 : cC6(iV16561), 314 : cowlThing(iV16561), 314 : cC12(iV16562), 314 : cowlThing(iV16562)],extension(296 ^ 1)).
% 0.33/1.38 ncf('1.1.1',plain,[-(cowlThing(297 ^ []))],extension(2 ^ 2,bind([[_34303], [297 ^ []]]))).
% 0.33/1.38 ncf('1.1.2',plain,[xsd_string(306 ^ []), xsd_integer(306 ^ [])],extension(6 ^ 4,bind([[_34468], [306 ^ []]]))).
% 0.33/1.38 ncf('1.1.2.1',plain,[-(xsd_integer(306 ^ []))],extension(312 ^ 5)).
% 0.33/1.38 ncf('1.1.3',plain,[-(xsd_integer(306 ^ [])), -(xsd_string(306 ^ []))],extension(12 ^ 4,bind([[_34621], [306 ^ []]]))).
% 0.33/1.38 ncf('1.1.3.1',plain,[xsd_string(306 ^ [])],extension(316 ^ 5)).
% 0.33/1.38 ncf('1.1.4',plain,[-(cC18(iV16560)), cTEST(iV16560)],extension(244 ^ 2,bind([[_42213], [iV16560]]))).
% 0.33/1.38 ncf('1.1.4.1',plain,[-(cTEST(iV16560))],extension(264 ^ 3)).
% 0.33/1.38 ncf('1.1.5',plain,[-(cC14(iV16560)), 92 : rR1(iV16560, iV16562), 92 : cC12(iV16562)],extension(90 ^ 2,bind([[_37194, _37282], [iV16560, iV16562]]))).
% 0.33/1.38 ncf('1.1.5.1',plain,[-(rR1(iV16560, iV16562))],extension(268 ^ 5)).
% 0.33/1.38 ncf('1.1.5.2',plain,[-(cC12(iV16562)), cC10xcomp(iV16562), cC2xcomp(iV16562)],extension(71 ^ 5,bind([[_36608], [iV16562]]))).
% 0.33/1.38 ncf('1.1.5.2.1',plain,[-(cC10xcomp(iV16562))],extension(292 ^ 6)).
% 0.33/1.38 ncf('1.1.5.2.2',plain,[-(cC2xcomp(iV16562))],extension(294 ^ 6)).
% 0.33/1.38 ncf('1.1.6',plain,[-(cC8(iV16560)), cC16(iV16560)],extension(100 ^ 2,bind([[_37556], [iV16560]]))).
% 0.33/1.38 ncf('1.1.6.1',plain,[-(cC16(iV16560)), cC18(iV16560)],extension(118 ^ 3,bind([[_38079], [iV16560]]))).
% 0.33/1.38 ncf('1.1.6.1.1',plain,[-(cC18(iV16560))],lemmata('[1].x')).
% 0.33/1.38 ncf('1.1.7',plain,[-(cC16(iV16560)), cC14(iV16560), cC8(iV16560)],extension(108 ^ 2,bind([[_37779], [iV16560]]))).
% 0.33/1.38 ncf('1.1.7.1',plain,[-(cC14(iV16560))],lemmata('[1].x')).
% 0.33/1.38 ncf('1.1.7.2',plain,[-(cC8(iV16560))],lemmata('[1].x')).
% 0.33/1.38 ncf('1.1.8',plain,[-(cowlThing(iV16560))],extension(2 ^ 2,bind([[_34303], [iV16560]]))).
% 0.33/1.38 ncf('1.1.9',plain,[-(cC6(iV16561)), cC4xcomp(iV16561), cC2xcomp(iV16561)],extension(215 ^ 2,bind([[_41265], [iV16561]]))).
% 0.33/1.38 ncf('1.1.9.1',plain,[-(cC4xcomp(iV16561))],extension(280 ^ 3)).
% 0.33/1.38 ncf('1.1.9.2',plain,[-(cC2xcomp(iV16561))],extension(282 ^ 3)).
% 0.33/1.38 ncf('1.1.10',plain,[-(cowlThing(iV16561))],extension(2 ^ 2,bind([[_34303], [iV16561]]))).
% 0.33/1.38 ncf('1.1.11',plain,[-(cC12(iV16562)), cC10xcomp(iV16562), cC2xcomp(iV16562)],extension(71 ^ 2,bind([[_36608], [iV16562]]))).
% 0.33/1.38 ncf('1.1.11.1',plain,[-(cC10xcomp(iV16562))],extension(292 ^ 3)).
% 0.33/1.38 ncf('1.1.11.2',plain,[-(cC2xcomp(iV16562))],extension(294 ^ 3)).
% 0.33/1.38 ncf('1.1.12',plain,[-(cowlThing(iV16562))],extension(2 ^ 2,bind([[_34303], [iV16562]]))).
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------