%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU206+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.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 : 600s
% DateTime : Tue Jul 19 12:00:59 EDT 2022
% Result : Theorem 0.51s 1.42s
% Output : Proof 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU206+1 : TPTP v8.1.0. Released v3.3.0.
% 0.06/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n024.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 : 600
% 0.12/0.34 % DateTime : Sun Jun 19 06:18:47 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.51/1.42 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.51/1.43 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.51/1.43
% 0.51/1.43 %-----------------------------------------------------
% 0.51/1.43 fof(t146_relat_1, conjecture, ! [_59968] : (relation(_59968) => relation_image(_59968, relation_dom(_59968)) = relation_rng(_59968)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t146_relat_1)).
% 0.51/1.43 fof(d13_relat_1, axiom, ! [_60180] : (relation(_60180) => ! [_60195, _60198] : (_60198 = relation_image(_60180, _60195) <=> ! [_60219] : (in(_60219, _60198) <=> ? [_60237] : (in(ordered_pair(_60237, _60219), _60180) & in(_60237, _60195))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d13_relat_1)).
% 0.51/1.43 fof(d4_relat_1, axiom, ! [_60541] : (relation(_60541) => ! [_60556] : (_60556 = relation_dom(_60541) <=> ! [_60574] : (in(_60574, _60556) <=> ? [_60592] : in(ordered_pair(_60574, _60592), _60541)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d4_relat_1)).
% 0.51/1.43 fof(d5_relat_1, axiom, ! [_60840] : (relation(_60840) => ! [_60855] : (_60855 = relation_rng(_60840) <=> ! [_60873] : (in(_60873, _60855) <=> ? [_60891] : in(ordered_pair(_60891, _60873), _60840)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d5_relat_1)).
% 0.51/1.43
% 0.51/1.43 cnf(1, plain, [-(relation(18 ^ []))], clausify(t146_relat_1)).
% 0.51/1.43 cnf(2, plain, [relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_rng(18 ^ [])], clausify(t146_relat_1)).
% 0.51/1.43 cnf(3, plain, [-(relation_image(_20761, _20894) = relation_image(_20828, _20959)), _20761 = _20828, _20894 = _20959], theory(equality)).
% 0.51/1.43 cnf(4, plain, [-(_15976 = _15976)], theory(equality)).
% 0.51/1.43 cnf(5, plain, [relation(_24029), _24227 = relation_image(_24029, _24150), in(_24399, _24227), -(in(ordered_pair(1 ^ [_24399, _24227, _24150, _24029], _24399), _24029))], clausify(d13_relat_1)).
% 0.51/1.43 cnf(6, plain, [relation(_24029), _24227 = relation_image(_24029, _24150), -(in(_24399, _24227)), in(ordered_pair(_24525, _24399), _24029), in(_24525, _24150)], clausify(d13_relat_1)).
% 0.51/1.43 cnf(7, plain, [relation(_25369), _25478 = relation_dom(_25369), -(in(_25618, _25478)), in(ordered_pair(_25618, _25734), _25369)], clausify(d4_relat_1)).
% 0.51/1.43 cnf(8, plain, [relation(_26026), -(_26135 = relation_rng(_26026)), in(9 ^ [_26135, _26026], _26135), in(ordered_pair(_39139, 9 ^ [_26135, _26026]), _26026)], clausify(d5_relat_1)).
% 0.51/1.43 cnf(9, plain, [relation(_26026), -(_26135 = relation_rng(_26026)), -(in(9 ^ [_26135, _26026], _26135)), -(in(ordered_pair(10 ^ [_26135, _26026], 9 ^ [_26135, _26026]), _26026))], clausify(d5_relat_1)).
% 0.51/1.43
% 0.51/1.43 cnf('1',plain,[relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_rng(18 ^ [])],start(2)).
% 0.51/1.43 cnf('1.1',plain,[-(relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_rng(18 ^ [])), relation(18 ^ []), in(9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_image(18 ^ [], relation_dom(18 ^ []))), in(ordered_pair(10 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], 9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []]), 18 ^ [])],extension(8,bind([[_39139, _26135, _26026], [10 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []]]))).
% 0.51/1.43 cnf('1.1.1',plain,[-(relation(18 ^ []))],extension(1)).
% 0.51/1.43 cnf('1.1.2',plain,[-(in(9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_image(18 ^ [], relation_dom(18 ^ [])))), relation(18 ^ []), relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_image(18 ^ [], relation_dom(18 ^ [])), in(ordered_pair(10 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], 9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []]), 18 ^ []), in(10 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_dom(18 ^ []))],extension(6,bind([[_24227, _24399, _24029, _24525, _24150], [relation_image(18 ^ [], relation_dom(18 ^ [])), 9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], 18 ^ [], 10 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_dom(18 ^ [])]]))).
% 0.51/1.43 cnf('1.1.2.1',plain,[-(relation(18 ^ []))],extension(1)).
% 0.51/1.43 cnf('1.1.2.2',plain,[-(relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_image(18 ^ [], relation_dom(18 ^ []))), 18 ^ [] = 18 ^ [], relation_dom(18 ^ []) = relation_dom(18 ^ [])],extension(3,bind([[_20761, _20828, _20894, _20959], [18 ^ [], 18 ^ [], relation_dom(18 ^ []), relation_dom(18 ^ [])]]))).
% 0.51/1.43 cnf('1.1.2.2.1',plain,[-(18 ^ [] = 18 ^ [])],extension(4,bind([[_15976], [18 ^ []]]))).
% 0.51/1.43 cnf('1.1.2.2.2',plain,[-(relation_dom(18 ^ []) = relation_dom(18 ^ []))],extension(4,bind([[_15976], [relation_dom(18 ^ [])]]))).
% 0.51/1.43 cnf('1.1.2.3',plain,[-(in(ordered_pair(10 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], 9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []]), 18 ^ [])), relation(18 ^ []), -(relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_rng(18 ^ [])), -(in(9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_image(18 ^ [], relation_dom(18 ^ []))))],extension(9,bind([[_26026, _26135], [18 ^ [], relation_image(18 ^ [], relation_dom(18 ^ []))]]))).
% 0.51/1.43 cnf('1.1.2.3.1',plain,[-(relation(18 ^ []))],extension(1)).
% 0.51/1.43 cnf('1.1.2.3.2',plain,[relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_rng(18 ^ [])],extension(2)).
% 0.51/1.43 cnf('1.1.2.3.3',plain,[in(9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_image(18 ^ [], relation_dom(18 ^ [])))],reduction('1.1')).
% 0.51/1.43 cnf('1.1.2.4',plain,[-(in(10 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_dom(18 ^ []))), relation(18 ^ []), relation_dom(18 ^ []) = relation_dom(18 ^ []), in(ordered_pair(10 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], 9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []]), 18 ^ [])],extension(7,bind([[_25478, _25618, _25734, _25369], [relation_dom(18 ^ []), 10 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], 9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], 18 ^ []]]))).
% 0.51/1.43 cnf('1.1.2.4.1',plain,[-(relation(18 ^ []))],extension(1)).
% 0.51/1.43 cnf('1.1.2.4.2',plain,[-(relation_dom(18 ^ []) = relation_dom(18 ^ []))],extension(4,bind([[_15976], [relation_dom(18 ^ [])]]))).
% 0.51/1.43 cnf('1.1.2.4.3',plain,[-(in(ordered_pair(10 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], 9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []]), 18 ^ [])), relation(18 ^ []), -(relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_rng(18 ^ [])), -(in(9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_image(18 ^ [], relation_dom(18 ^ []))))],extension(9,bind([[_26026, _26135], [18 ^ [], relation_image(18 ^ [], relation_dom(18 ^ []))]]))).
% 0.51/1.43 cnf('1.1.2.4.3.1',plain,[-(relation(18 ^ []))],extension(1)).
% 0.51/1.43 cnf('1.1.2.4.3.2',plain,[relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_rng(18 ^ [])],extension(2)).
% 0.51/1.43 cnf('1.1.2.4.3.3',plain,[in(9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_image(18 ^ [], relation_dom(18 ^ [])))],reduction('1.1')).
% 0.51/1.43 cnf('1.1.3',plain,[-(in(ordered_pair(10 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], 9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []]), 18 ^ [])), relation(18 ^ []), -(relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_rng(18 ^ [])), -(in(9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_image(18 ^ [], relation_dom(18 ^ []))))],extension(9,bind([[_26026, _26135], [18 ^ [], relation_image(18 ^ [], relation_dom(18 ^ []))]]))).
% 0.51/1.43 cnf('1.1.3.1',plain,[-(relation(18 ^ []))],extension(1)).
% 0.51/1.43 cnf('1.1.3.2',plain,[relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_rng(18 ^ [])],extension(2)).
% 0.51/1.43 cnf('1.1.3.3',plain,[in(9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_image(18 ^ [], relation_dom(18 ^ []))), relation(18 ^ []), relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_image(18 ^ [], relation_dom(18 ^ [])), -(in(ordered_pair(1 ^ [9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_image(18 ^ [], relation_dom(18 ^ [])), relation_dom(18 ^ []), 18 ^ []], 9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []]), 18 ^ []))],extension(5,bind([[_24227, _24150, _24399, _24029], [relation_image(18 ^ [], relation_dom(18 ^ [])), relation_dom(18 ^ []), 9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], 18 ^ []]]))).
% 0.51/1.43 cnf('1.1.3.3.1',plain,[-(relation(18 ^ []))],extension(1)).
% 0.51/1.43 cnf('1.1.3.3.2',plain,[-(relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_image(18 ^ [], relation_dom(18 ^ [])))],extension(4,bind([[_15976], [relation_image(18 ^ [], relation_dom(18 ^ []))]]))).
% 0.51/1.43 cnf('1.1.3.3.3',plain,[in(ordered_pair(1 ^ [9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_image(18 ^ [], relation_dom(18 ^ [])), relation_dom(18 ^ []), 18 ^ []], 9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []]), 18 ^ []), relation(18 ^ []), -(relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_rng(18 ^ [])), in(9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_image(18 ^ [], relation_dom(18 ^ [])))],extension(8,bind([[_39139, _26026, _26135], [1 ^ [9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_image(18 ^ [], relation_dom(18 ^ [])), relation_dom(18 ^ []), 18 ^ []], 18 ^ [], relation_image(18 ^ [], relation_dom(18 ^ []))]]))).
% 0.51/1.43 cnf('1.1.3.3.3.1',plain,[-(relation(18 ^ []))],extension(1)).
% 0.51/1.43 cnf('1.1.3.3.3.2',plain,[relation_image(18 ^ [], relation_dom(18 ^ [])) = relation_rng(18 ^ [])],extension(2)).
% 0.51/1.43 cnf('1.1.3.3.3.3',plain,[-(in(9 ^ [relation_image(18 ^ [], relation_dom(18 ^ [])), 18 ^ []], relation_image(18 ^ [], relation_dom(18 ^ []))))],lemmata('1.1')).
% 0.51/1.43 %-----------------------------------------------------
% 0.51/1.44
% 0.51/1.44 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------