%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU209+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n009.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:01 EDT 2022
% Result : Theorem 0.38s 1.40s
% Output : Proof 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU209+1 : TPTP v8.1.0. Released v3.3.0.
% 0.07/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n009.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sun Jun 19 18:55:22 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.38/1.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/1.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/1.41
% 0.38/1.41 %-----------------------------------------------------
% 0.38/1.41 fof(t167_relat_1, conjecture, ! [_46794, _46797] : (relation(_46797) => subset(relation_inverse_image(_46797, _46794), relation_dom(_46797))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t167_relat_1)).
% 0.38/1.41 fof(d14_relat_1, axiom, ! [_47008] : (relation(_47008) => ! [_47023, _47026] : (_47026 = relation_inverse_image(_47008, _47023) <=> ! [_47047] : (in(_47047, _47026) <=> ? [_47065] : (in(ordered_pair(_47047, _47065), _47008) & in(_47065, _47023))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d14_relat_1)).
% 0.38/1.41 fof(d3_tarski, axiom, ! [_47354, _47357] : (subset(_47354, _47357) <=> ! [_47375] : (in(_47375, _47354) => in(_47375, _47357))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d3_tarski)).
% 0.38/1.41 fof(d4_relat_1, axiom, ! [_47572] : (relation(_47572) => ! [_47587] : (_47587 = relation_dom(_47572) <=> ! [_47605] : (in(_47605, _47587) <=> ? [_47623] : in(ordered_pair(_47605, _47623), _47572)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d4_relat_1)).
% 0.38/1.41
% 0.38/1.41 cnf(1, plain, [-(relation(16 ^ []))], clausify(t167_relat_1)).
% 0.38/1.41 cnf(2, plain, [subset(relation_inverse_image(16 ^ [], 15 ^ []), relation_dom(16 ^ []))], clausify(t167_relat_1)).
% 0.38/1.41 cnf(3, plain, [-(relation_inverse_image(_18537, _18670) = relation_inverse_image(_18604, _18735)), _18537 = _18604, _18670 = _18735], theory(equality)).
% 0.38/1.41 cnf(4, plain, [-(_13752 = _13752)], theory(equality)).
% 0.38/1.41 cnf(5, plain, [relation(_21065), _21263 = relation_inverse_image(_21065, _21186), in(_21435, _21263), -(in(ordered_pair(_21435, 1 ^ [_21435, _21263, _21186, _21065]), _21065))], clausify(d14_relat_1)).
% 0.38/1.41 cnf(6, plain, [-(subset(_21944, _22000)), -(in(4 ^ [_22000, _21944], _21944))], clausify(d3_tarski)).
% 0.38/1.41 cnf(7, plain, [-(subset(_21944, _22000)), in(4 ^ [_22000, _21944], _22000)], clausify(d3_tarski)).
% 0.38/1.41 cnf(8, plain, [relation(_22405), _22514 = relation_dom(_22405), -(in(_22654, _22514)), in(ordered_pair(_22654, _22770), _22405)], clausify(d4_relat_1)).
% 0.38/1.41
% 0.38/1.41 cnf('1',plain,[subset(relation_inverse_image(16 ^ [], 15 ^ []), relation_dom(16 ^ []))],start(2)).
% 0.38/1.41 cnf('1.1',plain,[-(subset(relation_inverse_image(16 ^ [], 15 ^ []), relation_dom(16 ^ []))), -(in(4 ^ [relation_dom(16 ^ []), relation_inverse_image(16 ^ [], 15 ^ [])], relation_inverse_image(16 ^ [], 15 ^ [])))],extension(6,bind([[_22000, _21944], [relation_dom(16 ^ []), relation_inverse_image(16 ^ [], 15 ^ [])]]))).
% 0.38/1.41 cnf('1.1.1',plain,[in(4 ^ [relation_dom(16 ^ []), relation_inverse_image(16 ^ [], 15 ^ [])], relation_inverse_image(16 ^ [], 15 ^ [])), relation(16 ^ []), relation_inverse_image(16 ^ [], 15 ^ []) = relation_inverse_image(16 ^ [], 15 ^ []), -(in(ordered_pair(4 ^ [relation_dom(16 ^ []), relation_inverse_image(16 ^ [], 15 ^ [])], 1 ^ [4 ^ [relation_dom(16 ^ []), relation_inverse_image(16 ^ [], 15 ^ [])], relation_inverse_image(16 ^ [], 15 ^ []), 15 ^ [], 16 ^ []]), 16 ^ []))],extension(5,bind([[_21435, _21263, _21186, _21065], [4 ^ [relation_dom(16 ^ []), relation_inverse_image(16 ^ [], 15 ^ [])], relation_inverse_image(16 ^ [], 15 ^ []), 15 ^ [], 16 ^ []]]))).
% 0.38/1.41 cnf('1.1.1.1',plain,[-(relation(16 ^ []))],extension(1)).
% 0.38/1.41 cnf('1.1.1.2',plain,[-(relation_inverse_image(16 ^ [], 15 ^ []) = relation_inverse_image(16 ^ [], 15 ^ [])), 16 ^ [] = 16 ^ [], 15 ^ [] = 15 ^ []],extension(3,bind([[_18537, _18604, _18670, _18735], [16 ^ [], 16 ^ [], 15 ^ [], 15 ^ []]]))).
% 0.38/1.41 cnf('1.1.1.2.1',plain,[-(16 ^ [] = 16 ^ [])],extension(4,bind([[_13752], [16 ^ []]]))).
% 0.38/1.41 cnf('1.1.1.2.2',plain,[-(15 ^ [] = 15 ^ [])],extension(4,bind([[_13752], [15 ^ []]]))).
% 0.38/1.41 cnf('1.1.1.3',plain,[in(ordered_pair(4 ^ [relation_dom(16 ^ []), relation_inverse_image(16 ^ [], 15 ^ [])], 1 ^ [4 ^ [relation_dom(16 ^ []), relation_inverse_image(16 ^ [], 15 ^ [])], relation_inverse_image(16 ^ [], 15 ^ []), 15 ^ [], 16 ^ []]), 16 ^ []), relation(16 ^ []), relation_dom(16 ^ []) = relation_dom(16 ^ []), -(in(4 ^ [relation_dom(16 ^ []), relation_inverse_image(16 ^ [], 15 ^ [])], relation_dom(16 ^ [])))],extension(8,bind([[_22770, _22405, _22654, _22514], [1 ^ [4 ^ [relation_dom(16 ^ []), relation_inverse_image(16 ^ [], 15 ^ [])], relation_inverse_image(16 ^ [], 15 ^ []), 15 ^ [], 16 ^ []], 16 ^ [], 4 ^ [relation_dom(16 ^ []), relation_inverse_image(16 ^ [], 15 ^ [])], relation_dom(16 ^ [])]]))).
% 0.38/1.41 cnf('1.1.1.3.1',plain,[-(relation(16 ^ []))],extension(1)).
% 0.38/1.41 cnf('1.1.1.3.2',plain,[-(relation_dom(16 ^ []) = relation_dom(16 ^ []))],extension(4,bind([[_13752], [relation_dom(16 ^ [])]]))).
% 0.38/1.41 cnf('1.1.1.3.3',plain,[in(4 ^ [relation_dom(16 ^ []), relation_inverse_image(16 ^ [], 15 ^ [])], relation_dom(16 ^ [])), -(subset(relation_inverse_image(16 ^ [], 15 ^ []), relation_dom(16 ^ [])))],extension(7,bind([[_21944, _22000], [relation_inverse_image(16 ^ [], 15 ^ []), relation_dom(16 ^ [])]]))).
% 0.38/1.41 cnf('1.1.1.3.3.1',plain,[subset(relation_inverse_image(16 ^ [], 15 ^ []), relation_dom(16 ^ []))],extension(2)).
% 0.38/1.41 %-----------------------------------------------------
% 0.38/1.42
% 0.38/1.42 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------