%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU132+2 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n004.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:19 EDT 2022
% Result : Theorem 1.86s 2.43s
% Output : Proof 1.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : SEU132+2 : TPTP v8.1.0. Released v3.3.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n004.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.18/0.33 % DateTime : Sat Jun 18 20:55:38 EDT 2022
% 0.18/0.33 % CPUTime :
% 1.86/2.43 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.86/2.44 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.86/2.44
% 1.86/2.44 %-----------------------------------------------------
% 1.86/2.44 fof(t33_xboole_1, conjecture, ! [_59729, _59732, _59735] : (subset(_59729, _59732) => subset(set_difference(_59729, _59735), set_difference(_59732, _59735))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t33_xboole_1)).
% 1.86/2.44 fof(d1_xboole_0, axiom, ! [_59989] : (_59989 = empty_set <=> ! [_60003] : ~ in(_60003, _59989)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_xboole_0)).
% 1.86/2.44 fof(d2_xboole_0, axiom, ! [_60159, _60162, _60165] : (_60165 = set_union2(_60159, _60162) <=> ! [_60186] : (in(_60186, _60165) <=> in(_60186, _60159) | in(_60186, _60162))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d2_xboole_0)).
% 1.86/2.44 fof(d3_tarski, axiom, ! [_60429, _60432] : (subset(_60429, _60432) <=> ! [_60450] : (in(_60450, _60429) => in(_60450, _60432))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d3_tarski)).
% 1.86/2.44 fof(d4_xboole_0, axiom, ! [_60652, _60655, _60658] : (_60658 = set_difference(_60652, _60655) <=> ! [_60679] : (in(_60679, _60658) <=> in(_60679, _60652) & ~ in(_60679, _60655))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d4_xboole_0)).
% 1.86/2.44 fof(l32_xboole_1, lemma, ! [_60949, _60952] : (set_difference(_60949, _60952) = empty_set <=> subset(_60949, _60952)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', l32_xboole_1)).
% 1.86/2.44
% 1.86/2.44 cnf(1, plain, [-(subset(11 ^ [], 12 ^ []))], clausify(t33_xboole_1)).
% 1.86/2.44 cnf(2, plain, [subset(set_difference(11 ^ [], 13 ^ []), set_difference(12 ^ [], 13 ^ []))], clausify(t33_xboole_1)).
% 1.86/2.44 cnf(3, plain, [-(set_difference(_20029, _20162) = set_difference(_20096, _20227)), _20029 = _20096, _20162 = _20227], theory(equality)).
% 1.86/2.44 cnf(4, plain, [-(set_union2(_21267, _21400) = set_union2(_21334, _21465)), _21267 = _21334, _21400 = _21465], theory(equality)).
% 1.86/2.44 cnf(5, plain, [-(_16870 = _16870)], theory(equality)).
% 1.86/2.44 cnf(6, plain, [_17023 = _17068, -(_17068 = _17023)], theory(equality)).
% 1.86/2.44 cnf(7, plain, [_23303 = empty_set, in(_23409, _23303)], clausify(d1_xboole_0)).
% 1.86/2.44 cnf(8, plain, [_23766 = set_union2(_23627, _23697), -(in(_23930, _23766)), in(_23930, _23697)], clausify(d2_xboole_0)).
% 1.86/2.44 cnf(9, plain, [_23766 = set_union2(_23627, _23697), in(_23930, _23766), -(in(_23930, _23627)), -(in(_23930, _23697))], clausify(d2_xboole_0)).
% 1.86/2.44 cnf(10, plain, [-(subset(_24312, _24368)), -(in(3 ^ [_24368, _24312], _24312))], clausify(d3_tarski)).
% 1.86/2.44 cnf(11, plain, [-(subset(_24312, _24368)), in(3 ^ [_24368, _24312], _24368)], clausify(d3_tarski)).
% 1.86/2.44 cnf(12, plain, [_25601 = set_difference(_25458, _25530), in(_25767, _25601), -(in(_25767, _25458))], clausify(d4_xboole_0)).
% 1.86/2.44 cnf(13, plain, [_25601 = set_difference(_25458, _25530), in(_25767, _25601), in(_25767, _25530)], clausify(d4_xboole_0)).
% 1.86/2.44 cnf(14, plain, [_25601 = set_difference(_25458, _25530), -(in(_25767, _25601)), in(_25767, _25458), -(in(_25767, _25530))], clausify(d4_xboole_0)).
% 1.86/2.44 cnf(15, plain, [-(set_difference(_28392, _28440) = empty_set), subset(_28392, _28440)], clausify(l32_xboole_1)).
% 1.86/2.44
% 1.86/2.44 cnf('1',plain,[empty_set = empty_set, in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], empty_set)],start(7,bind([[_23409, _23303], [3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], empty_set]]))).
% 1.86/2.44 cnf('1.1',plain,[-(empty_set = empty_set)],extension(5,bind([[_16870], [empty_set]]))).
% 1.86/2.44 cnf('1.2',plain,[-(in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], empty_set)), empty_set = set_difference(11 ^ [], 12 ^ []), in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], 11 ^ []), -(in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], 12 ^ []))],extension(14,bind([[_25601, _25458, _25767, _25530], [empty_set, 11 ^ [], 3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], 12 ^ []]]))).
% 1.86/2.44 cnf('1.2.1',plain,[-(empty_set = set_difference(11 ^ [], 12 ^ [])), set_difference(11 ^ [], 12 ^ []) = empty_set],extension(6,bind([[_17023, _17068], [set_difference(11 ^ [], 12 ^ []), empty_set]]))).
% 1.86/2.44 cnf('1.2.1.1',plain,[-(set_difference(11 ^ [], 12 ^ []) = empty_set), subset(11 ^ [], 12 ^ [])],extension(15,bind([[_28392, _28440], [11 ^ [], 12 ^ []]]))).
% 1.86/2.44 cnf('1.2.1.1.1',plain,[-(subset(11 ^ [], 12 ^ []))],extension(1)).
% 1.86/2.44 cnf('1.2.2',plain,[-(in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], 11 ^ [])), set_union2(11 ^ [], set_difference(11 ^ [], 13 ^ [])) = set_union2(11 ^ [], set_difference(11 ^ [], 13 ^ [])), in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], set_union2(11 ^ [], set_difference(11 ^ [], 13 ^ []))), -(in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], set_difference(11 ^ [], 13 ^ [])))],extension(9,bind([[_23627, _23766, _23930, _23697], [11 ^ [], set_union2(11 ^ [], set_difference(11 ^ [], 13 ^ [])), 3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], set_difference(11 ^ [], 13 ^ [])]]))).
% 1.86/2.44 cnf('1.2.2.1',plain,[-(set_union2(11 ^ [], set_difference(11 ^ [], 13 ^ [])) = set_union2(11 ^ [], set_difference(11 ^ [], 13 ^ []))), 11 ^ [] = 11 ^ [], set_difference(11 ^ [], 13 ^ []) = set_difference(11 ^ [], 13 ^ [])],extension(4,bind([[_21267, _21334, _21400, _21465], [11 ^ [], 11 ^ [], set_difference(11 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])]]))).
% 1.86/2.44 cnf('1.2.2.1.1',plain,[-(11 ^ [] = 11 ^ [])],extension(5,bind([[_16870], [11 ^ []]]))).
% 1.86/2.44 cnf('1.2.2.1.2',plain,[-(set_difference(11 ^ [], 13 ^ []) = set_difference(11 ^ [], 13 ^ []))],extension(5,bind([[_16870], [set_difference(11 ^ [], 13 ^ [])]]))).
% 1.86/2.44 cnf('1.2.2.2',plain,[-(in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], set_union2(11 ^ [], set_difference(11 ^ [], 13 ^ [])))), set_union2(11 ^ [], set_difference(11 ^ [], 13 ^ [])) = set_union2(11 ^ [], set_difference(11 ^ [], 13 ^ [])), in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], set_difference(11 ^ [], 13 ^ []))],extension(8,bind([[_23766, _23627, _23930, _23697], [set_union2(11 ^ [], set_difference(11 ^ [], 13 ^ [])), 11 ^ [], 3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], set_difference(11 ^ [], 13 ^ [])]]))).
% 1.86/2.44 cnf('1.2.2.2.1',plain,[-(set_union2(11 ^ [], set_difference(11 ^ [], 13 ^ [])) = set_union2(11 ^ [], set_difference(11 ^ [], 13 ^ [])))],extension(5,bind([[_16870], [set_union2(11 ^ [], set_difference(11 ^ [], 13 ^ []))]]))).
% 1.86/2.44 cnf('1.2.2.2.2',plain,[-(in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], set_difference(11 ^ [], 13 ^ []))), -(subset(set_difference(11 ^ [], 13 ^ []), set_difference(12 ^ [], 13 ^ [])))],extension(10,bind([[_24312, _24368], [set_difference(11 ^ [], 13 ^ []), set_difference(12 ^ [], 13 ^ [])]]))).
% 1.86/2.44 cnf('1.2.2.2.2.1',plain,[subset(set_difference(11 ^ [], 13 ^ []), set_difference(12 ^ [], 13 ^ []))],extension(2)).
% 1.86/2.44 cnf('1.2.2.3',plain,[in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], set_difference(11 ^ [], 13 ^ [])), set_difference(11 ^ [], 13 ^ []) = set_difference(11 ^ [], 13 ^ []), -(in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], 11 ^ []))],extension(12,bind([[_25601, _25530, _25767, _25458], [set_difference(11 ^ [], 13 ^ []), 13 ^ [], 3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], 11 ^ []]]))).
% 1.86/2.44 cnf('1.2.2.3.1',plain,[-(set_difference(11 ^ [], 13 ^ []) = set_difference(11 ^ [], 13 ^ []))],extension(5,bind([[_16870], [set_difference(11 ^ [], 13 ^ [])]]))).
% 1.86/2.44 cnf('1.2.2.3.2',plain,[in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], 11 ^ [])],reduction('1.2')).
% 1.86/2.44 cnf('1.2.3',plain,[in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], 12 ^ []), set_difference(12 ^ [], 13 ^ []) = set_difference(12 ^ [], 13 ^ []), -(in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], set_difference(12 ^ [], 13 ^ []))), -(in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], 13 ^ []))],extension(14,bind([[_25458, _25601, _25767, _25530], [12 ^ [], set_difference(12 ^ [], 13 ^ []), 3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], 13 ^ []]]))).
% 1.86/2.44 cnf('1.2.3.1',plain,[-(set_difference(12 ^ [], 13 ^ []) = set_difference(12 ^ [], 13 ^ [])), 12 ^ [] = 12 ^ [], 13 ^ [] = 13 ^ []],extension(3,bind([[_20029, _20096, _20162, _20227], [12 ^ [], 12 ^ [], 13 ^ [], 13 ^ []]]))).
% 1.86/2.44 cnf('1.2.3.1.1',plain,[-(12 ^ [] = 12 ^ [])],extension(5,bind([[_16870], [12 ^ []]]))).
% 1.86/2.44 cnf('1.2.3.1.2',plain,[-(13 ^ [] = 13 ^ [])],extension(5,bind([[_16870], [13 ^ []]]))).
% 1.86/2.44 cnf('1.2.3.2',plain,[in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], set_difference(12 ^ [], 13 ^ [])), -(subset(set_difference(11 ^ [], 13 ^ []), set_difference(12 ^ [], 13 ^ [])))],extension(11,bind([[_24312, _24368], [set_difference(11 ^ [], 13 ^ []), set_difference(12 ^ [], 13 ^ [])]]))).
% 1.86/2.44 cnf('1.2.3.2.1',plain,[subset(set_difference(11 ^ [], 13 ^ []), set_difference(12 ^ [], 13 ^ []))],extension(2)).
% 1.86/2.44 cnf('1.2.3.3',plain,[in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], 13 ^ []), set_difference(11 ^ [], 13 ^ []) = set_difference(11 ^ [], 13 ^ []), in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], set_difference(11 ^ [], 13 ^ []))],extension(13,bind([[_25458, _25530, _25767, _25601], [11 ^ [], 13 ^ [], 3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], set_difference(11 ^ [], 13 ^ [])]]))).
% 1.86/2.44 cnf('1.2.3.3.1',plain,[-(set_difference(11 ^ [], 13 ^ []) = set_difference(11 ^ [], 13 ^ []))],extension(5,bind([[_16870], [set_difference(11 ^ [], 13 ^ [])]]))).
% 1.86/2.44 cnf('1.2.3.3.2',plain,[-(in(3 ^ [set_difference(12 ^ [], 13 ^ []), set_difference(11 ^ [], 13 ^ [])], set_difference(11 ^ [], 13 ^ []))), -(subset(set_difference(11 ^ [], 13 ^ []), set_difference(12 ^ [], 13 ^ [])))],extension(10,bind([[_24312, _24368], [set_difference(11 ^ [], 13 ^ []), set_difference(12 ^ [], 13 ^ [])]]))).
% 1.86/2.44 cnf('1.2.3.3.2.1',plain,[subset(set_difference(11 ^ [], 13 ^ []), set_difference(12 ^ [], 13 ^ []))],extension(2)).
% 1.86/2.44 %-----------------------------------------------------
% 1.86/2.45
% 1.86/2.45 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------