%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU257+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n024.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:54 EDT 2023
% Result : Theorem 0.35s 1.37s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SEU257+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n024.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:29:36 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.35/1.37
% 0.35/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.35/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.35/1.37 %-----------------------------------------------------
% 0.35/1.37 ncf(matrix, plain, [(240 ^ _34360) ^ [] : [-(relation(238 ^ []))], (242 ^ _34360) ^ [] : [-(well_ordering(238 ^ []))], (244 ^ _34360) ^ [] : [well_ordering(relation_restriction(238 ^ [], 237 ^ []))], (120 ^ _34360) ^ [_38243, _38245] : [-(set_intersection2(_38245, _38243) = set_intersection2(_38243, _38245))], (122 ^ _34360) ^ [_38344] : [relation(_38344), 125 ^ _34360 : [(126 ^ _34360) ^ [] : [well_ordering(_38344), 129 ^ _34360 : [(130 ^ _34360) ^ [] : [-(reflexive(_38344))], (132 ^ _34360) ^ [] : [-(transitive(_38344))], (134 ^ _34360) ^ [] : [-(antisymmetric(_38344))], (136 ^ _34360) ^ [] : [-(connected(_38344))], (138 ^ _34360) ^ [] : [-(well_founded_relation(_38344))]]], (140 ^ _34360) ^ [] : [-(well_ordering(_38344)), reflexive(_38344), transitive(_38344), antisymmetric(_38344), connected(_38344), well_founded_relation(_38344)]]], (162 ^ _34360) ^ [_39359] : [relation(_39359), 165 ^ _34360 : [(166 ^ _34360) ^ [_39478] : [-(relation_restriction(_39359, _39478) = set_intersection2(_39359, cartesian_product2(_39478, _39478)))]]], (168 ^ _34360) ^ [_39601, _39603] : [relation(_39603), -(relation(relation_restriction(_39603, _39601)))], (174 ^ _34360) ^ [] : [true___, -(true___)], (180 ^ _34360) ^ [] : [true___, -(true___)], (186 ^ _34360) ^ [_40036, _40038] : [-(set_intersection2(_40038, _40038) = _40038)], (188 ^ _34360) ^ [_40148, _40150] : [relation(_40148), reflexive(_40148), -(reflexive(relation_restriction(_40148, _40150)))], (198 ^ _34360) ^ [_40447, _40449] : [relation(_40447), connected(_40447), -(connected(relation_restriction(_40447, _40449)))], (208 ^ _34360) ^ [_40746, _40748] : [relation(_40746), transitive(_40746), -(transitive(relation_restriction(_40746, _40748)))], (218 ^ _34360) ^ [_41045, _41047] : [relation(_41045), antisymmetric(_41045), -(antisymmetric(relation_restriction(_41045, _41047)))], (228 ^ _34360) ^ [_41324, _41326] : [relation(_41324), well_founded_relation(_41324), -(well_founded_relation(relation_restriction(_41324, _41326)))], (90 ^ _34360) ^ [_37219, _37221, _37223, _37225] : [-(cartesian_product2(_37225, _37221) = cartesian_product2(_37223, _37219)), _37225 = _37223, _37221 = _37219], (100 ^ _34360) ^ [_37578, _37580, _37582, _37584] : [-(set_intersection2(_37584, _37580) = set_intersection2(_37582, _37578)), _37584 = _37582, _37580 = _37578], (110 ^ _34360) ^ [_37917, _37919, _37921, _37923] : [-(relation_restriction(_37923, _37919) = relation_restriction(_37921, _37917)), _37923 = _37921, _37919 = _37917], (2 ^ _34360) ^ [_34504] : [-(_34504 = _34504)], (4 ^ _34360) ^ [_34611, _34613] : [_34613 = _34611, -(_34611 = _34613)], (10 ^ _34360) ^ [_34815, _34817, _34819] : [-(_34819 = _34815), _34819 = _34817, _34817 = _34815], (20 ^ _34360) ^ [_35128, _35130] : [-(reflexive(_35128)), _35130 = _35128, reflexive(_35130)], (30 ^ _34360) ^ [_35423, _35425] : [-(connected(_35423)), _35425 = _35423, connected(_35425)], (40 ^ _34360) ^ [_35718, _35720] : [-(transitive(_35718)), _35720 = _35718, transitive(_35720)], (50 ^ _34360) ^ [_36013, _36015] : [-(antisymmetric(_36013)), _36015 = _36013, antisymmetric(_36015)], (60 ^ _34360) ^ [_36308, _36310] : [-(well_founded_relation(_36308)), _36310 = _36308, well_founded_relation(_36310)], (70 ^ _34360) ^ [_36603, _36605] : [-(relation(_36603)), _36605 = _36603, relation(_36605)], (80 ^ _34360) ^ [_36878, _36880] : [-(well_ordering(_36878)), _36880 = _36878, well_ordering(_36880)]], input).
% 0.35/1.37 ncf('1',plain,[well_ordering(relation_restriction(238 ^ [], 237 ^ []))],start(244 ^ 0)).
% 0.35/1.37 ncf('1.1',plain,[-(well_ordering(relation_restriction(238 ^ [], 237 ^ []))), 140 : reflexive(relation_restriction(238 ^ [], 237 ^ [])), 140 : transitive(relation_restriction(238 ^ [], 237 ^ [])), 140 : antisymmetric(relation_restriction(238 ^ [], 237 ^ [])), 140 : connected(relation_restriction(238 ^ [], 237 ^ [])), 140 : well_founded_relation(relation_restriction(238 ^ [], 237 ^ [])), 140 : relation(relation_restriction(238 ^ [], 237 ^ []))],extension(122 ^ 1,bind([[_38344], [relation_restriction(238 ^ [], 237 ^ [])]]))).
% 0.35/1.37 ncf('1.1.1',plain,[-(reflexive(relation_restriction(238 ^ [], 237 ^ []))), relation(238 ^ []), reflexive(238 ^ [])],extension(188 ^ 4,bind([[_40148, _40150], [238 ^ [], 237 ^ []]]))).
% 0.35/1.37 ncf('1.1.1.1',plain,[-(relation(238 ^ []))],extension(240 ^ 5)).
% 0.35/1.37 ncf('1.1.1.2',plain,[-(reflexive(238 ^ [])), 126 : well_ordering(238 ^ []), 126 : relation(238 ^ [])],extension(122 ^ 5,bind([[_38344], [238 ^ []]]))).
% 0.35/1.37 ncf('1.1.1.2.1',plain,[-(well_ordering(238 ^ []))],extension(242 ^ 8)).
% 0.35/1.37 ncf('1.1.1.2.2',plain,[-(relation(238 ^ []))],lemmata('[1, 1].x')).
% 0.35/1.37 ncf('1.1.2',plain,[-(transitive(relation_restriction(238 ^ [], 237 ^ []))), relation(238 ^ []), transitive(238 ^ [])],extension(208 ^ 4,bind([[_40746, _40748], [238 ^ [], 237 ^ []]]))).
% 0.35/1.37 ncf('1.1.2.1',plain,[-(relation(238 ^ []))],extension(240 ^ 5)).
% 0.35/1.37 ncf('1.1.2.2',plain,[-(transitive(238 ^ [])), 126 : well_ordering(238 ^ []), 126 : relation(238 ^ [])],extension(122 ^ 5,bind([[_38344], [238 ^ []]]))).
% 0.35/1.37 ncf('1.1.2.2.1',plain,[-(well_ordering(238 ^ []))],extension(242 ^ 8)).
% 0.35/1.37 ncf('1.1.2.2.2',plain,[-(relation(238 ^ []))],lemmata('[1, 1].x')).
% 0.35/1.37 ncf('1.1.3',plain,[-(antisymmetric(relation_restriction(238 ^ [], 237 ^ []))), relation(238 ^ []), antisymmetric(238 ^ [])],extension(218 ^ 4,bind([[_41045, _41047], [238 ^ [], 237 ^ []]]))).
% 0.35/1.37 ncf('1.1.3.1',plain,[-(relation(238 ^ []))],extension(240 ^ 5)).
% 0.35/1.37 ncf('1.1.3.2',plain,[-(antisymmetric(238 ^ [])), 126 : well_ordering(238 ^ []), 126 : relation(238 ^ [])],extension(122 ^ 5,bind([[_38344], [238 ^ []]]))).
% 0.35/1.37 ncf('1.1.3.2.1',plain,[-(well_ordering(238 ^ []))],extension(242 ^ 8)).
% 0.35/1.37 ncf('1.1.3.2.2',plain,[-(relation(238 ^ []))],lemmata('[1, 1].x')).
% 0.35/1.37 ncf('1.1.4',plain,[-(connected(relation_restriction(238 ^ [], 237 ^ []))), relation(238 ^ []), connected(238 ^ [])],extension(198 ^ 4,bind([[_40447, _40449], [238 ^ [], 237 ^ []]]))).
% 0.35/1.37 ncf('1.1.4.1',plain,[-(relation(238 ^ []))],extension(240 ^ 5)).
% 0.35/1.37 ncf('1.1.4.2',plain,[-(connected(238 ^ [])), 126 : well_ordering(238 ^ []), 126 : relation(238 ^ [])],extension(122 ^ 5,bind([[_38344], [238 ^ []]]))).
% 0.35/1.37 ncf('1.1.4.2.1',plain,[-(well_ordering(238 ^ []))],extension(242 ^ 8)).
% 0.35/1.37 ncf('1.1.4.2.2',plain,[-(relation(238 ^ []))],lemmata('[1, 1].x')).
% 0.35/1.37 ncf('1.1.5',plain,[-(well_founded_relation(relation_restriction(238 ^ [], 237 ^ []))), relation(238 ^ []), well_founded_relation(238 ^ [])],extension(228 ^ 4,bind([[_41324, _41326], [238 ^ [], 237 ^ []]]))).
% 0.35/1.37 ncf('1.1.5.1',plain,[-(relation(238 ^ []))],extension(240 ^ 5)).
% 0.35/1.37 ncf('1.1.5.2',plain,[-(well_founded_relation(238 ^ [])), 126 : well_ordering(238 ^ []), 126 : relation(238 ^ [])],extension(122 ^ 5,bind([[_38344], [238 ^ []]]))).
% 0.35/1.37 ncf('1.1.5.2.1',plain,[-(well_ordering(238 ^ []))],extension(242 ^ 8)).
% 0.35/1.37 ncf('1.1.5.2.2',plain,[-(relation(238 ^ []))],lemmata('[1, 1].x')).
% 0.35/1.37 ncf('1.1.6',plain,[-(relation(relation_restriction(238 ^ [], 237 ^ []))), relation(238 ^ [])],extension(168 ^ 2,bind([[_39601, _39603], [237 ^ [], 238 ^ []]]))).
% 0.35/1.37 ncf('1.1.6.1',plain,[-(relation(238 ^ []))],extension(240 ^ 3)).
% 0.35/1.37 %-----------------------------------------------------
% 0.35/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------