%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM836+1 : TPTP v8.1.2. Released v4.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:45:43 EDT 2023
% Result : Theorem 0.36s 1.37s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : NUM836+1 : TPTP v8.1.2. Released v4.1.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n010.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 16:30:12 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.36/1.37
% 0.36/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.36/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 ncf(matrix, plain, [(174 ^ _35706) ^ [] : [-(greater(vd203, vd204))], (176 ^ _35706) ^ [] : [-(less(vd203, vd204))], (48 ^ _35706) ^ [_37378, _37380, _37382, _37384] : [-(vplus(_37384, _37380) = vplus(_37382, _37378)), _37384 = _37382, _37380 = _37378], (58 ^ _35706) ^ [_37709, _37711] : [_37711 = _37709, -(vskolem2(_37711) = vskolem2(_37709))], (64 ^ _35706) ^ [_37907, _37909] : [_37909 = _37907, -(vsucc(_37909) = vsucc(_37907))], (2 ^ _35706) ^ [_35850] : [-(_35850 = _35850)], (4 ^ _35706) ^ [_35957, _35959] : [_35959 = _35957, -(_35957 = _35959)], (10 ^ _35706) ^ [_36161, _36163, _36165] : [-(_36165 = _36161), _36165 = _36163, _36163 = _36161], (20 ^ _35706) ^ [_36502, _36504, _36506, _36508] : [-(greater(_36506, _36502)), greater(_36508, _36504), _36508 = _36506, _36504 = _36502], (34 ^ _35706) ^ [_36926, _36928, _36930, _36932] : [-(less(_36930, _36926)), less(_36932, _36928), _36932 = _36930, _36928 = _36926], (70 ^ _35706) ^ [] : [vd203 = vd204, greater(vd203, vd204)], (76 ^ _35706) ^ [_38282, _38284] : [less(_38282, _38284), -(_38284 = vplus(_38282, 79 ^ [_38282, _38284]))], (83 ^ _35706) ^ [_38510, _38512] : [84 ^ _35706 : [(85 ^ _35706) ^ [_38583] : [_38512 = vplus(_38510, _38583)]], -(less(_38510, _38512))], (89 ^ _35706) ^ [_38779, _38781] : [greater(_38779, _38781), -(_38779 = vplus(_38781, 92 ^ [_38779, _38781]))], (96 ^ _35706) ^ [_39007, _39009] : [97 ^ _35706 : [(98 ^ _35706) ^ [_39080] : [_39007 = vplus(_39009, _39080)]], -(greater(_39007, _39009))], (102 ^ _35706) ^ [_39247, _39249] : [-(_39249 = _39247), -(_39249 = vplus(_39247, 107 ^ [_39247, _39249])), -(_39247 = vplus(_39249, 110 ^ [_39247, _39249]))], (114 ^ _35706) ^ [_39680, _39682] : [_39682 = _39680, 117 ^ _35706 : [(118 ^ _35706) ^ [_39802] : [_39680 = vplus(_39682, _39802)]]], (120 ^ _35706) ^ [_39921, _39923] : [121 ^ _35706 : [(122 ^ _35706) ^ [_40006] : [_39923 = vplus(_39921, _40006)]], 123 ^ _35706 : [(124 ^ _35706) ^ [_40070] : [_39921 = vplus(_39923, _40070)]]], (126 ^ _35706) ^ [_40190, _40192] : [_40192 = _40190, 129 ^ _35706 : [(130 ^ _35706) ^ [_40312] : [_40192 = vplus(_40190, _40312)]]], (132 ^ _35706) ^ [_40431, _40433] : [-(_40433 = _40431), 135 ^ _35706 : [(136 ^ _35706) ^ [_40557] : [vplus(_40557, _40433) = vplus(_40557, _40431)]]], (138 ^ _35706) ^ [_40663, _40665] : [_40663 = vplus(_40665, _40663)], (140 ^ _35706) ^ [_40760, _40762] : [-(vplus(_40760, _40762) = vplus(_40762, _40760))], (142 ^ _35706) ^ [_40860, _40862] : [-(vplus(vsucc(_40862), _40860) = vsucc(vplus(_40862, _40860)))], (144 ^ _35706) ^ [_40950] : [-(vplus(v1, _40950) = vsucc(_40950))], (146 ^ _35706) ^ [_41061, _41063, _41065] : [-(vplus(vplus(_41065, _41063), _41061) = vplus(_41065, vplus(_41063, _41061)))], (148 ^ _35706) ^ [_41189, _41191] : [-(vplus(_41191, vsucc(_41189)) = vsucc(vplus(_41191, _41189)))], (150 ^ _35706) ^ [_41245, _41247] : [-(vplus(_41247, v1) = vsucc(_41247))], (152 ^ _35706) ^ [_41347] : [-(_41347 = v1), -(_41347 = vsucc(vskolem2(_41347)))], (158 ^ _35706) ^ [_41532] : [vsucc(_41532) = _41532], (160 ^ _35706) ^ [_41641, _41643] : [-(_41643 = _41641), vsucc(_41643) = vsucc(_41641)], (172 ^ _35706) ^ [_42031] : [vsucc(_42031) = v1], (166 ^ _35706) ^ [_41863, _41865] : [vsucc(_41865) = vsucc(_41863), -(_41865 = _41863)]], input).
% 0.36/1.37 ncf('1',plain,[vd203 = vd204, greater(vd203, vd204)],start(70 ^ 0)).
% 0.36/1.37 ncf('1.1',plain,[-(vd203 = vd204), -(vd203 = vplus(vd204, 107 ^ [vd204, vd203])), -(vd204 = vplus(vd203, 110 ^ [vd204, vd203]))],extension(102 ^ 1,bind([[_39247, _39249], [vd204, vd203]]))).
% 0.36/1.37 ncf('1.1.1',plain,[vd203 = vplus(vd204, 107 ^ [vd204, vd203]), 124 : vd204 = vplus(vd203, 79 ^ [vd203, vd204])],extension(120 ^ 2,bind([[_39921, _39923, _40006, _40070], [vd204, vd203, 107 ^ [vd204, vd203], 79 ^ [vd203, vd204]]]))).
% 0.36/1.37 ncf('1.1.1.1',plain,[-(vd204 = vplus(vd203, 79 ^ [vd203, vd204])), less(vd203, vd204)],extension(76 ^ 5,bind([[_38282, _38284], [vd203, vd204]]))).
% 0.36/1.37 ncf('1.1.1.1.1',plain,[-(less(vd203, vd204))],extension(176 ^ 6)).
% 0.36/1.37 ncf('1.1.2',plain,[vd204 = vplus(vd203, 110 ^ [vd204, vd203]), 124 : vd203 = vplus(vd204, 92 ^ [vd203, vd204])],extension(120 ^ 2,bind([[_39921, _39923, _40006, _40070], [vd203, vd204, 110 ^ [vd204, vd203], 92 ^ [vd203, vd204]]]))).
% 0.36/1.37 ncf('1.1.2.1',plain,[-(vd203 = vplus(vd204, 92 ^ [vd203, vd204])), greater(vd203, vd204)],extension(89 ^ 5,bind([[_38779, _38781], [vd203, vd204]]))).
% 0.36/1.37 ncf('1.1.2.1.1',plain,[-(greater(vd203, vd204))],extension(174 ^ 6)).
% 0.36/1.37 ncf('1.2',plain,[-(greater(vd203, vd204))],extension(174 ^ 1)).
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------