%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU031+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n027.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:51 EDT 2022
% Result : Theorem 0.45s 1.39s
% Output : Proof 0.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : SEU031+1 : TPTP v8.1.0. Released v3.2.0.
% 0.10/0.12 % Command : leancop_casc.sh %s %d
% 0.13/0.32 % Computer : n027.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 600
% 0.13/0.32 % DateTime : Sun Jun 19 20:16:54 EDT 2022
% 0.18/0.32 % CPUTime :
% 0.45/1.39 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.45/1.40 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.45/1.40
% 0.45/1.40 %-----------------------------------------------------
% 0.45/1.40 fof(t64_funct_1, conjecture, ! [_59979] : (relation(_59979) & function(_59979) => ! [_60001] : (relation(_60001) & function(_60001) => one_to_one(_59979) & relation_rng(_60001) = relation_dom(_59979) & relation_composition(_60001, _59979) = identity_relation(relation_rng(_59979)) => _60001 = function_inverse(_59979))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t64_funct_1)).
% 0.45/1.40 fof(dt_k2_funct_1, axiom, ! [_60457] : (relation(_60457) & function(_60457) => relation(function_inverse(_60457)) & function(function_inverse(_60457))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k2_funct_1)).
% 0.45/1.40 fof(l72_funct_1, axiom, ! [_60674, _60677] : (relation(_60677) & function(_60677) => ! [_60699] : (relation(_60699) & function(_60699) => ! [_60721] : (relation(_60721) & function(_60721) => relation_rng(_60677) = _60674 & relation_composition(_60677, _60699) = identity_relation(relation_dom(_60721)) & relation_composition(_60699, _60721) = identity_relation(_60674) => _60721 = _60677))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l72_funct_1)).
% 0.45/1.40 fof(t55_funct_1, axiom, ! [_61140] : (relation(_61140) & function(_61140) => one_to_one(_61140) => relation_rng(_61140) = relation_dom(function_inverse(_61140)) & relation_dom(_61140) = relation_rng(function_inverse(_61140))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t55_funct_1)).
% 0.45/1.40 fof(t61_funct_1, axiom, ! [_61386] : (relation(_61386) & function(_61386) => one_to_one(_61386) => relation_composition(_61386, function_inverse(_61386)) = identity_relation(relation_dom(_61386)) & relation_composition(function_inverse(_61386), _61386) = identity_relation(relation_rng(_61386))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t61_funct_1)).
% 0.45/1.40
% 0.45/1.40 cnf(1, plain, [-(relation(12 ^ []))], clausify(t64_funct_1)).
% 0.45/1.40 cnf(2, plain, [-(function(12 ^ []))], clausify(t64_funct_1)).
% 0.45/1.40 cnf(3, plain, [-(relation(13 ^ []))], clausify(t64_funct_1)).
% 0.45/1.40 cnf(4, plain, [-(function(13 ^ []))], clausify(t64_funct_1)).
% 0.45/1.40 cnf(5, plain, [-(one_to_one(12 ^ []))], clausify(t64_funct_1)).
% 0.45/1.40 cnf(6, plain, [-(relation_rng(13 ^ []) = relation_dom(12 ^ []))], clausify(t64_funct_1)).
% 0.45/1.40 cnf(7, plain, [-(relation_composition(13 ^ [], 12 ^ []) = identity_relation(relation_rng(12 ^ [])))], clausify(t64_funct_1)).
% 0.45/1.40 cnf(8, plain, [13 ^ [] = function_inverse(12 ^ [])], clausify(t64_funct_1)).
% 0.45/1.40 cnf(9, plain, [_24041 = _24090, -(identity_relation(_24041) = identity_relation(_24090))], theory(equality)).
% 0.45/1.40 cnf(10, plain, [_19330 = _19375, -(_19375 = _19330)], theory(equality)).
% 0.45/1.40 cnf(11, plain, [-(_19609 = _19720), _19609 = _19665, _19665 = _19720], theory(equality)).
% 0.45/1.40 cnf(12, plain, [-(relation(function_inverse(_27274))), relation(_27274), function(_27274)], clausify(dt_k2_funct_1)).
% 0.45/1.40 cnf(13, plain, [-(function(function_inverse(_27274))), relation(_27274), function(_27274)], clausify(dt_k2_funct_1)).
% 0.45/1.40 cnf(14, plain, [function(_32247), relation(_32247), function(_32448), relation(_32448), function(_32638), relation(_32638), -(_32638 = _32247), relation_rng(_32247) = _32136, relation_composition(_32247, _32448) = identity_relation(relation_dom(_32638)), relation_composition(_32448, _32638) = identity_relation(_32136)], clausify(l72_funct_1)).
% 0.45/1.40 cnf(15, plain, [function(_37545), relation(_37545), one_to_one(_37545), -(relation_rng(_37545) = relation_dom(function_inverse(_37545)))], clausify(t55_funct_1)).
% 0.45/1.40 cnf(16, plain, [function(_38568), relation(_38568), one_to_one(_38568), -(relation_composition(_38568, function_inverse(_38568)) = identity_relation(relation_dom(_38568)))], clausify(t61_funct_1)).
% 0.45/1.40
% 0.45/1.40 cnf('1',plain,[13 ^ [] = function_inverse(12 ^ [])],start(8)).
% 0.45/1.40 cnf('1.1',plain,[-(13 ^ [] = function_inverse(12 ^ [])), function_inverse(12 ^ []) = 13 ^ []],extension(10,bind([[_19330, _19375], [function_inverse(12 ^ []), 13 ^ []]]))).
% 0.45/1.40 cnf('1.1.1',plain,[-(function_inverse(12 ^ []) = 13 ^ []), function(13 ^ []), relation(13 ^ []), function(12 ^ []), relation(12 ^ []), function(function_inverse(12 ^ [])), relation(function_inverse(12 ^ [])), relation_rng(13 ^ []) = relation_dom(12 ^ []), relation_composition(13 ^ [], 12 ^ []) = identity_relation(relation_dom(function_inverse(12 ^ []))), relation_composition(12 ^ [], function_inverse(12 ^ [])) = identity_relation(relation_dom(12 ^ []))],extension(14,bind([[_32247, _32448, _32638, _32136], [13 ^ [], 12 ^ [], function_inverse(12 ^ []), relation_dom(12 ^ [])]]))).
% 0.45/1.40 cnf('1.1.1.1',plain,[-(function(13 ^ []))],extension(4)).
% 0.45/1.40 cnf('1.1.1.2',plain,[-(relation(13 ^ []))],extension(3)).
% 0.45/1.40 cnf('1.1.1.3',plain,[-(function(12 ^ []))],extension(2)).
% 0.45/1.40 cnf('1.1.1.4',plain,[-(relation(12 ^ []))],extension(1)).
% 0.45/1.40 cnf('1.1.1.5',plain,[-(function(function_inverse(12 ^ []))), relation(12 ^ []), function(12 ^ [])],extension(13,bind([[_27274], [12 ^ []]]))).
% 0.45/1.40 cnf('1.1.1.5.1',plain,[-(relation(12 ^ []))],extension(1)).
% 0.45/1.40 cnf('1.1.1.5.2',plain,[-(function(12 ^ []))],extension(2)).
% 0.45/1.40 cnf('1.1.1.6',plain,[-(relation(function_inverse(12 ^ []))), relation(12 ^ []), function(12 ^ [])],extension(12,bind([[_27274], [12 ^ []]]))).
% 0.45/1.40 cnf('1.1.1.6.1',plain,[-(relation(12 ^ []))],extension(1)).
% 0.45/1.40 cnf('1.1.1.6.2',plain,[-(function(12 ^ []))],extension(2)).
% 0.45/1.40 cnf('1.1.1.7',plain,[-(relation_rng(13 ^ []) = relation_dom(12 ^ []))],extension(6)).
% 0.45/1.40 cnf('1.1.1.8',plain,[-(relation_composition(13 ^ [], 12 ^ []) = identity_relation(relation_dom(function_inverse(12 ^ [])))), relation_composition(13 ^ [], 12 ^ []) = identity_relation(relation_rng(12 ^ [])), identity_relation(relation_rng(12 ^ [])) = identity_relation(relation_dom(function_inverse(12 ^ [])))],extension(11,bind([[_19609, _19665, _19720], [relation_composition(13 ^ [], 12 ^ []), identity_relation(relation_rng(12 ^ [])), identity_relation(relation_dom(function_inverse(12 ^ [])))]]))).
% 0.45/1.40 cnf('1.1.1.8.1',plain,[-(relation_composition(13 ^ [], 12 ^ []) = identity_relation(relation_rng(12 ^ [])))],extension(7)).
% 0.45/1.40 cnf('1.1.1.8.2',plain,[-(identity_relation(relation_rng(12 ^ [])) = identity_relation(relation_dom(function_inverse(12 ^ [])))), relation_rng(12 ^ []) = relation_dom(function_inverse(12 ^ []))],extension(9,bind([[_24041, _24090], [relation_rng(12 ^ []), relation_dom(function_inverse(12 ^ []))]]))).
% 0.45/1.40 cnf('1.1.1.8.2.1',plain,[-(relation_rng(12 ^ []) = relation_dom(function_inverse(12 ^ []))), function(12 ^ []), relation(12 ^ []), one_to_one(12 ^ [])],extension(15,bind([[_37545], [12 ^ []]]))).
% 0.45/1.40 cnf('1.1.1.8.2.1.1',plain,[-(function(12 ^ []))],extension(2)).
% 0.45/1.40 cnf('1.1.1.8.2.1.2',plain,[-(relation(12 ^ []))],extension(1)).
% 0.45/1.40 cnf('1.1.1.8.2.1.3',plain,[-(one_to_one(12 ^ []))],extension(5)).
% 0.45/1.40 cnf('1.1.1.9',plain,[-(relation_composition(12 ^ [], function_inverse(12 ^ [])) = identity_relation(relation_dom(12 ^ []))), function(12 ^ []), relation(12 ^ []), one_to_one(12 ^ [])],extension(16,bind([[_38568], [12 ^ []]]))).
% 0.45/1.40 cnf('1.1.1.9.1',plain,[-(function(12 ^ []))],extension(2)).
% 0.45/1.40 cnf('1.1.1.9.2',plain,[-(relation(12 ^ []))],extension(1)).
% 0.45/1.40 cnf('1.1.1.9.3',plain,[-(one_to_one(12 ^ []))],extension(5)).
% 0.45/1.40 %-----------------------------------------------------
% 0.45/1.41
% 0.45/1.41 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------