%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU171+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n019.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:30 EDT 2023
% Result : Theorem 1.87s 2.42s
% Output : Proof 1.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SEU171+1 : TPTP v8.1.2. Released v3.3.0.
% 0.04/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n019.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 13:38:12 EDT 2023
% 0.12/0.34 % CPUTime :
% 1.87/2.42
% 1.87/2.42 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 1.87/2.42 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.87/2.42 %-----------------------------------------------------
% 1.87/2.42 ncf(matrix, plain, [(261 ^ _40124) ^ [] : [259 ^ [] = empty_set], (264 ^ _40124) ^ [] : [-(element(262 ^ [], powerset(259 ^ [])))], (267 ^ _40124) ^ [] : [-(element(265 ^ [], 259 ^ []))], (269 ^ _40124) ^ [] : [in(265 ^ [], 262 ^ [])], (271 ^ _40124) ^ [] : [in(265 ^ [], subset_complement(259 ^ [], 262 ^ []))], (58 ^ _40124) ^ [_42093, _42095, _42097, _42099] : [-(set_difference(_42099, _42095) = set_difference(_42097, _42093)), _42099 = _42097, _42095 = _42093], (68 ^ _40124) ^ [_42424, _42426] : [_42426 = _42424, -(powerset(_42426) = powerset(_42424))], (74 ^ _40124) ^ [_42650, _42652, _42654, _42656] : [-(subset_complement(_42656, _42652) = subset_complement(_42654, _42650)), _42656 = _42654, _42652 = _42650], (2 ^ _40124) ^ [_40268] : [-(_40268 = _40268)], (4 ^ _40124) ^ [_40375, _40377] : [_40377 = _40375, -(_40375 = _40377)], (10 ^ _40124) ^ [_40579, _40581, _40583] : [-(_40583 = _40579), _40583 = _40581, _40581 = _40579], (20 ^ _40124) ^ [_40892, _40894] : [-(empty(_40892)), _40894 = _40892, empty(_40894)], (30 ^ _40124) ^ [_41215, _41217, _41219, _41221] : [-(element(_41219, _41215)), element(_41221, _41217), _41221 = _41219, _41217 = _41215], (44 ^ _40124) ^ [_41639, _41641, _41643, _41645] : [-(in(_41643, _41639)), in(_41645, _41641), _41645 = _41643, _41641 = _41639], (84 ^ _40124) ^ [_42991, _42993] : [in(_42993, _42991), in(_42991, _42993)], (90 ^ _40124) ^ [_43222, _43224] : [-(empty(_43224)), 93 ^ _40124 : [(94 ^ _40124) ^ [] : [element(_43222, _43224), -(in(_43222, _43224))], (100 ^ _40124) ^ [] : [in(_43222, _43224), -(element(_43222, _43224))]]], (106 ^ _40124) ^ [_43635, _43637] : [empty(_43637), 109 ^ _40124 : [(110 ^ _40124) ^ [] : [element(_43635, _43637), -(empty(_43635))], (116 ^ _40124) ^ [] : [empty(_43635), -(element(_43635, _43637))]]], (144 ^ _40124) ^ [_44866, _44868, _44870] : [-(_44866 = set_difference(_44870, _44868)), 156 ^ _40124 : [(157 ^ _40124) ^ [] : [-(in(145 ^ [_44866, _44868, _44870], _44870))], (159 ^ _40124) ^ [] : [in(145 ^ [_44866, _44868, _44870], _44868)], (161 ^ _40124) ^ [] : [in(145 ^ [_44866, _44868, _44870], _44866)]], 148 ^ _40124 : [(149 ^ _40124) ^ [] : [-(in(145 ^ [_44866, _44868, _44870], _44866))], (151 ^ _40124) ^ [] : [in(145 ^ [_44866, _44868, _44870], _44870), -(in(145 ^ [_44866, _44868, _44870], _44868))]]], (122 ^ _40124) ^ [_44135, _44137, _44139] : [_44135 = set_difference(_44139, _44137), 125 ^ _40124 : [(126 ^ _40124) ^ [_44319] : [in(_44319, _44135), 129 ^ _40124 : [(130 ^ _40124) ^ [] : [-(in(_44319, _44139))], (132 ^ _40124) ^ [] : [in(_44319, _44137)]]], (134 ^ _40124) ^ [_44579] : [-(in(_44579, _44135)), in(_44579, _44139), -(in(_44579, _44137))]]], (165 ^ _40124) ^ [_45623, _45625] : [element(_45623, powerset(_45625)), -(subset_complement(_45625, _45623) = set_difference(_45625, _45623))], (171 ^ _40124) ^ [] : [true___, -(true___)], (177 ^ _40124) ^ [] : [true___, -(true___)], (183 ^ _40124) ^ [_46087, _46089] : [element(_46087, powerset(_46089)), -(element(subset_complement(_46089, _46087), powerset(_46089)))], (189 ^ _40124) ^ [] : [true___, -(true___)], (195 ^ _40124) ^ [] : [true___, -(true___)], (202 ^ _40124) ^ [_46559] : [-(element(200 ^ [_46559], _46559))], (204 ^ _40124) ^ [_46641] : [empty(powerset(_46641))], (206 ^ _40124) ^ [] : [-(empty(empty_set))], (208 ^ _40124) ^ [_46802, _46804] : [element(_46802, powerset(_46804)), -(subset_complement(_46804, subset_complement(_46804, _46802)) = _46802)], (214 ^ _40124) ^ [_47014] : [-(empty(_47014)), 218 ^ _40124 : [(219 ^ _40124) ^ [] : [-(element(217 ^ [_47014], powerset(_47014)))], (221 ^ _40124) ^ [] : [empty(217 ^ [_47014])]]], (224 ^ _40124) ^ [] : [-(empty(222 ^ []))], (227 ^ _40124) ^ [_47486] : [-(element(225 ^ [_47486], powerset(_47486)))], (229 ^ _40124) ^ [_47537] : [-(empty(225 ^ [_47537]))], (232 ^ _40124) ^ [] : [empty(230 ^ [])], (234 ^ _40124) ^ [_47711] : [-(set_difference(_47711, empty_set) = _47711)], (236 ^ _40124) ^ [_47792] : [-(set_difference(empty_set, _47792) = empty_set)], (238 ^ _40124) ^ [_47888] : [empty(_47888), -(_47888 = empty_set)], (244 ^ _40124) ^ [_48090, _48092] : [in(_48092, _48090), empty(_48090)], (250 ^ _40124) ^ [_48277, _48279] : [empty(_48279), -(_48279 = _48277), empty(_48277)]], input).
% 1.87/2.42 ncf('1',plain,[empty(powerset(259 ^ []))],start(204 ^ 0,bind([[_46641], [259 ^ []]]))).
% 1.87/2.42 ncf('1.1',plain,[-(empty(powerset(259 ^ []))), 100 : in(262 ^ [], powerset(259 ^ [])), 100 : -(element(262 ^ [], powerset(259 ^ [])))],extension(90 ^ 1,bind([[_43222, _43224], [262 ^ [], powerset(259 ^ [])]]))).
% 1.87/2.42 ncf('1.1.1',plain,[-(in(262 ^ [], powerset(259 ^ []))), in(262 ^ [], powerset(259 ^ [])), 262 ^ [] = 262 ^ [], powerset(259 ^ []) = powerset(259 ^ [])],extension(44 ^ 4,bind([[_41639, _41641, _41643, _41645], [powerset(259 ^ []), powerset(259 ^ []), 262 ^ [], 262 ^ []]]))).
% 1.87/2.42 ncf('1.1.1.1',plain,[-(in(262 ^ [], powerset(259 ^ []))), in(262 ^ [], powerset(259 ^ [])), 262 ^ [] = 262 ^ [], powerset(259 ^ []) = powerset(259 ^ [])],extension(44 ^ 5,bind([[_41639, _41641, _41643, _41645], [powerset(259 ^ []), powerset(259 ^ []), 262 ^ [], 262 ^ []]]))).
% 1.87/2.42 ncf('1.1.1.1.1',plain,[-(in(262 ^ [], powerset(259 ^ []))), in(262 ^ [], powerset(259 ^ [])), 262 ^ [] = 262 ^ [], powerset(259 ^ []) = powerset(259 ^ [])],extension(44 ^ 6,bind([[_41639, _41641, _41643, _41645], [powerset(259 ^ []), powerset(259 ^ []), 262 ^ [], 262 ^ []]]))).
% 1.87/2.42 ncf('1.1.1.1.1.1',plain,[-(in(262 ^ [], powerset(259 ^ []))), element(262 ^ [], powerset(259 ^ []))],extension(94 ^ 7)).
% 1.87/2.42 ncf('1.1.1.1.1.1.1',plain,[-(element(262 ^ [], powerset(259 ^ [])))],extension(264 ^ 8)).
% 1.87/2.42 ncf('1.1.1.1.1.2',plain,[-(262 ^ [] = 262 ^ [])],extension(2 ^ 7,bind([[_40268], [262 ^ []]]))).
% 1.87/2.42 ncf('1.1.1.1.1.3',plain,[-(powerset(259 ^ []) = powerset(259 ^ []))],extension(2 ^ 7,bind([[_40268], [powerset(259 ^ [])]]))).
% 1.87/2.42 ncf('1.1.1.1.2',plain,[-(262 ^ [] = 262 ^ [])],extension(2 ^ 6,bind([[_40268], [262 ^ []]]))).
% 1.87/2.42 ncf('1.1.1.1.3',plain,[-(powerset(259 ^ []) = powerset(259 ^ [])), 259 ^ [] = 259 ^ []],extension(68 ^ 6,bind([[_42424, _42426], [259 ^ [], 259 ^ []]]))).
% 1.87/2.42 ncf('1.1.1.1.3.1',plain,[-(259 ^ [] = 259 ^ [])],extension(2 ^ 7,bind([[_40268], [259 ^ []]]))).
% 1.87/2.42 ncf('1.1.1.2',plain,[-(262 ^ [] = 262 ^ [])],extension(2 ^ 5,bind([[_40268], [262 ^ []]]))).
% 1.87/2.42 ncf('1.1.1.3',plain,[-(powerset(259 ^ []) = powerset(259 ^ [])), 259 ^ [] = 259 ^ []],extension(68 ^ 5,bind([[_42424, _42426], [259 ^ [], 259 ^ []]]))).
% 1.87/2.42 ncf('1.1.1.3.1',plain,[-(259 ^ [] = 259 ^ [])],extension(2 ^ 6,bind([[_40268], [259 ^ []]]))).
% 1.87/2.42 ncf('1.1.2',plain,[element(262 ^ [], powerset(259 ^ [])), -(subset_complement(259 ^ [], 262 ^ []) = set_difference(259 ^ [], 262 ^ []))],extension(165 ^ 4,bind([[_45623, _45625], [262 ^ [], 259 ^ []]]))).
% 1.87/2.42 ncf('1.1.2.1',plain,[subset_complement(259 ^ [], 262 ^ []) = set_difference(259 ^ [], 262 ^ []), 134 : -(in(265 ^ [], subset_complement(259 ^ [], 262 ^ []))), 134 : in(265 ^ [], 259 ^ []), 134 : -(in(265 ^ [], 262 ^ []))],extension(122 ^ 5,bind([[_44135, _44137, _44139, _44579], [subset_complement(259 ^ [], 262 ^ []), 262 ^ [], 259 ^ [], 265 ^ []]]))).
% 1.87/2.42 ncf('1.1.2.1.1',plain,[in(265 ^ [], subset_complement(259 ^ [], 262 ^ []))],extension(271 ^ 8)).
% 1.87/2.42 ncf('1.1.2.1.2',plain,[-(in(265 ^ [], 259 ^ [])), 94 : element(265 ^ [], 259 ^ []), 94 : -(empty(259 ^ []))],extension(90 ^ 8,bind([[_43222, _43224], [265 ^ [], 259 ^ []]]))).
% 1.87/2.42 ncf('1.1.2.1.2.1',plain,[-(element(265 ^ [], 259 ^ []))],extension(267 ^ 11)).
% 1.87/2.42 ncf('1.1.2.1.2.2',plain,[empty(259 ^ []), -(259 ^ [] = empty_set)],extension(238 ^ 9,bind([[_47888], [259 ^ []]]))).
% 1.87/2.42 ncf('1.1.2.1.2.2.1',plain,[259 ^ [] = empty_set],extension(261 ^ 10)).
% 1.87/2.42 ncf('1.1.2.1.3',plain,[in(265 ^ [], 262 ^ [])],extension(269 ^ 8)).
% 1.87/2.42 %-----------------------------------------------------
% 1.87/2.42 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------