%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU174+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n026.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:44 EDT 2022
% Result : Theorem 115.19s 111.20s
% Output : Proof 115.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU174+1 : TPTP v8.1.0. Released v3.3.0.
% 0.07/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n026.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 04:02:25 EDT 2022
% 0.12/0.34 % CPUTime :
% 115.19/111.20 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 115.19/111.21 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 115.19/111.21
% 115.19/111.21 %-----------------------------------------------------
% 115.19/111.21 fof(t46_setfam_1, conjecture, ! [_43989, _43992] : (element(_43992, powerset(powerset(_43989))) => ~ ((! _43992) = empty_set & complements_of_subsets(_43989, _43992) = empty_set)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t46_setfam_1)).
% 115.19/111.21 fof(d8_setfam_1, axiom, ! [_44295, _44298] : (element(_44298, powerset(powerset(_44295))) => ! [_44324] : (element(_44324, powerset(powerset(_44295))) => (_44324 = complements_of_subsets(_44295, _44298) <=> ! [_44363] : (element(_44363, powerset(_44295)) => (in(_44363, _44324) <=> in(subset_complement(_44295, _44363), _44298)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d8_setfam_1)).
% 115.19/111.21 fof(dt_k7_setfam_1, axiom, ! [_44701, _44704] : (element(_44704, powerset(powerset(_44701))) => element(complements_of_subsets(_44701, _44704), powerset(powerset(_44701)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', dt_k7_setfam_1)).
% 115.19/111.21 fof(fc1_xboole_0, axiom, empty(empty_set), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fc1_xboole_0)).
% 115.19/111.21 fof(involutiveness_k7_setfam_1, axiom, ! [_44949, _44952] : (element(_44952, powerset(powerset(_44949))) => complements_of_subsets(_44949, complements_of_subsets(_44949, _44952)) = _44952), file('/export/starexec/sandbox/benchmark/theBenchmark.p', involutiveness_k7_setfam_1)).
% 115.19/111.21 fof(t7_boole, axiom, ! [_45155, _45158] : ~ (in(_45155, _45158) & empty(_45158)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t7_boole)).
% 115.19/111.21
% 115.19/111.21 cnf(1, plain, [-(element(9 ^ [], powerset(powerset(8 ^ []))))], clausify(t46_setfam_1)).
% 115.19/111.21 cnf(2, plain, [9 ^ [] = empty_set], clausify(t46_setfam_1)).
% 115.19/111.21 cnf(3, plain, [-(complements_of_subsets(8 ^ [], 9 ^ []) = empty_set)], clausify(t46_setfam_1)).
% 115.19/111.21 cnf(4, plain, [-(complements_of_subsets(_14545, _14678) = complements_of_subsets(_14612, _14743)), _14545 = _14612, _14678 = _14743], theory(equality)).
% 115.19/111.21 cnf(5, plain, [-(_11386 = _11386)], theory(equality)).
% 115.19/111.21 cnf(6, plain, [_11539 = _11584, -(_11584 = _11539)], theory(equality)).
% 115.19/111.21 cnf(7, plain, [-(_11818 = _11929), _11818 = _11874, _11874 = _11929], theory(equality)).
% 115.19/111.21 cnf(8, plain, [-(element(_12361, _12492)), element(_12294, _12427), _12294 = _12361, _12427 = _12492], theory(equality)).
% 115.19/111.21 cnf(9, plain, [element(_17064, powerset(powerset(_16969))), element(_17249, powerset(powerset(_16969))), -(_17249 = complements_of_subsets(_16969, _17064)), in(2 ^ [_17249, _17064, _16969], _17249), in(subset_complement(_16969, 2 ^ [_17249, _17064, _16969]), _17064)], clausify(d8_setfam_1)).
% 115.19/111.21 cnf(10, plain, [element(_17064, powerset(powerset(_16969))), element(_17249, powerset(powerset(_16969))), -(_17249 = complements_of_subsets(_16969, _17064)), -(in(2 ^ [_17249, _17064, _16969], _17249)), -(in(subset_complement(_16969, 2 ^ [_17249, _17064, _16969]), _17064))], clausify(d8_setfam_1)).
% 115.19/111.21 cnf(11, plain, [element(_18704, powerset(powerset(_18648))), -(element(complements_of_subsets(_18648, _18704), powerset(powerset(_18648))))], clausify(dt_k7_setfam_1)).
% 115.19/111.21 cnf(12, plain, [-(empty(empty_set))], clausify(fc1_xboole_0)).
% 115.19/111.21 cnf(13, plain, [element(_20210, powerset(powerset(_20155))), -(complements_of_subsets(_20155, complements_of_subsets(_20155, _20210)) = _20210)], clausify(involutiveness_k7_setfam_1)).
% 115.19/111.21 cnf(14, plain, [in(_24072, _24118), empty(_24118)], clausify(t7_boole)).
% 115.19/111.21
% 115.19/111.21 cnf('1',plain,[9 ^ [] = empty_set],start(2)).
% 115.19/111.21 cnf('1.1',plain,[-(9 ^ [] = empty_set), empty_set = 9 ^ []],extension(6,bind([[_11539, _11584], [empty_set, 9 ^ []]]))).
% 115.19/111.21 cnf('1.1.1',plain,[-(empty_set = 9 ^ []), empty_set = complements_of_subsets(8 ^ [], empty_set), complements_of_subsets(8 ^ [], empty_set) = 9 ^ []],extension(7,bind([[_11818, _11874, _11929], [empty_set, complements_of_subsets(8 ^ [], empty_set), 9 ^ []]]))).
% 115.19/111.21 cnf('1.1.1.1',plain,[-(empty_set = complements_of_subsets(8 ^ [], empty_set)), element(empty_set, powerset(powerset(8 ^ []))), element(empty_set, powerset(powerset(8 ^ []))), in(2 ^ [empty_set, empty_set, 8 ^ []], empty_set), in(subset_complement(8 ^ [], 2 ^ [empty_set, empty_set, 8 ^ []]), empty_set)],extension(9,bind([[_17249, _16969, _17064], [empty_set, 8 ^ [], empty_set]]))).
% 115.19/111.21 cnf('1.1.1.1.1',plain,[-(element(empty_set, powerset(powerset(8 ^ [])))), element(complements_of_subsets(8 ^ [], 9 ^ []), powerset(powerset(8 ^ []))), complements_of_subsets(8 ^ [], 9 ^ []) = empty_set, powerset(powerset(8 ^ [])) = powerset(powerset(8 ^ []))],extension(8,bind([[_12294, _12361, _12427, _12492], [complements_of_subsets(8 ^ [], 9 ^ []), empty_set, powerset(powerset(8 ^ [])), powerset(powerset(8 ^ []))]]))).
% 115.19/111.21 cnf('1.1.1.1.1.1',plain,[-(element(complements_of_subsets(8 ^ [], 9 ^ []), powerset(powerset(8 ^ [])))), element(9 ^ [], powerset(powerset(8 ^ [])))],extension(11,bind([[_18704, _18648], [9 ^ [], 8 ^ []]]))).
% 115.19/111.21 cnf('1.1.1.1.1.1.1',plain,[-(element(9 ^ [], powerset(powerset(8 ^ []))))],extension(1)).
% 115.19/111.21 cnf('1.1.1.1.1.2',plain,[-(complements_of_subsets(8 ^ [], 9 ^ []) = empty_set)],extension(3)).
% 115.19/111.21 cnf('1.1.1.1.1.3',plain,[-(powerset(powerset(8 ^ [])) = powerset(powerset(8 ^ [])))],extension(5,bind([[_11386], [powerset(powerset(8 ^ []))]]))).
% 115.19/111.21 cnf('1.1.1.1.2',plain,[-(element(empty_set, powerset(powerset(8 ^ []))))],lemmata('1.1.1.1')).
% 115.19/111.21 cnf('1.1.1.1.3',plain,[-(in(2 ^ [empty_set, empty_set, 8 ^ []], empty_set)), element(empty_set, powerset(powerset(8 ^ []))), element(empty_set, powerset(powerset(8 ^ []))), -(empty_set = complements_of_subsets(8 ^ [], empty_set)), -(in(subset_complement(8 ^ [], 2 ^ [empty_set, empty_set, 8 ^ []]), empty_set))],extension(10,bind([[_17249, _16969, _17064], [empty_set, 8 ^ [], empty_set]]))).
% 115.19/111.21 cnf('1.1.1.1.3.1',plain,[-(element(empty_set, powerset(powerset(8 ^ []))))],lemmata('1.1.1.1')).
% 115.19/111.21 cnf('1.1.1.1.3.2',plain,[-(element(empty_set, powerset(powerset(8 ^ []))))],lemmata('1.1.1.1.3')).
% 115.19/111.21 cnf('1.1.1.1.3.3',plain,[empty_set = complements_of_subsets(8 ^ [], empty_set)],reduction('1.1.1')).
% 115.19/111.21 cnf('1.1.1.1.3.4',plain,[in(subset_complement(8 ^ [], 2 ^ [empty_set, empty_set, 8 ^ []]), empty_set), empty(empty_set)],extension(14,bind([[_24072, _24118], [subset_complement(8 ^ [], 2 ^ [empty_set, empty_set, 8 ^ []]), empty_set]]))).
% 115.19/111.21 cnf('1.1.1.1.3.4.1',plain,[-(empty(empty_set))],extension(12)).
% 115.19/111.21 cnf('1.1.1.1.4',plain,[-(in(subset_complement(8 ^ [], 2 ^ [empty_set, empty_set, 8 ^ []]), empty_set)), element(empty_set, powerset(powerset(8 ^ []))), element(empty_set, powerset(powerset(8 ^ []))), -(empty_set = complements_of_subsets(8 ^ [], empty_set)), -(in(2 ^ [empty_set, empty_set, 8 ^ []], empty_set))],extension(10,bind([[_17064, _16969, _17249], [empty_set, 8 ^ [], empty_set]]))).
% 115.19/111.21 cnf('1.1.1.1.4.1',plain,[-(element(empty_set, powerset(powerset(8 ^ []))))],lemmata('1.1.1.1')).
% 115.19/111.21 cnf('1.1.1.1.4.2',plain,[-(element(empty_set, powerset(powerset(8 ^ []))))],lemmata('1.1.1.1.4')).
% 115.19/111.21 cnf('1.1.1.1.4.3',plain,[empty_set = complements_of_subsets(8 ^ [], empty_set)],reduction('1.1.1')).
% 115.19/111.21 cnf('1.1.1.1.4.4',plain,[in(2 ^ [empty_set, empty_set, 8 ^ []], empty_set), empty(empty_set)],extension(14,bind([[_24072, _24118], [2 ^ [empty_set, empty_set, 8 ^ []], empty_set]]))).
% 115.19/111.21 cnf('1.1.1.1.4.4.1',plain,[-(empty(empty_set))],extension(12)).
% 115.19/111.21 cnf('1.1.1.2',plain,[-(complements_of_subsets(8 ^ [], empty_set) = 9 ^ []), complements_of_subsets(8 ^ [], empty_set) = complements_of_subsets(8 ^ [], complements_of_subsets(8 ^ [], 9 ^ [])), complements_of_subsets(8 ^ [], complements_of_subsets(8 ^ [], 9 ^ [])) = 9 ^ []],extension(7,bind([[_11818, _11874, _11929], [complements_of_subsets(8 ^ [], empty_set), complements_of_subsets(8 ^ [], complements_of_subsets(8 ^ [], 9 ^ [])), 9 ^ []]]))).
% 115.19/111.21 cnf('1.1.1.2.1',plain,[-(complements_of_subsets(8 ^ [], empty_set) = complements_of_subsets(8 ^ [], complements_of_subsets(8 ^ [], 9 ^ []))), 8 ^ [] = 8 ^ [], empty_set = complements_of_subsets(8 ^ [], 9 ^ [])],extension(4,bind([[_14545, _14612, _14678, _14743], [8 ^ [], 8 ^ [], empty_set, complements_of_subsets(8 ^ [], 9 ^ [])]]))).
% 115.19/111.21 cnf('1.1.1.2.1.1',plain,[-(8 ^ [] = 8 ^ [])],extension(5,bind([[_11386], [8 ^ []]]))).
% 115.19/111.21 cnf('1.1.1.2.1.2',plain,[-(empty_set = complements_of_subsets(8 ^ [], 9 ^ [])), complements_of_subsets(8 ^ [], 9 ^ []) = empty_set],extension(6,bind([[_11539, _11584], [complements_of_subsets(8 ^ [], 9 ^ []), empty_set]]))).
% 115.19/111.21 cnf('1.1.1.2.1.2.1',plain,[-(complements_of_subsets(8 ^ [], 9 ^ []) = empty_set)],extension(3)).
% 115.19/111.21 cnf('1.1.1.2.2',plain,[-(complements_of_subsets(8 ^ [], complements_of_subsets(8 ^ [], 9 ^ [])) = 9 ^ []), complements_of_subsets(8 ^ [], complements_of_subsets(8 ^ [], 9 ^ [])) = 9 ^ [], 9 ^ [] = 9 ^ []],extension(7,bind([[_11818, _11874, _11929], [complements_of_subsets(8 ^ [], complements_of_subsets(8 ^ [], 9 ^ [])), 9 ^ [], 9 ^ []]]))).
% 115.19/111.21 cnf('1.1.1.2.2.1',plain,[-(complements_of_subsets(8 ^ [], complements_of_subsets(8 ^ [], 9 ^ [])) = 9 ^ []), element(9 ^ [], powerset(powerset(8 ^ [])))],extension(13,bind([[_20210, _20155], [9 ^ [], 8 ^ []]]))).
% 115.19/111.21 cnf('1.1.1.2.2.1.1',plain,[-(element(9 ^ [], powerset(powerset(8 ^ []))))],extension(1)).
% 115.19/111.21 cnf('1.1.1.2.2.2',plain,[-(9 ^ [] = 9 ^ [])],extension(5,bind([[_11386], [9 ^ []]]))).
% 115.19/111.21 %-----------------------------------------------------
% 115.19/111.22
% 115.19/111.22 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------