%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU002+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n004.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 : 600s
% DateTime : Tue Jul 19 11:59:44 EDT 2022
% Result : Theorem 159.23s 154.49s
% Output : Proof 159.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.11 % Problem : SEU002+1 : TPTP v8.1.0. Released v3.2.0.
% 0.04/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.32 % Computer : n004.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 600
% 0.11/0.32 % DateTime : Sat Jun 18 19:40:08 EDT 2022
% 0.11/0.33 % CPUTime :
% 159.23/154.49 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 159.23/154.50 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 159.23/154.50
% 159.23/154.50 %-----------------------------------------------------
% 159.23/154.50 fof(t25_funct_1, conjecture, ! [_60251, _60254] : (relation(_60254) & function(_60254) => ! [_60276] : (relation(_60276) & function(_60276) => in(_60251, relation_rng(relation_composition(_60276, _60254))) => in(_60251, relation_rng(_60254)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t25_funct_1)).
% 159.23/154.50 fof(d5_funct_1, axiom, ! [_60651] : (relation(_60651) & function(_60651) => ! [_60673] : (_60673 = relation_rng(_60651) <=> ! [_60691] : (in(_60691, _60673) <=> ? [_60709] : (in(_60709, relation_dom(_60651)) & _60691 = apply(_60651, _60709))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d5_funct_1)).
% 159.23/154.50 fof(dt_k5_relat_1, axiom, ! [_61027, _61030] : (relation(_61027) & relation(_61030) => relation(relation_composition(_61027, _61030))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k5_relat_1)).
% 159.23/154.50 fof(fc1_funct_1, axiom, ! [_61203, _61206] : (relation(_61203) & function(_61203) & relation(_61206) & function(_61206) => relation(relation_composition(_61203, _61206)) & function(relation_composition(_61203, _61206))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc1_funct_1)).
% 159.23/154.50 fof(t21_funct_1, axiom, ! [_61480, _61483] : (relation(_61483) & function(_61483) => ! [_61505] : (relation(_61505) & function(_61505) => (in(_61480, relation_dom(relation_composition(_61505, _61483))) <=> in(_61480, relation_dom(_61505)) & in(apply(_61505, _61480), relation_dom(_61483))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t21_funct_1)).
% 159.23/154.50 fof(t22_funct_1, axiom, ! [_61828, _61831] : (relation(_61831) & function(_61831) => ! [_61853] : (relation(_61853) & function(_61853) => in(_61828, relation_dom(relation_composition(_61853, _61831))) => apply(relation_composition(_61853, _61831), _61828) = apply(_61831, apply(_61853, _61828)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t22_funct_1)).
% 159.23/154.50
% 159.23/154.50 cnf(1, plain, [-(relation(14 ^ []))], clausify(t25_funct_1)).
% 159.23/154.50 cnf(2, plain, [-(function(14 ^ []))], clausify(t25_funct_1)).
% 159.23/154.50 cnf(3, plain, [-(relation(15 ^ []))], clausify(t25_funct_1)).
% 159.23/154.50 cnf(4, plain, [-(function(15 ^ []))], clausify(t25_funct_1)).
% 159.23/154.50 cnf(5, plain, [-(in(13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ []))))], clausify(t25_funct_1)).
% 159.23/154.50 cnf(6, plain, [in(13 ^ [], relation_rng(14 ^ []))], clausify(t25_funct_1)).
% 159.23/154.50 cnf(7, plain, [_22702 = _22751, -(relation_rng(_22702) = relation_rng(_22751))], theory(equality)).
% 159.23/154.50 cnf(8, plain, [-(_16615 = _16615)], theory(equality)).
% 159.23/154.50 cnf(9, plain, [-(_17047 = _17158), _17047 = _17103, _17103 = _17158], theory(equality)).
% 159.23/154.50 cnf(10, plain, [function(_23877), relation(_23877), _24052 = relation_rng(_23877), in(_24200, _24052), -(in(1 ^ [_24200, _24052, _23877], relation_dom(_23877)))], clausify(d5_funct_1)).
% 159.23/154.50 cnf(11, plain, [function(_23877), relation(_23877), _24052 = relation_rng(_23877), in(_24200, _24052), -(_24200 = apply(_23877, 1 ^ [_24200, _24052, _23877]))], clausify(d5_funct_1)).
% 159.23/154.50 cnf(12, plain, [function(_23877), relation(_23877), _24052 = relation_rng(_23877), -(in(_24200, _24052)), in(_24324, relation_dom(_23877)), _24200 = apply(_23877, _24324)], clausify(d5_funct_1)).
% 159.23/154.50 cnf(13, plain, [-(relation(relation_composition(_24714, _24765))), relation(_24714), relation(_24765)], clausify(dt_k5_relat_1)).
% 159.23/154.50 cnf(14, plain, [-(function(relation_composition(_26003, _26072))), relation(_26003), function(_26003), relation(_26072), function(_26072)], clausify(fc1_funct_1)).
% 159.23/154.50 cnf(15, plain, [function(_31318), relation(_31318), function(_31496), relation(_31496), in(_31230, relation_dom(relation_composition(_31496, _31318))), -(in(apply(_31496, _31230), relation_dom(_31318)))], clausify(t21_funct_1)).
% 159.23/154.50 cnf(16, plain, [function(_32204), relation(_32204), function(_32381), relation(_32381), in(_32117, relation_dom(relation_composition(_32381, _32204))), -(apply(relation_composition(_32381, _32204), _32117) = apply(_32204, apply(_32381, _32117)))], clausify(t22_funct_1)).
% 159.23/154.50
% 159.23/154.50 cnf('1',plain,[-(relation(15 ^ []))],start(3)).
% 159.23/154.50 cnf('1.1',plain,[relation(15 ^ []), function(14 ^ []), relation(14 ^ []), function(15 ^ []), in(1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])], relation_dom(relation_composition(15 ^ [], 14 ^ []))), -(apply(relation_composition(15 ^ [], 14 ^ []), 1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])]) = apply(14 ^ [], apply(15 ^ [], 1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])])))],extension(16,bind([[_32204, _32381, _32117], [14 ^ [], 15 ^ [], 1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])]]]))).
% 159.23/154.50 cnf('1.1.1',plain,[-(function(14 ^ []))],extension(2)).
% 159.23/154.50 cnf('1.1.2',plain,[-(relation(14 ^ []))],extension(1)).
% 159.23/154.50 cnf('1.1.3',plain,[-(function(15 ^ []))],extension(4)).
% 159.23/154.50 cnf('1.1.4',plain,[-(in(1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])], relation_dom(relation_composition(15 ^ [], 14 ^ [])))), function(relation_composition(15 ^ [], 14 ^ [])), relation(relation_composition(15 ^ [], 14 ^ [])), relation_rng(relation_composition(15 ^ [], 14 ^ [])) = relation_rng(relation_composition(15 ^ [], 14 ^ [])), in(13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])))],extension(10,bind([[_23877, _24200, _24052], [relation_composition(15 ^ [], 14 ^ []), 13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ []))]]))).
% 159.23/154.50 cnf('1.1.4.1',plain,[-(function(relation_composition(15 ^ [], 14 ^ []))), relation(15 ^ []), function(15 ^ []), relation(14 ^ []), function(14 ^ [])],extension(14,bind([[_26003, _26072], [15 ^ [], 14 ^ []]]))).
% 159.23/154.50 cnf('1.1.4.1.1',plain,[-(relation(15 ^ []))],extension(3)).
% 159.23/154.50 cnf('1.1.4.1.2',plain,[-(function(15 ^ []))],extension(4)).
% 159.23/154.50 cnf('1.1.4.1.3',plain,[-(relation(14 ^ []))],extension(1)).
% 159.23/154.50 cnf('1.1.4.1.4',plain,[-(function(14 ^ []))],extension(2)).
% 159.23/154.50 cnf('1.1.4.2',plain,[-(relation(relation_composition(15 ^ [], 14 ^ []))), relation(15 ^ []), relation(14 ^ [])],extension(13,bind([[_24714, _24765], [15 ^ [], 14 ^ []]]))).
% 159.23/154.50 cnf('1.1.4.2.1',plain,[-(relation(15 ^ []))],extension(3)).
% 159.23/154.50 cnf('1.1.4.2.2',plain,[-(relation(14 ^ []))],extension(1)).
% 159.23/154.50 cnf('1.1.4.3',plain,[-(relation_rng(relation_composition(15 ^ [], 14 ^ [])) = relation_rng(relation_composition(15 ^ [], 14 ^ []))), relation_composition(15 ^ [], 14 ^ []) = relation_composition(15 ^ [], 14 ^ [])],extension(7,bind([[_22702, _22751], [relation_composition(15 ^ [], 14 ^ []), relation_composition(15 ^ [], 14 ^ [])]]))).
% 159.23/154.50 cnf('1.1.4.3.1',plain,[-(relation_composition(15 ^ [], 14 ^ []) = relation_composition(15 ^ [], 14 ^ []))],extension(8,bind([[_16615], [relation_composition(15 ^ [], 14 ^ [])]]))).
% 159.23/154.50 cnf('1.1.4.4',plain,[-(in(13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ []))))],extension(5)).
% 159.23/154.50 cnf('1.1.5',plain,[apply(relation_composition(15 ^ [], 14 ^ []), 1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])]) = apply(14 ^ [], apply(15 ^ [], 1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])])), -(13 ^ [] = apply(14 ^ [], apply(15 ^ [], 1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])]))), 13 ^ [] = apply(relation_composition(15 ^ [], 14 ^ []), 1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])])],extension(9,bind([[_17158, _17047, _17103], [apply(14 ^ [], apply(15 ^ [], 1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])])), 13 ^ [], apply(relation_composition(15 ^ [], 14 ^ []), 1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])])]]))).
% 159.23/154.50 cnf('1.1.5.1',plain,[13 ^ [] = apply(14 ^ [], apply(15 ^ [], 1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])])), function(14 ^ []), relation(14 ^ []), relation_rng(14 ^ []) = relation_rng(14 ^ []), -(in(13 ^ [], relation_rng(14 ^ []))), in(apply(15 ^ [], 1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])]), relation_dom(14 ^ []))],extension(12,bind([[_24200, _24052, _24324, _23877], [13 ^ [], relation_rng(14 ^ []), apply(15 ^ [], 1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])]), 14 ^ []]]))).
% 159.23/154.50 cnf('1.1.5.1.1',plain,[-(function(14 ^ []))],extension(2)).
% 159.23/154.50 cnf('1.1.5.1.2',plain,[-(relation(14 ^ []))],extension(1)).
% 159.23/154.50 cnf('1.1.5.1.3',plain,[-(relation_rng(14 ^ []) = relation_rng(14 ^ []))],extension(8,bind([[_16615], [relation_rng(14 ^ [])]]))).
% 159.23/154.50 cnf('1.1.5.1.4',plain,[in(13 ^ [], relation_rng(14 ^ []))],extension(6)).
% 159.23/154.50 cnf('1.1.5.1.5',plain,[-(in(apply(15 ^ [], 1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])]), relation_dom(14 ^ []))), function(14 ^ []), relation(14 ^ []), function(15 ^ []), relation(15 ^ []), in(1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])], relation_dom(relation_composition(15 ^ [], 14 ^ [])))],extension(15,bind([[_31230, _31496, _31318], [1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])], 15 ^ [], 14 ^ []]]))).
% 159.23/154.50 cnf('1.1.5.1.5.1',plain,[-(function(14 ^ []))],extension(2)).
% 159.23/154.50 cnf('1.1.5.1.5.2',plain,[-(relation(14 ^ []))],extension(1)).
% 159.23/154.50 cnf('1.1.5.1.5.3',plain,[-(function(15 ^ []))],extension(4)).
% 159.23/154.50 cnf('1.1.5.1.5.4',plain,[-(relation(15 ^ []))],extension(3)).
% 159.23/154.50 cnf('1.1.5.1.5.5',plain,[-(in(1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])], relation_dom(relation_composition(15 ^ [], 14 ^ []))))],lemmata('1.1')).
% 159.23/154.50 cnf('1.1.5.2',plain,[-(13 ^ [] = apply(relation_composition(15 ^ [], 14 ^ []), 1 ^ [13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])), relation_composition(15 ^ [], 14 ^ [])])), function(relation_composition(15 ^ [], 14 ^ [])), relation(relation_composition(15 ^ [], 14 ^ [])), relation_rng(relation_composition(15 ^ [], 14 ^ [])) = relation_rng(relation_composition(15 ^ [], 14 ^ [])), in(13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ [])))],extension(11,bind([[_23877, _24200, _24052], [relation_composition(15 ^ [], 14 ^ []), 13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ []))]]))).
% 159.23/154.50 cnf('1.1.5.2.1',plain,[-(function(relation_composition(15 ^ [], 14 ^ []))), relation(15 ^ []), function(15 ^ []), relation(14 ^ []), function(14 ^ [])],extension(14,bind([[_26003, _26072], [15 ^ [], 14 ^ []]]))).
% 159.23/154.50 cnf('1.1.5.2.1.1',plain,[-(relation(15 ^ []))],extension(3)).
% 159.23/154.50 cnf('1.1.5.2.1.2',plain,[-(function(15 ^ []))],extension(4)).
% 159.23/154.50 cnf('1.1.5.2.1.3',plain,[-(relation(14 ^ []))],extension(1)).
% 159.23/154.50 cnf('1.1.5.2.1.4',plain,[-(function(14 ^ []))],extension(2)).
% 159.23/154.50 cnf('1.1.5.2.2',plain,[-(relation(relation_composition(15 ^ [], 14 ^ []))), relation(15 ^ []), relation(14 ^ [])],extension(13,bind([[_24714, _24765], [15 ^ [], 14 ^ []]]))).
% 159.23/154.50 cnf('1.1.5.2.2.1',plain,[-(relation(15 ^ []))],extension(3)).
% 159.23/154.50 cnf('1.1.5.2.2.2',plain,[-(relation(14 ^ []))],extension(1)).
% 159.23/154.50 cnf('1.1.5.2.3',plain,[-(relation_rng(relation_composition(15 ^ [], 14 ^ [])) = relation_rng(relation_composition(15 ^ [], 14 ^ [])))],extension(8,bind([[_16615], [relation_rng(relation_composition(15 ^ [], 14 ^ []))]]))).
% 159.23/154.50 cnf('1.1.5.2.4',plain,[-(in(13 ^ [], relation_rng(relation_composition(15 ^ [], 14 ^ []))))],extension(5)).
% 159.23/154.50 %-----------------------------------------------------
% 159.23/154.51
% 159.33/154.51 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------