%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU224+2 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n010.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 12:01:11 EDT 2022
% Result : Theorem 0.58s 1.47s
% Output : Proof 0.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SEU224+2 : TPTP v8.1.0. Released v3.3.0.
% 0.08/0.15 % Command : leancop_casc.sh %s %d
% 0.14/0.37 % Computer : n010.cluster.edu
% 0.14/0.37 % Model : x86_64 x86_64
% 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.37 % Memory : 8042.1875MB
% 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.37 % CPULimit : 300
% 0.14/0.37 % WCLimit : 600
% 0.14/0.37 % DateTime : Sun Jun 19 12:19:37 EDT 2022
% 0.14/0.37 % CPUTime :
% 0.58/1.47 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.58/1.47 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.58/1.48
% 0.58/1.48 %-----------------------------------------------------
% 0.58/1.48 fof(l82_funct_1, conjecture, ! [_346580, _346583, _346586] : (relation(_346586) & function(_346586) => (in(_346583, relation_dom(relation_dom_restriction(_346586, _346580))) <=> in(_346583, relation_dom(_346586)) & in(_346583, _346580))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l82_funct_1)).
% 0.58/1.48 fof(t86_relat_1, lemma, ! [_347359, _347362, _347365] : (relation(_347365) => (in(_347359, relation_dom(relation_dom_restriction(_347365, _347362))) <=> in(_347359, _347362) & in(_347359, relation_dom(_347365)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t86_relat_1)).
% 0.58/1.48
% 0.58/1.48 cnf(1, plain, [-(84 ^ []), in(81 ^ [], relation_dom(relation_dom_restriction(82 ^ [], 80 ^ [])))], clausify(l82_funct_1)).
% 0.58/1.48 cnf(2, plain, [-(84 ^ []), -(in(81 ^ [], 80 ^ []))], clausify(l82_funct_1)).
% 0.58/1.48 cnf(3, plain, [-(84 ^ []), -(in(81 ^ [], relation_dom(82 ^ [])))], clausify(l82_funct_1)).
% 0.58/1.48 cnf(4, plain, [-(83 ^ []), in(81 ^ [], relation_dom(82 ^ [])), in(81 ^ [], 80 ^ [])], clausify(l82_funct_1)).
% 0.58/1.48 cnf(5, plain, [-(83 ^ []), -(in(81 ^ [], relation_dom(relation_dom_restriction(82 ^ [], 80 ^ []))))], clausify(l82_funct_1)).
% 0.58/1.48 cnf(6, plain, [-(relation(82 ^ []))], clausify(l82_funct_1)).
% 0.58/1.48 cnf(7, plain, [84 ^ [], 83 ^ []], clausify(l82_funct_1)).
% 0.58/1.48 cnf(8, plain, [relation(_238358), in(_238223, relation_dom(relation_dom_restriction(_238358, _238291))), -(in(_238223, _238291))], clausify(t86_relat_1)).
% 0.58/1.48 cnf(9, plain, [relation(_238358), in(_238223, relation_dom(relation_dom_restriction(_238358, _238291))), -(in(_238223, relation_dom(_238358)))], clausify(t86_relat_1)).
% 0.58/1.48 cnf(10, plain, [relation(_238358), -(in(_238223, relation_dom(relation_dom_restriction(_238358, _238291)))), in(_238223, _238291), in(_238223, relation_dom(_238358))], clausify(t86_relat_1)).
% 0.58/1.48
% 0.58/1.48 cnf('1',plain,[84 ^ [], 83 ^ []],start(7)).
% 0.58/1.48 cnf('1.1',plain,[-(84 ^ []), in(81 ^ [], relation_dom(relation_dom_restriction(82 ^ [], 80 ^ [])))],extension(1)).
% 0.58/1.48 cnf('1.1.1',plain,[-(in(81 ^ [], relation_dom(relation_dom_restriction(82 ^ [], 80 ^ [])))), relation(82 ^ []), in(81 ^ [], 80 ^ []), in(81 ^ [], relation_dom(82 ^ []))],extension(10,bind([[_238291, _238223, _238358], [80 ^ [], 81 ^ [], 82 ^ []]]))).
% 0.58/1.48 cnf('1.1.1.1',plain,[-(relation(82 ^ []))],extension(6)).
% 0.58/1.48 cnf('1.1.1.2',plain,[-(in(81 ^ [], 80 ^ [])), -(84 ^ [])],extension(2)).
% 0.58/1.48 cnf('1.1.1.2.1',plain,[84 ^ []],reduction('1')).
% 0.58/1.48 cnf('1.1.1.3',plain,[-(in(81 ^ [], relation_dom(82 ^ []))), -(84 ^ [])],extension(3)).
% 0.58/1.48 cnf('1.1.1.3.1',plain,[84 ^ []],reduction('1')).
% 0.58/1.48 cnf('1.2',plain,[-(83 ^ []), in(81 ^ [], relation_dom(82 ^ [])), in(81 ^ [], 80 ^ [])],extension(4)).
% 0.58/1.48 cnf('1.2.1',plain,[-(in(81 ^ [], relation_dom(82 ^ []))), relation(82 ^ []), in(81 ^ [], relation_dom(relation_dom_restriction(82 ^ [], 80 ^ [])))],extension(9,bind([[_238223, _238358, _238291], [81 ^ [], 82 ^ [], 80 ^ []]]))).
% 0.58/1.48 cnf('1.2.1.1',plain,[-(relation(82 ^ []))],extension(6)).
% 0.58/1.48 cnf('1.2.1.2',plain,[-(in(81 ^ [], relation_dom(relation_dom_restriction(82 ^ [], 80 ^ [])))), -(83 ^ [])],extension(5)).
% 0.58/1.48 cnf('1.2.1.2.1',plain,[83 ^ []],reduction('1')).
% 0.58/1.48 cnf('1.2.2',plain,[-(in(81 ^ [], 80 ^ [])), relation(82 ^ []), in(81 ^ [], relation_dom(relation_dom_restriction(82 ^ [], 80 ^ [])))],extension(8,bind([[_238223, _238358, _238291], [81 ^ [], 82 ^ [], 80 ^ []]]))).
% 0.58/1.48 cnf('1.2.2.1',plain,[-(relation(82 ^ []))],extension(6)).
% 0.58/1.48 cnf('1.2.2.2',plain,[-(in(81 ^ [], relation_dom(relation_dom_restriction(82 ^ [], 80 ^ [])))), -(83 ^ [])],extension(5)).
% 0.58/1.48 cnf('1.2.2.2.1',plain,[83 ^ []],reduction('1')).
% 0.58/1.48 %-----------------------------------------------------
% 0.58/1.49
% 0.58/1.49 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------