%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS180+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n025.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.38s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS180+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n025.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:11:03 EDT 2023
% 0.12/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, [(194 ^ _30905) ^ [_38560, _38562] : [-(status(_38562, _38560, 191 ^ []))], (196 ^ _30905) ^ [_38627, _38629] : [-(isa(191 ^ [], 192 ^ []))], (198 ^ _30905) ^ [_38682, _38684] : [-(nota(191 ^ [], 192 ^ [])), -(nevera(191 ^ [], 192 ^ [])), -(xora(191 ^ [], 192 ^ []))], (12 ^ _30905) ^ [_31392, _31394] : [mighta(_31394, _31392), 17 ^ _30905 : [(18 ^ _30905) ^ [] : [-(status(15 ^ [_31392, _31394], 16 ^ [_31392, _31394], _31394))], (20 ^ _30905) ^ [] : [-(status(15 ^ [_31392, _31394], 16 ^ [_31392, _31394], _31392))]]], (2 ^ _30905) ^ [_31047, _31049] : [-(mighta(_31049, _31047)), 3 ^ _30905 : [(4 ^ _30905) ^ [_31160, _31162] : [status(_31162, _31160, _31049), status(_31162, _31160, _31047)]]], (22 ^ _30905) ^ [_31875, _31877] : [25 ^ _30905 : [(26 ^ _30905) ^ [] : [-(status(23 ^ [_31875, _31877], 24 ^ [_31875, _31877], _31877))], (28 ^ _30905) ^ [] : [status(23 ^ [_31875, _31877], 24 ^ [_31875, _31877], _31875)]], -(isa(_31877, _31875))], (32 ^ _30905) ^ [_32279, _32281] : [isa(_32281, _32279), 35 ^ _30905 : [(36 ^ _30905) ^ [_32437, _32439] : [status(_32439, _32437, _32281), -(status(_32439, _32437, _32279))]]], (52 ^ _30905) ^ [_33053, _33055] : [nota(_33055, _33053), 57 ^ _30905 : [(58 ^ _30905) ^ [] : [-(status(55 ^ [_33053, _33055], 56 ^ [_33053, _33055], _33055))], (60 ^ _30905) ^ [] : [status(55 ^ [_33053, _33055], 56 ^ [_33053, _33055], _33053)]]], (42 ^ _30905) ^ [_32703, _32705] : [-(nota(_32705, _32703)), 43 ^ _30905 : [(44 ^ _30905) ^ [_32818, _32820] : [status(_32820, _32818, _32705), -(status(_32820, _32818, _32703))]]], (62 ^ _30905) ^ [_33541, _33543] : [65 ^ _30905 : [(66 ^ _30905) ^ [] : [-(status(63 ^ [_33541, _33543], 64 ^ [_33541, _33543], _33543))], (68 ^ _30905) ^ [] : [-(status(63 ^ [_33541, _33543], 64 ^ [_33541, _33543], _33541))]], -(nevera(_33543, _33541))], (72 ^ _30905) ^ [_33952, _33954] : [nevera(_33954, _33952), 75 ^ _30905 : [(76 ^ _30905) ^ [_34112, _34114] : [status(_34114, _34112, _33954), status(_34114, _34112, _33952)]]], (100 ^ _30905) ^ [_34995, _34997] : [xora(_34997, _34995), 103 ^ _30905 : [(104 ^ _30905) ^ [_35164, _35166] : [105 ^ _30905 : [(106 ^ _30905) ^ [] : [-(status(_35166, _35164, _34997))], (108 ^ _30905) ^ [] : [status(_35166, _35164, _34995)]], 109 ^ _30905 : [(110 ^ _30905) ^ [] : [-(status(_35166, _35164, _34995))], (112 ^ _30905) ^ [] : [status(_35166, _35164, _34997)]]]]], (82 ^ _30905) ^ [_34379, _34381] : [-(xora(_34381, _34379)), 85 ^ _30905 : [(86 ^ _30905) ^ [] : [status(83 ^ [_34379, _34381], 84 ^ [_34379, _34381], _34381), -(status(83 ^ [_34379, _34381], 84 ^ [_34379, _34381], _34379))], (92 ^ _30905) ^ [] : [status(83 ^ [_34379, _34381], 84 ^ [_34379, _34381], _34379), -(status(83 ^ [_34379, _34381], 84 ^ [_34379, _34381], _34381))]]], (114 ^ _30905) ^ [_35571, _35573] : [115 ^ _30905 : [(116 ^ _30905) ^ [] : [-(model(_35573, _35571))], (118 ^ _30905) ^ [] : [model(_35573, not _35571)]], 119 ^ _30905 : [(120 ^ _30905) ^ [] : [-(model(_35573, not _35571))], (122 ^ _30905) ^ [] : [model(_35573, _35571)]]], (124 ^ _30905) ^ [_35967, _35969] : [model(_35969, _35967), model(_35969, not _35967)], (130 ^ _30905) ^ [_36134, _36136] : [-(model(_36136, not _36134)), -(model(_36136, _36134))], (137 ^ _30905) ^ [_36366] : [-(model(_36366, 135 ^ []))], (141 ^ _30905) ^ [] : [-(model(139 ^ [], 138 ^ []))], (144 ^ _30905) ^ [] : [model(142 ^ [], 138 ^ [])], (147 ^ _30905) ^ [_36725] : [model(_36725, 145 ^ [])], (152 ^ _30905) ^ [] : [-(model(150 ^ [], 148 ^ []))], (154 ^ _30905) ^ [] : [-(model(150 ^ [], 149 ^ []))], (157 ^ _30905) ^ [] : [model(155 ^ [], 148 ^ []), model(155 ^ [], 149 ^ [])], (185 ^ _30905) ^ [] : [-(model(181 ^ [], 182 ^ []))], (187 ^ _30905) ^ [] : [model(181 ^ [], 183 ^ [])], (190 ^ _30905) ^ [] : [-(model(188 ^ [], 183 ^ []))], (166 ^ _30905) ^ [] : [-(model(164 ^ [], 162 ^ []))], (175 ^ _30905) ^ [] : [model(173 ^ [], 162 ^ [])], (177 ^ _30905) ^ [] : [-(model(173 ^ [], 163 ^ []))], (180 ^ _30905) ^ [] : [model(178 ^ [], 163 ^ [])], (168 ^ _30905) ^ [_37578] : [model(_37578, 162 ^ []), -(model(_37578, 163 ^ []))]], input).
% 0.33/1.38 ncf('1',plain,[nota(191 ^ [], 192 ^ []), 60 : status(55 ^ [192 ^ [], 191 ^ []], 56 ^ [192 ^ [], 191 ^ []], 192 ^ [])],start(52 ^ 0,bind([[_33053, _33055], [192 ^ [], 191 ^ []]]))).
% 0.33/1.38 ncf('1.1',plain,[-(nota(191 ^ [], 192 ^ [])), -(nevera(191 ^ [], 192 ^ [])), -(xora(191 ^ [], 192 ^ []))],extension(198 ^ 1,bind([[_38682, _38684], [_21602, _21604]]))).
% 0.33/1.38 ncf('1.1.1',plain,[nevera(191 ^ [], 192 ^ []), 76 : status(_21771, _21769, 191 ^ []), 76 : status(_21771, _21769, 192 ^ [])],extension(72 ^ 2,bind([[_33952, _33954, _34112, _34114], [192 ^ [], 191 ^ [], _21769, _21771]]))).
% 0.33/1.38 ncf('1.1.1.1',plain,[-(status(_21771, _21769, 191 ^ []))],extension(194 ^ 5,bind([[_38560, _38562], [_21769, _21771]]))).
% 0.33/1.38 ncf('1.1.1.2',plain,[-(status(_21771, _21769, 192 ^ [])), 36 : status(_21771, _21769, 191 ^ []), 36 : isa(191 ^ [], 192 ^ [])],extension(32 ^ 5,bind([[_32279, _32281, _32437, _32439], [192 ^ [], 191 ^ [], _21769, _21771]]))).
% 0.33/1.38 ncf('1.1.1.2.1',plain,[-(status(_21771, _21769, 191 ^ []))],extension(194 ^ 8,bind([[_38560, _38562], [_21769, _21771]]))).
% 0.33/1.38 ncf('1.1.1.2.2',plain,[-(isa(191 ^ [], 192 ^ []))],extension(196 ^ 6,bind([[_38627, _38629], [_22308, _22310]]))).
% 0.33/1.38 ncf('1.1.2',plain,[xora(191 ^ [], 192 ^ []), 106 : -(status(_22455, _22453, 191 ^ [])), 112 : status(_22455, _22453, 191 ^ [])],extension(100 ^ 2,bind([[_34995, _34997, _35164, _35166], [192 ^ [], 191 ^ [], _22453, _22455]]))).
% 0.33/1.38 ncf('1.1.2.1',plain,[status(_22455, _22453, 191 ^ []), 36 : -(status(_22455, _22453, 192 ^ [])), 36 : isa(191 ^ [], 192 ^ [])],extension(32 ^ 7,bind([[_32279, _32281, _32437, _32439], [192 ^ [], 191 ^ [], _22453, _22455]]))).
% 0.33/1.38 ncf('1.1.2.1.1',plain,[status(_22455, _22453, 192 ^ [])],extension(108 ^ 10)).
% 0.33/1.38 ncf('1.1.2.1.2',plain,[-(isa(191 ^ [], 192 ^ []))],extension(196 ^ 8,bind([[_38627, _38629], [_23407, _23409]]))).
% 0.33/1.38 ncf('1.1.2.2',plain,[-(status(_22455, _22453, 191 ^ []))],extension(194 ^ 7,bind([[_38560, _38562], [_22453, _22455]]))).
% 0.33/1.38 ncf('1.2',plain,[-(status(55 ^ [192 ^ [], 191 ^ []], 56 ^ [192 ^ [], 191 ^ []], 192 ^ [])), 36 : status(55 ^ [192 ^ [], 191 ^ []], 56 ^ [192 ^ [], 191 ^ []], 191 ^ []), 36 : isa(191 ^ [], 192 ^ [])],extension(32 ^ 3,bind([[_32279, _32281, _32437, _32439], [192 ^ [], 191 ^ [], 56 ^ [192 ^ [], 191 ^ []], 55 ^ [192 ^ [], 191 ^ []]]]))).
% 0.33/1.38 ncf('1.2.1',plain,[-(status(55 ^ [192 ^ [], 191 ^ []], 56 ^ [192 ^ [], 191 ^ []], 191 ^ []))],extension(194 ^ 6,bind([[_38560, _38562], [56 ^ [192 ^ [], 191 ^ []], 55 ^ [192 ^ [], 191 ^ []]]]))).
% 0.33/1.38 ncf('1.2.2',plain,[-(isa(191 ^ [], 192 ^ []))],extension(196 ^ 4,bind([[_38627, _38629], [_23941, _23943]]))).
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------