%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU131+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n025.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 0.42s 1.35s
% Output : Proof 0.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.09 % Problem : SEU131+1 : TPTP v8.1.0. Released v3.3.0.
% 0.03/0.10 % Command : leancop_casc.sh %s %d
% 0.09/0.29 % Computer : n025.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 600
% 0.09/0.29 % DateTime : Sun Jun 19 07:17:13 EDT 2022
% 0.09/0.29 % CPUTime :
% 0.42/1.35 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.42/1.36 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.50/1.36
% 0.50/1.36 %-----------------------------------------------------
% 0.50/1.36 fof(l32_xboole_1, conjecture, ! [_27141, _27144] : (set_difference(_27141, _27144) = empty_set <=> subset(_27141, _27144)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', l32_xboole_1)).
% 0.50/1.36 fof(d3_tarski, axiom, ! [_27362, _27365] : (subset(_27362, _27365) <=> ! [_27383] : (in(_27383, _27362) => in(_27383, _27365))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d3_tarski)).
% 0.50/1.36 fof(d4_xboole_0, axiom, ! [_27591, _27594, _27597] : (_27597 = set_difference(_27591, _27594) <=> ! [_27618] : (in(_27618, _27597) <=> in(_27618, _27591) & ~ in(_27618, _27594))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d4_xboole_0)).
% 0.50/1.36 fof(fc1_xboole_0, axiom, empty(empty_set), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fc1_xboole_0)).
% 0.50/1.36 fof(t3_boole, axiom, ! [_27942] : set_difference(_27942, empty_set) = _27942, file('/export/starexec/sandbox/benchmark/theBenchmark.p', t3_boole)).
% 0.50/1.36 fof(t7_boole, axiom, ! [_28063, _28066] : ~ (in(_28063, _28066) & empty(_28066)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t7_boole)).
% 0.50/1.36
% 0.50/1.36 cnf(1, plain, [-(9 ^ []), set_difference(6 ^ [], 7 ^ []) = empty_set], clausify(l32_xboole_1)).
% 0.50/1.36 cnf(2, plain, [-(9 ^ []), -(subset(6 ^ [], 7 ^ []))], clausify(l32_xboole_1)).
% 0.50/1.36 cnf(3, plain, [-(8 ^ []), subset(6 ^ [], 7 ^ [])], clausify(l32_xboole_1)).
% 0.50/1.36 cnf(4, plain, [-(8 ^ []), -(set_difference(6 ^ [], 7 ^ []) = empty_set)], clausify(l32_xboole_1)).
% 0.50/1.36 cnf(5, plain, [8 ^ [], 9 ^ []], clausify(l32_xboole_1)).
% 0.50/1.36 cnf(6, plain, [_7070 = _7115, -(_7115 = _7070)], theory(equality)).
% 0.50/1.36 cnf(7, plain, [-(subset(_10417, _10473)), -(in(1 ^ [_10473, _10417], _10417))], clausify(d3_tarski)).
% 0.50/1.36 cnf(8, plain, [-(subset(_10417, _10473)), in(1 ^ [_10473, _10417], _10473)], clausify(d3_tarski)).
% 0.50/1.36 cnf(9, plain, [subset(_10417, _10473), in(_10587, _10417), -(in(_10587, _10473))], clausify(d3_tarski)).
% 0.50/1.36 cnf(10, plain, [_11021 = set_difference(_10878, _10950), in(_11187, _11021), in(_11187, _10950)], clausify(d4_xboole_0)).
% 0.50/1.36 cnf(11, plain, [_11021 = set_difference(_10878, _10950), -(in(_11187, _11021)), in(_11187, _10878), -(in(_11187, _10950))], clausify(d4_xboole_0)).
% 0.50/1.36 cnf(12, plain, [-(_11021 = set_difference(_10878, _10950)), -(in(2 ^ [_11021, _10950, _10878], _11021)), -(in(2 ^ [_11021, _10950, _10878], _10878))], clausify(d4_xboole_0)).
% 0.50/1.36 cnf(13, plain, [-(_11021 = set_difference(_10878, _10950)), -(in(2 ^ [_11021, _10950, _10878], _11021)), in(2 ^ [_11021, _10950, _10878], _10950)], clausify(d4_xboole_0)).
% 0.50/1.36 cnf(14, plain, [-(empty(empty_set))], clausify(fc1_xboole_0)).
% 0.50/1.36 cnf(15, plain, [-(set_difference(_12974, empty_set) = _12974)], clausify(t3_boole)).
% 0.50/1.36 cnf(16, plain, [in(_13634, _13680), empty(_13680)], clausify(t7_boole)).
% 0.50/1.36
% 0.50/1.36 cnf('1',plain,[8 ^ [], 9 ^ []],start(5)).
% 0.50/1.36 cnf('1.1',plain,[-(8 ^ []), subset(6 ^ [], 7 ^ [])],extension(3)).
% 0.50/1.36 cnf('1.1.1',plain,[-(subset(6 ^ [], 7 ^ [])), -(in(1 ^ [7 ^ [], 6 ^ []], 6 ^ []))],extension(7,bind([[_10473, _10417], [7 ^ [], 6 ^ []]]))).
% 0.50/1.36 cnf('1.1.1.1',plain,[in(1 ^ [7 ^ [], 6 ^ []], 6 ^ []), 6 ^ [] = set_difference(6 ^ [], empty_set), in(1 ^ [7 ^ [], 6 ^ []], empty_set)],extension(10,bind([[_11021, _10878, _11187, _10950], [6 ^ [], 6 ^ [], 1 ^ [7 ^ [], 6 ^ []], empty_set]]))).
% 0.50/1.36 cnf('1.1.1.1.1',plain,[-(6 ^ [] = set_difference(6 ^ [], empty_set)), set_difference(6 ^ [], empty_set) = 6 ^ []],extension(6,bind([[_7070, _7115], [set_difference(6 ^ [], empty_set), 6 ^ []]]))).
% 0.50/1.36 cnf('1.1.1.1.1.1',plain,[-(set_difference(6 ^ [], empty_set) = 6 ^ [])],extension(15,bind([[_12974], [6 ^ []]]))).
% 0.50/1.36 cnf('1.1.1.1.2',plain,[-(in(1 ^ [7 ^ [], 6 ^ []], empty_set)), empty_set = set_difference(6 ^ [], 7 ^ []), in(1 ^ [7 ^ [], 6 ^ []], 6 ^ []), -(in(1 ^ [7 ^ [], 6 ^ []], 7 ^ []))],extension(11,bind([[_11021, _10878, _11187, _10950], [empty_set, 6 ^ [], 1 ^ [7 ^ [], 6 ^ []], 7 ^ []]]))).
% 0.50/1.36 cnf('1.1.1.1.2.1',plain,[-(empty_set = set_difference(6 ^ [], 7 ^ [])), set_difference(6 ^ [], 7 ^ []) = empty_set],extension(6,bind([[_7070, _7115], [set_difference(6 ^ [], 7 ^ []), empty_set]]))).
% 0.50/1.36 cnf('1.1.1.1.2.1.1',plain,[-(set_difference(6 ^ [], 7 ^ []) = empty_set), -(8 ^ [])],extension(4)).
% 0.50/1.36 cnf('1.1.1.1.2.1.1.1',plain,[8 ^ []],reduction('1')).
% 0.50/1.36 cnf('1.1.1.1.2.2',plain,[-(in(1 ^ [7 ^ [], 6 ^ []], 6 ^ []))],reduction('1.1.1')).
% 0.50/1.36 cnf('1.1.1.1.2.3',plain,[in(1 ^ [7 ^ [], 6 ^ []], 7 ^ []), -(subset(6 ^ [], 7 ^ []))],extension(8,bind([[_10417, _10473], [6 ^ [], 7 ^ []]]))).
% 0.50/1.36 cnf('1.1.1.1.2.3.1',plain,[subset(6 ^ [], 7 ^ [])],reduction('1.1')).
% 0.50/1.36 cnf('1.2',plain,[-(9 ^ []), set_difference(6 ^ [], 7 ^ []) = empty_set],extension(1)).
% 0.50/1.36 cnf('1.2.1',plain,[-(set_difference(6 ^ [], 7 ^ []) = empty_set), empty_set = set_difference(6 ^ [], 7 ^ [])],extension(6,bind([[_7070, _7115], [empty_set, set_difference(6 ^ [], 7 ^ [])]]))).
% 0.50/1.36 cnf('1.2.1.1',plain,[-(empty_set = set_difference(6 ^ [], 7 ^ [])), -(in(2 ^ [empty_set, 7 ^ [], 6 ^ []], empty_set)), -(in(2 ^ [empty_set, 7 ^ [], 6 ^ []], 6 ^ []))],extension(12,bind([[_11021, _10950, _10878], [empty_set, 7 ^ [], 6 ^ []]]))).
% 0.50/1.36 cnf('1.2.1.1.1',plain,[in(2 ^ [empty_set, 7 ^ [], 6 ^ []], empty_set), empty(empty_set)],extension(16,bind([[_13634, _13680], [2 ^ [empty_set, 7 ^ [], 6 ^ []], empty_set]]))).
% 0.50/1.36 cnf('1.2.1.1.1.1',plain,[-(empty(empty_set))],extension(14)).
% 0.50/1.36 cnf('1.2.1.1.2',plain,[in(2 ^ [empty_set, 7 ^ [], 6 ^ []], 6 ^ []), subset(6 ^ [], 7 ^ []), -(in(2 ^ [empty_set, 7 ^ [], 6 ^ []], 7 ^ []))],extension(9,bind([[_10417, _10587, _10473], [6 ^ [], 2 ^ [empty_set, 7 ^ [], 6 ^ []], 7 ^ []]]))).
% 0.50/1.36 cnf('1.2.1.1.2.1',plain,[-(subset(6 ^ [], 7 ^ [])), -(9 ^ [])],extension(2)).
% 0.50/1.36 cnf('1.2.1.1.2.1.1',plain,[9 ^ []],reduction('1')).
% 0.50/1.36 cnf('1.2.1.1.2.2',plain,[in(2 ^ [empty_set, 7 ^ [], 6 ^ []], 7 ^ []), -(empty_set = set_difference(6 ^ [], 7 ^ [])), -(in(2 ^ [empty_set, 7 ^ [], 6 ^ []], empty_set))],extension(13,bind([[_10950, _10878, _11021], [7 ^ [], 6 ^ [], empty_set]]))).
% 0.50/1.36 cnf('1.2.1.1.2.2.1',plain,[empty_set = set_difference(6 ^ [], 7 ^ [])],reduction('1.2.1')).
% 0.50/1.36 cnf('1.2.1.1.2.2.2',plain,[in(2 ^ [empty_set, 7 ^ [], 6 ^ []], empty_set)],lemmata('1.2.1.1')).
% 0.50/1.36 %-----------------------------------------------------
% 0.50/1.37
% 0.50/1.37 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------