%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU157+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n007.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:33 EDT 2022
% Result : Theorem 72.34s 70.68s
% Output : Proof 72.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU157+1 : TPTP v8.1.0. Released v3.3.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n007.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 11:09:29 EDT 2022
% 0.12/0.33 % CPUTime :
% 72.34/70.68 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 72.34/70.69 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 72.34/70.69
% 72.34/70.69 %-----------------------------------------------------
% 72.34/70.69 fof(l55_zfmisc_1, conjecture, ! [_33892, _33895, _33898, _33901] : (in(ordered_pair(_33892, _33895), cartesian_product2(_33898, _33901)) <=> in(_33892, _33898) & in(_33895, _33901)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', l55_zfmisc_1)).
% 72.34/70.69 fof(t33_zfmisc_1, axiom, ! [_34212, _34215, _34218, _34221] : (ordered_pair(_34212, _34215) = ordered_pair(_34218, _34221) => _34212 = _34218 & _34215 = _34221), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t33_zfmisc_1)).
% 72.34/70.69 fof(d2_zfmisc_1, axiom, ! [_34440, _34443, _34446] : (_34446 = cartesian_product2(_34440, _34443) <=> ! [_34467] : (in(_34467, _34446) <=> ? [_34485, _34488] : (in(_34485, _34440) & in(_34488, _34443) & _34467 = ordered_pair(_34485, _34488)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d2_zfmisc_1)).
% 72.34/70.69
% 72.34/70.69 cnf(1, plain, [-(in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []))), -(in(8 ^ [], 10 ^ []))], clausify(l55_zfmisc_1)).
% 72.34/70.69 cnf(2, plain, [-(in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []))), -(in(9 ^ [], 11 ^ []))], clausify(l55_zfmisc_1)).
% 72.34/70.69 cnf(3, plain, [in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ [])), in(8 ^ [], 10 ^ []), in(9 ^ [], 11 ^ [])], clausify(l55_zfmisc_1)).
% 72.34/70.69 cnf(4, plain, [-(cartesian_product2(_8370, _8503) = cartesian_product2(_8437, _8568)), _8370 = _8437, _8503 = _8568], theory(equality)).
% 72.34/70.69 cnf(5, plain, [-(ordered_pair(_8994, _9127) = ordered_pair(_9061, _9192)), _8994 = _9061, _9127 = _9192], theory(equality)).
% 72.34/70.69 cnf(6, plain, [-(_6489 = _6489)], theory(equality)).
% 72.34/70.69 cnf(7, plain, [_6642 = _6687, -(_6687 = _6642)], theory(equality)).
% 72.34/70.69 cnf(8, plain, [-(in(_7783, _7914)), in(_7716, _7849), _7716 = _7783, _7849 = _7914], theory(equality)).
% 72.34/70.69 cnf(9, plain, [ordered_pair(_13792, _13859) = ordered_pair(_13925, _13990), -(_13792 = _13925)], clausify(t33_zfmisc_1)).
% 72.34/70.69 cnf(10, plain, [ordered_pair(_13792, _13859) = ordered_pair(_13925, _13990), -(_13859 = _13990)], clausify(t33_zfmisc_1)).
% 72.34/70.69 cnf(11, plain, [_11459 = cartesian_product2(_11282, _11371), in(_11642, _11459), -(in(1 ^ [_11642, _11459, _11371, _11282], _11282))], clausify(d2_zfmisc_1)).
% 72.34/70.69 cnf(12, plain, [_11459 = cartesian_product2(_11282, _11371), in(_11642, _11459), -(in(2 ^ [_11642, _11459, _11371, _11282], _11371))], clausify(d2_zfmisc_1)).
% 72.34/70.69 cnf(13, plain, [_11459 = cartesian_product2(_11282, _11371), in(_11642, _11459), -(_11642 = ordered_pair(1 ^ [_11642, _11459, _11371, _11282], 2 ^ [_11642, _11459, _11371, _11282]))], clausify(d2_zfmisc_1)).
% 72.34/70.69 cnf(14, plain, [_11459 = cartesian_product2(_11282, _11371), -(in(_11642, _11459)), in(_11779, _11282), in(_11850, _11371), _11642 = ordered_pair(_11779, _11850)], clausify(d2_zfmisc_1)).
% 72.34/70.69
% 72.34/70.69 cnf('1',plain,[in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ [])), in(8 ^ [], 10 ^ []), in(9 ^ [], 11 ^ [])],start(3)).
% 72.34/70.69 cnf('1.1',plain,[-(in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []))), cartesian_product2(10 ^ [], 11 ^ []) = cartesian_product2(10 ^ [], 11 ^ []), in(8 ^ [], 10 ^ []), in(9 ^ [], 11 ^ []), ordered_pair(8 ^ [], 9 ^ []) = ordered_pair(8 ^ [], 9 ^ [])],extension(14,bind([[_11459, _11282, _11371, _11642, _11779, _11850], [cartesian_product2(10 ^ [], 11 ^ []), 10 ^ [], 11 ^ [], ordered_pair(8 ^ [], 9 ^ []), 8 ^ [], 9 ^ []]]))).
% 72.34/70.69 cnf('1.1.1',plain,[-(cartesian_product2(10 ^ [], 11 ^ []) = cartesian_product2(10 ^ [], 11 ^ [])), 10 ^ [] = 10 ^ [], 11 ^ [] = 11 ^ []],extension(4,bind([[_8370, _8437, _8503, _8568], [10 ^ [], 10 ^ [], 11 ^ [], 11 ^ []]]))).
% 72.34/70.69 cnf('1.1.1.1',plain,[-(10 ^ [] = 10 ^ [])],extension(6,bind([[_6489], [10 ^ []]]))).
% 72.34/70.69 cnf('1.1.1.2',plain,[-(11 ^ [] = 11 ^ [])],extension(6,bind([[_6489], [11 ^ []]]))).
% 72.34/70.69 cnf('1.1.2',plain,[-(in(8 ^ [], 10 ^ [])), -(in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ [])))],extension(1)).
% 72.34/70.69 cnf('1.1.2.1',plain,[in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []))],reduction('1')).
% 72.34/70.69 cnf('1.1.3',plain,[-(in(9 ^ [], 11 ^ [])), -(in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ [])))],extension(2)).
% 72.34/70.69 cnf('1.1.3.1',plain,[in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []))],reduction('1')).
% 72.34/70.69 cnf('1.1.4',plain,[-(ordered_pair(8 ^ [], 9 ^ []) = ordered_pair(8 ^ [], 9 ^ [])), 8 ^ [] = 8 ^ [], 9 ^ [] = 9 ^ []],extension(5,bind([[_8994, _9061, _9127, _9192], [8 ^ [], 8 ^ [], 9 ^ [], 9 ^ []]]))).
% 72.34/70.69 cnf('1.1.4.1',plain,[-(8 ^ [] = 8 ^ [])],extension(6,bind([[_6489], [8 ^ []]]))).
% 72.34/70.69 cnf('1.1.4.2',plain,[-(9 ^ [] = 9 ^ [])],extension(6,bind([[_6489], [9 ^ []]]))).
% 72.34/70.69 cnf('1.2',plain,[-(in(8 ^ [], 10 ^ [])), -(in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ [])))],extension(1)).
% 72.34/70.69 cnf('1.2.1',plain,[in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ [])), cartesian_product2(10 ^ [], 11 ^ []) = cartesian_product2(10 ^ [], 11 ^ []), -(in(1 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []], 10 ^ []))],extension(11,bind([[_11642, _11459, _11371, _11282], [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []]]))).
% 72.34/70.69 cnf('1.2.1.1',plain,[-(cartesian_product2(10 ^ [], 11 ^ []) = cartesian_product2(10 ^ [], 11 ^ [])), 10 ^ [] = 10 ^ [], 11 ^ [] = 11 ^ []],extension(4,bind([[_8370, _8437, _8503, _8568], [10 ^ [], 10 ^ [], 11 ^ [], 11 ^ []]]))).
% 72.34/70.69 cnf('1.2.1.1.1',plain,[-(10 ^ [] = 10 ^ [])],extension(6,bind([[_6489], [10 ^ []]]))).
% 72.34/70.69 cnf('1.2.1.1.2',plain,[-(11 ^ [] = 11 ^ [])],extension(6,bind([[_6489], [11 ^ []]]))).
% 72.34/70.69 cnf('1.2.1.2',plain,[in(1 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []], 10 ^ []), -(in(8 ^ [], 10 ^ [])), 1 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []] = 8 ^ [], 10 ^ [] = 10 ^ []],extension(8,bind([[_7716, _7783, _7849, _7914], [1 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []], 8 ^ [], 10 ^ [], 10 ^ []]]))).
% 72.34/70.69 cnf('1.2.1.2.1',plain,[in(8 ^ [], 10 ^ [])],reduction('1')).
% 72.34/70.69 cnf('1.2.1.2.2',plain,[-(1 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []] = 8 ^ []), 8 ^ [] = 1 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []]],extension(7,bind([[_6642, _6687], [8 ^ [], 1 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []]]]))).
% 72.34/70.69 cnf('1.2.1.2.2.1',plain,[-(8 ^ [] = 1 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []]), ordered_pair(8 ^ [], 9 ^ []) = ordered_pair(1 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []], 2 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []])],extension(9,bind([[_13792, _13859, _13925, _13990], [8 ^ [], 9 ^ [], 1 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []], 2 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []]]]))).
% 72.34/70.69 cnf('1.2.1.2.2.1.1',plain,[-(ordered_pair(8 ^ [], 9 ^ []) = ordered_pair(1 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []], 2 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []])), cartesian_product2(10 ^ [], 11 ^ []) = cartesian_product2(10 ^ [], 11 ^ []), in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []))],extension(13,bind([[_11282, _11371, _11642, _11459], [10 ^ [], 11 ^ [], ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ [])]]))).
% 72.34/70.69 cnf('1.2.1.2.2.1.1.1',plain,[-(cartesian_product2(10 ^ [], 11 ^ []) = cartesian_product2(10 ^ [], 11 ^ []))],extension(6,bind([[_6489], [cartesian_product2(10 ^ [], 11 ^ [])]]))).
% 72.34/70.69 cnf('1.2.1.2.2.1.1.2',plain,[-(in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ [])))],lemmata('1')).
% 72.34/70.69 cnf('1.2.1.2.3',plain,[-(10 ^ [] = 10 ^ [])],extension(6,bind([[_6489], [10 ^ []]]))).
% 72.34/70.69 cnf('1.3',plain,[-(in(9 ^ [], 11 ^ [])), -(in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ [])))],extension(2)).
% 72.34/70.69 cnf('1.3.1',plain,[in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ [])), cartesian_product2(10 ^ [], 11 ^ []) = cartesian_product2(10 ^ [], 11 ^ []), -(in(2 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []], 11 ^ []))],extension(12,bind([[_11642, _11459, _11282, _11371], [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 10 ^ [], 11 ^ []]]))).
% 72.34/70.69 cnf('1.3.1.1',plain,[-(cartesian_product2(10 ^ [], 11 ^ []) = cartesian_product2(10 ^ [], 11 ^ [])), 10 ^ [] = 10 ^ [], 11 ^ [] = 11 ^ []],extension(4,bind([[_8370, _8437, _8503, _8568], [10 ^ [], 10 ^ [], 11 ^ [], 11 ^ []]]))).
% 72.34/70.69 cnf('1.3.1.1.1',plain,[-(10 ^ [] = 10 ^ [])],extension(6,bind([[_6489], [10 ^ []]]))).
% 72.34/70.69 cnf('1.3.1.1.2',plain,[-(11 ^ [] = 11 ^ [])],extension(6,bind([[_6489], [11 ^ []]]))).
% 72.34/70.69 cnf('1.3.1.2',plain,[in(2 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []], 11 ^ []), -(in(9 ^ [], 11 ^ [])), 2 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []] = 9 ^ [], 11 ^ [] = 11 ^ []],extension(8,bind([[_7716, _7783, _7849, _7914], [2 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []], 9 ^ [], 11 ^ [], 11 ^ []]]))).
% 72.34/70.69 cnf('1.3.1.2.1',plain,[in(9 ^ [], 11 ^ [])],reduction('1')).
% 72.34/70.69 cnf('1.3.1.2.2',plain,[-(2 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []] = 9 ^ []), 9 ^ [] = 2 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []]],extension(7,bind([[_6642, _6687], [9 ^ [], 2 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []]]]))).
% 72.34/70.69 cnf('1.3.1.2.2.1',plain,[-(9 ^ [] = 2 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []]), ordered_pair(8 ^ [], 9 ^ []) = ordered_pair(1 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []], 2 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []])],extension(10,bind([[_13792, _13859, _13925, _13990], [8 ^ [], 9 ^ [], 1 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []], 2 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []]]]))).
% 72.34/70.69 cnf('1.3.1.2.2.1.1',plain,[-(ordered_pair(8 ^ [], 9 ^ []) = ordered_pair(1 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []], 2 ^ [ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []), 11 ^ [], 10 ^ []])), cartesian_product2(10 ^ [], 11 ^ []) = cartesian_product2(10 ^ [], 11 ^ []), in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ []))],extension(13,bind([[_11282, _11371, _11642, _11459], [10 ^ [], 11 ^ [], ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ [])]]))).
% 72.34/70.69 cnf('1.3.1.2.2.1.1.1',plain,[-(cartesian_product2(10 ^ [], 11 ^ []) = cartesian_product2(10 ^ [], 11 ^ []))],extension(6,bind([[_6489], [cartesian_product2(10 ^ [], 11 ^ [])]]))).
% 72.34/70.69 cnf('1.3.1.2.2.1.1.2',plain,[-(in(ordered_pair(8 ^ [], 9 ^ []), cartesian_product2(10 ^ [], 11 ^ [])))],lemmata('1')).
% 72.34/70.69 cnf('1.3.1.2.3',plain,[-(11 ^ [] = 11 ^ [])],extension(6,bind([[_6489], [11 ^ []]]))).
% 72.34/70.69 %-----------------------------------------------------
% 72.34/70.70
% 72.34/70.70 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------