%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET579+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n007.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:56:01 EDT 2023
% Result : Theorem 0.37s 1.37s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SET579+3 : TPTP v8.1.2. Released v2.2.0.
% 0.10/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n007.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 19:04:53 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.37/1.37
% 0.37/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.37/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/1.37 %-----------------------------------------------------
% 0.37/1.37 ncf(matrix, plain, [(136 ^ _20588) ^ [] : [114 ^ [] = difference(115 ^ [], 116 ^ [])], (118 ^ _20588) ^ [_24762] : [member(_24762, 114 ^ []), 121 ^ _20588 : [(122 ^ _20588) ^ [] : [-(member(_24762, 115 ^ []))], (124 ^ _20588) ^ [] : [member(_24762, 116 ^ [])]]], (126 ^ _20588) ^ [_24992] : [-(member(_24992, 114 ^ [])), member(_24992, 115 ^ []), -(member(_24992, 116 ^ []))], (58 ^ _20588) ^ [_22616, _22618, _22620] : [member(_22616, difference(_22620, _22618)), 61 ^ _20588 : [(62 ^ _20588) ^ [] : [-(member(_22616, _22620))], (64 ^ _20588) ^ [] : [member(_22616, _22618)]]], (66 ^ _20588) ^ [_22868, _22870, _22872] : [-(member(_22868, difference(_22872, _22870))), member(_22868, _22872), -(member(_22868, _22870))], (76 ^ _20588) ^ [_23217, _23219] : [_23219 = _23217, 79 ^ _20588 : [(80 ^ _20588) ^ [] : [-(subset(_23219, _23217))], (82 ^ _20588) ^ [] : [-(subset(_23217, _23219))]]], (84 ^ _20588) ^ [_23454, _23456] : [-(_23456 = _23454), subset(_23456, _23454), subset(_23454, _23456)], (113 ^ _20588) ^ [_24406] : [-(subset(_24406, _24406))], (104 ^ _20588) ^ [_24098, _24100] : [106 ^ _20588 : [(107 ^ _20588) ^ [] : [-(member(105 ^ [_24098, _24100], _24100))], (109 ^ _20588) ^ [] : [member(105 ^ [_24098, _24100], _24098)]], -(subset(_24100, _24098))], (94 ^ _20588) ^ [_23784, _23786] : [subset(_23786, _23784), 97 ^ _20588 : [(98 ^ _20588) ^ [_23921] : [member(_23921, _23786), -(member(_23921, _23784))]]], (48 ^ _20588) ^ [_22240, _22242, _22244, _22246] : [-(difference(_22246, _22242) = difference(_22244, _22240)), _22246 = _22244, _22242 = _22240], (2 ^ _20588) ^ [_20732] : [-(_20732 = _20732)], (4 ^ _20588) ^ [_20839, _20841] : [_20841 = _20839, -(_20839 = _20841)], (10 ^ _20588) ^ [_21043, _21045, _21047] : [-(_21047 = _21043), _21047 = _21045, _21045 = _21043], (20 ^ _20588) ^ [_21384, _21386, _21388, _21390] : [-(subset(_21388, _21384)), subset(_21390, _21386), _21390 = _21388, _21386 = _21384], (34 ^ _20588) ^ [_21808, _21810, _21812, _21814] : [-(member(_21812, _21808)), member(_21814, _21810), _21814 = _21812, _21810 = _21808]], input).
% 0.37/1.37 ncf('1',plain,[114 ^ [] = difference(115 ^ [], 116 ^ [])],start(136 ^ 0)).
% 0.37/1.37 ncf('1.1',plain,[-(114 ^ [] = difference(115 ^ [], 116 ^ [])), subset(114 ^ [], difference(115 ^ [], 116 ^ [])), subset(difference(115 ^ [], 116 ^ []), 114 ^ [])],extension(84 ^ 1,bind([[_23454, _23456], [difference(115 ^ [], 116 ^ []), 114 ^ []]]))).
% 0.37/1.37 ncf('1.1.1',plain,[-(subset(114 ^ [], difference(115 ^ [], 116 ^ []))), 109 : member(105 ^ [difference(115 ^ [], 116 ^ []), 114 ^ []], difference(115 ^ [], 116 ^ []))],extension(104 ^ 2,bind([[_24098, _24100], [difference(115 ^ [], 116 ^ []), 114 ^ []]]))).
% 0.37/1.37 ncf('1.1.1.1',plain,[-(member(105 ^ [difference(115 ^ [], 116 ^ []), 114 ^ []], difference(115 ^ [], 116 ^ []))), member(105 ^ [difference(115 ^ [], 116 ^ []), 114 ^ []], 115 ^ []), -(member(105 ^ [difference(115 ^ [], 116 ^ []), 114 ^ []], 116 ^ []))],extension(66 ^ 5,bind([[_22868, _22870, _22872], [105 ^ [difference(115 ^ [], 116 ^ []), 114 ^ []], 116 ^ [], 115 ^ []]]))).
% 0.37/1.37 ncf('1.1.1.1.1',plain,[-(member(105 ^ [difference(115 ^ [], 116 ^ []), 114 ^ []], 115 ^ [])), member(105 ^ [difference(115 ^ [], 116 ^ []), 114 ^ []], 114 ^ [])],extension(118 ^ 6,bind([[_24762], [105 ^ [difference(115 ^ [], 116 ^ []), 114 ^ []]]]))).
% 0.37/1.37 ncf('1.1.1.1.1.1',plain,[-(member(105 ^ [difference(115 ^ [], 116 ^ []), 114 ^ []], 114 ^ []))],extension(107 ^ 7)).
% 0.37/1.37 ncf('1.1.1.1.2',plain,[member(105 ^ [difference(115 ^ [], 116 ^ []), 114 ^ []], 116 ^ []), member(105 ^ [difference(115 ^ [], 116 ^ []), 114 ^ []], 114 ^ [])],extension(118 ^ 6,bind([[_24762], [105 ^ [difference(115 ^ [], 116 ^ []), 114 ^ []]]]))).
% 0.37/1.37 ncf('1.1.1.1.2.1',plain,[-(member(105 ^ [difference(115 ^ [], 116 ^ []), 114 ^ []], 114 ^ []))],extension(107 ^ 7)).
% 0.37/1.37 ncf('1.1.2',plain,[-(subset(difference(115 ^ [], 116 ^ []), 114 ^ [])), 107 : -(member(105 ^ [114 ^ [], difference(115 ^ [], 116 ^ [])], difference(115 ^ [], 116 ^ [])))],extension(104 ^ 2,bind([[_24098, _24100], [114 ^ [], difference(115 ^ [], 116 ^ [])]]))).
% 0.37/1.37 ncf('1.1.2.1',plain,[member(105 ^ [114 ^ [], difference(115 ^ [], 116 ^ [])], difference(115 ^ [], 116 ^ [])), 62 : -(member(105 ^ [114 ^ [], difference(115 ^ [], 116 ^ [])], 115 ^ []))],extension(58 ^ 5,bind([[_22616, _22618, _22620], [105 ^ [114 ^ [], difference(115 ^ [], 116 ^ [])], 116 ^ [], 115 ^ []]]))).
% 0.37/1.37 ncf('1.1.2.1.1',plain,[member(105 ^ [114 ^ [], difference(115 ^ [], 116 ^ [])], 115 ^ []), -(member(105 ^ [114 ^ [], difference(115 ^ [], 116 ^ [])], 114 ^ [])), -(member(105 ^ [114 ^ [], difference(115 ^ [], 116 ^ [])], 116 ^ []))],extension(126 ^ 8,bind([[_24992], [105 ^ [114 ^ [], difference(115 ^ [], 116 ^ [])]]]))).
% 0.37/1.37 ncf('1.1.2.1.1.1',plain,[member(105 ^ [114 ^ [], difference(115 ^ [], 116 ^ [])], 114 ^ [])],extension(109 ^ 9)).
% 0.37/1.37 ncf('1.1.2.1.1.2',plain,[member(105 ^ [114 ^ [], difference(115 ^ [], 116 ^ [])], 116 ^ [])],extension(64 ^ 9)).
% 0.37/1.37 %-----------------------------------------------------
% 0.37/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------