%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU155+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n014.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 12:02:25 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.07/0.12 % Problem : SEU155+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n014.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 13:37:12 EDT 2023
% 0.13/0.33 % 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, [(134 ^ _18214) ^ [] : [-(in(131 ^ [], 132 ^ []))], (136 ^ _18214) ^ [] : [subset(131 ^ [], union(132 ^ []))], (48 ^ _18214) ^ [_19838, _19840] : [_19840 = _19838, -(union(_19840) = union(_19838))], (2 ^ _18214) ^ [_18358] : [-(_18358 = _18358)], (4 ^ _18214) ^ [_18465, _18467] : [_18467 = _18465, -(_18465 = _18467)], (10 ^ _18214) ^ [_18669, _18671, _18673] : [-(_18673 = _18669), _18673 = _18671, _18671 = _18669], (20 ^ _18214) ^ [_19010, _19012, _19014, _19016] : [-(in(_19014, _19010)), in(_19016, _19012), _19016 = _19014, _19012 = _19010], (34 ^ _18214) ^ [_19434, _19436, _19438, _19440] : [-(subset(_19438, _19434)), subset(_19440, _19436), _19440 = _19438, _19436 = _19434], (54 ^ _18214) ^ [_20058, _20060] : [in(_20060, _20058), in(_20058, _20060)], (70 ^ _18214) ^ [_20612, _20614] : [72 ^ _18214 : [(73 ^ _18214) ^ [] : [-(in(71 ^ [_20612, _20614], _20614))], (75 ^ _18214) ^ [] : [in(71 ^ [_20612, _20614], _20612)]], -(subset(_20614, _20612))], (60 ^ _18214) ^ [_20298, _20300] : [subset(_20300, _20298), 63 ^ _18214 : [(64 ^ _18214) ^ [_20435] : [in(_20435, _20300), -(in(_20435, _20298))]]], (130 ^ _18214) ^ [_22774, _22776] : [-(subset(_22776, _22776))], (124 ^ _18214) ^ [] : [true___, -(true___)], (102 ^ _18214) ^ [_21843, _21845] : [-(_21843 = union(_21845)), 115 ^ _18214 : [(116 ^ _18214) ^ [] : [-(in(103 ^ [_21843, _21845], 114 ^ [_21843, _21845]))], (118 ^ _18214) ^ [] : [-(in(114 ^ [_21843, _21845], _21845))], (120 ^ _18214) ^ [] : [in(103 ^ [_21843, _21845], _21843)]], 106 ^ _18214 : [(107 ^ _18214) ^ [] : [-(in(103 ^ [_21843, _21845], _21843))], (109 ^ _18214) ^ [_22126] : [in(103 ^ [_21843, _21845], _22126), in(_22126, _21845)]]], (79 ^ _18214) ^ [_20998, _21000] : [_20998 = union(_21000), 82 ^ _18214 : [(83 ^ _18214) ^ [_21179] : [in(_21179, _20998), 87 ^ _18214 : [(88 ^ _18214) ^ [] : [-(in(_21179, 86 ^ [_20998, _21000, _21179]))], (90 ^ _18214) ^ [] : [-(in(86 ^ [_20998, _21000, _21179], _21000))]]], (92 ^ _18214) ^ [_21506] : [-(in(_21506, _20998)), 93 ^ _18214 : [(94 ^ _18214) ^ [_21604] : [in(_21506, _21604), in(_21604, _21000)]]]]]], input).
% 0.33/1.38 ncf('1',plain,[subset(131 ^ [], union(132 ^ []))],start(136 ^ 0)).
% 0.33/1.38 ncf('1.1',plain,[-(subset(131 ^ [], union(132 ^ []))), 75 : in(71 ^ [union(132 ^ []), 131 ^ []], union(132 ^ []))],extension(70 ^ 1,bind([[_20612, _20614], [union(132 ^ []), 131 ^ []]]))).
% 0.33/1.38 ncf('1.1.1',plain,[-(in(71 ^ [union(132 ^ []), 131 ^ []], union(132 ^ []))), 94 : in(71 ^ [union(132 ^ []), 131 ^ []], 131 ^ []), 94 : in(131 ^ [], 132 ^ []), 92 : union(132 ^ []) = union(132 ^ [])],extension(79 ^ 4,bind([[_20998, _21000, _21506, _21604], [union(132 ^ []), 132 ^ [], 71 ^ [union(132 ^ []), 131 ^ []], 131 ^ []]]))).
% 0.33/1.38 ncf('1.1.1.1',plain,[-(in(71 ^ [union(132 ^ []), 131 ^ []], 131 ^ []))],extension(73 ^ 9)).
% 0.33/1.38 ncf('1.1.1.2',plain,[-(in(131 ^ [], 132 ^ []))],extension(134 ^ 9)).
% 0.33/1.38 ncf('1.1.1.3',plain,[-(union(132 ^ []) = union(132 ^ []))],extension(2 ^ 5,bind([[_18358], [union(132 ^ [])]]))).
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------