%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU146+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n028.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:26 EDT 2022
% Result : Theorem 35.05s 34.54s
% Output : Proof 35.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SEU146+1 : TPTP v8.1.0. Released v3.3.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.32 % Computer : n028.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 600
% 0.12/0.32 % DateTime : Sat Jun 18 22:53:59 EDT 2022
% 0.12/0.33 % CPUTime :
% 35.05/34.54 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.05/34.55 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.05/34.56
% 35.05/34.56 %-----------------------------------------------------
% 35.05/34.56 fof(l4_zfmisc_1, conjecture, ! [_28964, _28967] : (subset(_28964, singleton(_28967)) <=> _28964 = empty_set | _28964 = singleton(_28967)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', l4_zfmisc_1)).
% 35.05/34.56 fof(d10_xboole_0, axiom, ! [_29192, _29195] : (_29192 = _29195 <=> subset(_29192, _29195) & subset(_29195, _29192)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d10_xboole_0)).
% 35.05/34.56 fof(l2_zfmisc_1, axiom, ! [_29475, _29478] : (subset(singleton(_29475), _29478) <=> in(_29475, _29478)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', l2_zfmisc_1)).
% 35.05/34.56 fof(l3_zfmisc_1, axiom, ! [_29630, _29633, _29636] : (subset(_29630, _29633) => in(_29636, _29630) | subset(_29630, set_difference(_29633, singleton(_29636)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', l3_zfmisc_1)).
% 35.05/34.56 fof(reflexivity_r1_tarski, axiom, ! [_29842, _29845] : subset(_29842, _29842), file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity_r1_tarski)).
% 35.05/34.56 fof(t2_xboole_1, axiom, ! [_29960] : subset(empty_set, _29960), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t2_xboole_1)).
% 35.05/34.56 fof(t37_xboole_1, axiom, ! [_30068, _30071] : (set_difference(_30068, _30071) = empty_set <=> subset(_30068, _30071)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t37_xboole_1)).
% 35.05/34.56
% 35.05/34.56 cnf(1, plain, [-(7 ^ []), -(4 ^ [] = empty_set), -(4 ^ [] = singleton(5 ^ []))], clausify(l4_zfmisc_1)).
% 35.05/34.56 cnf(2, plain, [-(7 ^ []), subset(4 ^ [], singleton(5 ^ []))], clausify(l4_zfmisc_1)).
% 35.05/34.56 cnf(3, plain, [-(6 ^ []), 4 ^ [] = singleton(5 ^ [])], clausify(l4_zfmisc_1)).
% 35.05/34.56 cnf(4, plain, [-(6 ^ []), 4 ^ [] = empty_set], clausify(l4_zfmisc_1)).
% 35.05/34.56 cnf(5, plain, [-(6 ^ []), -(subset(4 ^ [], singleton(5 ^ [])))], clausify(l4_zfmisc_1)).
% 35.05/34.56 cnf(6, plain, [-(1 ^ [_10222, _10171]), -(subset(_10222, _10171))], clausify(d10_xboole_0)).
% 35.05/34.56 cnf(7, plain, [6 ^ [], 7 ^ []], clausify(l4_zfmisc_1)).
% 35.05/34.56 cnf(8, plain, [_9461 = _9510, -(singleton(_9461) = singleton(_9510))], theory(equality)).
% 35.05/34.56 cnf(9, plain, [-(set_difference(_8847, _8980) = set_difference(_8914, _9045)), _8847 = _8914, _8980 = _9045], theory(equality)).
% 35.05/34.56 cnf(10, plain, [-(_6327 = _6327)], theory(equality)).
% 35.05/34.56 cnf(11, plain, [_6480 = _6525, -(_6525 = _6480)], theory(equality)).
% 35.05/34.56 cnf(12, plain, [-(_6759 = _6870), _6759 = _6815, _6815 = _6870], theory(equality)).
% 35.05/34.56 cnf(13, plain, [-(subset(_8245, _8376)), subset(_8178, _8311), _8178 = _8245, _8311 = _8376], theory(equality)).
% 35.05/34.56 cnf(14, plain, [_10171 = _10222, 1 ^ [_10222, _10171]], clausify(d10_xboole_0)).
% 35.05/34.56 cnf(15, plain, [-(_10171 = _10222), subset(_10171, _10222), subset(_10222, _10171)], clausify(d10_xboole_0)).
% 35.05/34.56 cnf(16, plain, [-(subset(singleton(_11078), _11125)), in(_11078, _11125)], clausify(l2_zfmisc_1)).
% 35.05/34.56 cnf(17, plain, [subset(_11408, _11469), -(in(_11529, _11408)), -(subset(_11408, set_difference(_11469, singleton(_11529))))], clausify(l3_zfmisc_1)).
% 35.05/34.56 cnf(18, plain, [-(subset(_12267, _12267))], clausify(reflexivity_r1_tarski)).
% 35.05/34.56 cnf(19, plain, [-(subset(empty_set, _12491))], clausify(t2_xboole_1)).
% 35.05/34.56 cnf(20, plain, [set_difference(_12665, _12713) = empty_set, -(subset(_12665, _12713))], clausify(t37_xboole_1)).
% 35.05/34.56 cnf(21, plain, [-(set_difference(_12665, _12713) = empty_set), subset(_12665, _12713)], clausify(t37_xboole_1)).
% 35.05/34.56
% 35.05/34.56 cnf('1',plain,[6 ^ [], 7 ^ []],start(7)).
% 35.05/34.56 cnf('1.1',plain,[-(6 ^ []), -(subset(4 ^ [], singleton(5 ^ [])))],extension(5)).
% 35.05/34.56 cnf('1.1.1',plain,[subset(4 ^ [], singleton(5 ^ [])), -(set_difference(4 ^ [], singleton(5 ^ [])) = empty_set)],extension(21,bind([[_12665, _12713], [4 ^ [], singleton(5 ^ [])]]))).
% 35.05/34.56 cnf('1.1.1.1',plain,[set_difference(4 ^ [], singleton(5 ^ [])) = empty_set, -(4 ^ [] = empty_set), 4 ^ [] = set_difference(4 ^ [], singleton(5 ^ []))],extension(12,bind([[_6870, _6759, _6815], [empty_set, 4 ^ [], set_difference(4 ^ [], singleton(5 ^ []))]]))).
% 35.05/34.56 cnf('1.1.1.1.1',plain,[4 ^ [] = empty_set, -(6 ^ [])],extension(4)).
% 35.05/34.56 cnf('1.1.1.1.1.1',plain,[6 ^ []],reduction('1')).
% 35.05/34.56 cnf('1.1.1.1.2',plain,[-(4 ^ [] = set_difference(4 ^ [], singleton(5 ^ []))), subset(4 ^ [], set_difference(4 ^ [], singleton(5 ^ []))), subset(set_difference(4 ^ [], singleton(5 ^ [])), 4 ^ [])],extension(15,bind([[_10222, _10171], [set_difference(4 ^ [], singleton(5 ^ [])), 4 ^ []]]))).
% 35.05/34.56 cnf('1.1.1.1.2.1',plain,[-(subset(4 ^ [], set_difference(4 ^ [], singleton(5 ^ [])))), subset(4 ^ [], 4 ^ []), -(in(5 ^ [], 4 ^ []))],extension(17,bind([[_11469, _11529, _11408], [4 ^ [], 5 ^ [], 4 ^ []]]))).
% 35.05/34.56 cnf('1.1.1.1.2.1.1',plain,[-(subset(4 ^ [], 4 ^ [])), -(1 ^ [4 ^ [], 4 ^ []])],extension(6,bind([[_10222, _10171], [4 ^ [], 4 ^ []]]))).
% 35.05/34.56 cnf('1.1.1.1.2.1.1.1',plain,[1 ^ [4 ^ [], 4 ^ []], 4 ^ [] = 4 ^ []],extension(14,bind([[_10171, _10222], [4 ^ [], 4 ^ []]]))).
% 35.05/34.56 cnf('1.1.1.1.2.1.1.1.1',plain,[-(4 ^ [] = 4 ^ [])],extension(10,bind([[_6327], [4 ^ []]]))).
% 35.05/34.56 cnf('1.1.1.1.2.1.2',plain,[in(5 ^ [], 4 ^ []), -(subset(singleton(5 ^ []), 4 ^ []))],extension(16,bind([[_11078, _11125], [5 ^ [], 4 ^ []]]))).
% 35.05/34.56 cnf('1.1.1.1.2.1.2.1',plain,[subset(singleton(5 ^ []), 4 ^ []), -(singleton(5 ^ []) = 4 ^ []), subset(4 ^ [], singleton(5 ^ []))],extension(15,bind([[_10222, _10171], [4 ^ [], singleton(5 ^ [])]]))).
% 35.05/34.56 cnf('1.1.1.1.2.1.2.1.1',plain,[singleton(5 ^ []) = 4 ^ [], -(4 ^ [] = singleton(5 ^ []))],extension(11,bind([[_6525, _6480], [4 ^ [], singleton(5 ^ [])]]))).
% 35.05/34.56 cnf('1.1.1.1.2.1.2.1.1.1',plain,[4 ^ [] = singleton(5 ^ []), -(6 ^ [])],extension(3)).
% 35.05/34.56 cnf('1.1.1.1.2.1.2.1.1.1.1',plain,[6 ^ []],reduction('1')).
% 35.05/34.56 cnf('1.1.1.1.2.1.2.1.2',plain,[-(subset(4 ^ [], singleton(5 ^ [])))],reduction('1.1')).
% 35.05/34.56 cnf('1.1.1.1.2.2',plain,[-(subset(set_difference(4 ^ [], singleton(5 ^ [])), 4 ^ [])), set_difference(set_difference(4 ^ [], singleton(5 ^ [])), 4 ^ []) = empty_set],extension(20,bind([[_12665, _12713], [set_difference(4 ^ [], singleton(5 ^ [])), 4 ^ []]]))).
% 35.05/34.56 cnf('1.1.1.1.2.2.1',plain,[-(set_difference(set_difference(4 ^ [], singleton(5 ^ [])), 4 ^ []) = empty_set), set_difference(set_difference(4 ^ [], singleton(5 ^ [])), 4 ^ []) = set_difference(empty_set, 4 ^ []), set_difference(empty_set, 4 ^ []) = empty_set],extension(12,bind([[_6759, _6815, _6870], [set_difference(set_difference(4 ^ [], singleton(5 ^ [])), 4 ^ []), set_difference(empty_set, 4 ^ []), empty_set]]))).
% 35.05/34.56 cnf('1.1.1.1.2.2.1.1',plain,[-(set_difference(set_difference(4 ^ [], singleton(5 ^ [])), 4 ^ []) = set_difference(empty_set, 4 ^ [])), set_difference(4 ^ [], singleton(5 ^ [])) = empty_set, 4 ^ [] = 4 ^ []],extension(9,bind([[_8847, _8914, _8980, _9045], [set_difference(4 ^ [], singleton(5 ^ [])), empty_set, 4 ^ [], 4 ^ []]]))).
% 35.05/34.56 cnf('1.1.1.1.2.2.1.1.1',plain,[-(set_difference(4 ^ [], singleton(5 ^ [])) = empty_set)],reduction('1.1.1')).
% 35.05/34.56 cnf('1.1.1.1.2.2.1.1.2',plain,[-(4 ^ [] = 4 ^ [])],extension(10,bind([[_6327], [4 ^ []]]))).
% 35.05/34.56 cnf('1.1.1.1.2.2.1.2',plain,[-(set_difference(empty_set, 4 ^ []) = empty_set), subset(empty_set, 4 ^ [])],extension(21,bind([[_12665, _12713], [empty_set, 4 ^ []]]))).
% 35.05/34.56 cnf('1.1.1.1.2.2.1.2.1',plain,[-(subset(empty_set, 4 ^ []))],extension(19,bind([[_12491], [4 ^ []]]))).
% 35.05/34.56 cnf('1.2',plain,[-(7 ^ []), subset(4 ^ [], singleton(5 ^ []))],extension(2)).
% 35.05/34.56 cnf('1.2.1',plain,[-(subset(4 ^ [], singleton(5 ^ []))), set_difference(4 ^ [], singleton(5 ^ [])) = empty_set],extension(20,bind([[_12665, _12713], [4 ^ [], singleton(5 ^ [])]]))).
% 35.05/34.56 cnf('1.2.1.1',plain,[-(set_difference(4 ^ [], singleton(5 ^ [])) = empty_set), set_difference(4 ^ [], singleton(5 ^ [])) = set_difference(empty_set, singleton(5 ^ [])), set_difference(empty_set, singleton(5 ^ [])) = empty_set],extension(12,bind([[_6759, _6815, _6870], [set_difference(4 ^ [], singleton(5 ^ [])), set_difference(empty_set, singleton(5 ^ [])), empty_set]]))).
% 35.05/34.56 cnf('1.2.1.1.1',plain,[-(set_difference(4 ^ [], singleton(5 ^ [])) = set_difference(empty_set, singleton(5 ^ []))), 4 ^ [] = empty_set, singleton(5 ^ []) = singleton(5 ^ [])],extension(9,bind([[_8847, _8914, _8980, _9045], [4 ^ [], empty_set, singleton(5 ^ []), singleton(5 ^ [])]]))).
% 35.05/34.56 cnf('1.2.1.1.1.1',plain,[-(4 ^ [] = empty_set), -(7 ^ []), -(4 ^ [] = singleton(5 ^ []))],extension(1)).
% 35.05/34.56 cnf('1.2.1.1.1.1.1',plain,[7 ^ []],reduction('1')).
% 35.05/34.56 cnf('1.2.1.1.1.1.2',plain,[4 ^ [] = singleton(5 ^ []), -(singleton(5 ^ []) = 4 ^ [])],extension(11,bind([[_6525, _6480], [singleton(5 ^ []), 4 ^ []]]))).
% 35.05/34.56 cnf('1.2.1.1.1.1.2.1',plain,[singleton(5 ^ []) = 4 ^ [], -(subset(4 ^ [], singleton(5 ^ []))), subset(singleton(5 ^ []), singleton(5 ^ [])), singleton(5 ^ []) = singleton(5 ^ [])],extension(13,bind([[_8245, _8178, _8311, _8376], [4 ^ [], singleton(5 ^ []), singleton(5 ^ []), singleton(5 ^ [])]]))).
% 35.05/34.56 cnf('1.2.1.1.1.1.2.1.1',plain,[subset(4 ^ [], singleton(5 ^ []))],reduction('1.2')).
% 35.05/34.56 cnf('1.2.1.1.1.1.2.1.2',plain,[-(subset(singleton(5 ^ []), singleton(5 ^ [])))],extension(18,bind([[_12267], [singleton(5 ^ [])]]))).
% 35.05/34.56 cnf('1.2.1.1.1.1.2.1.3',plain,[-(singleton(5 ^ []) = singleton(5 ^ []))],extension(10,bind([[_6327], [singleton(5 ^ [])]]))).
% 35.05/34.56 cnf('1.2.1.1.1.2',plain,[-(singleton(5 ^ []) = singleton(5 ^ [])), 5 ^ [] = 5 ^ []],extension(8,bind([[_9461, _9510], [5 ^ [], 5 ^ []]]))).
% 35.05/34.56 cnf('1.2.1.1.1.2.1',plain,[-(5 ^ [] = 5 ^ [])],extension(10,bind([[_6327], [5 ^ []]]))).
% 35.05/34.56 cnf('1.2.1.1.2',plain,[-(set_difference(empty_set, singleton(5 ^ [])) = empty_set), subset(empty_set, singleton(5 ^ []))],extension(21,bind([[_12665, _12713], [empty_set, singleton(5 ^ [])]]))).
% 35.05/34.56 cnf('1.2.1.1.2.1',plain,[-(subset(empty_set, singleton(5 ^ [])))],extension(19,bind([[_12491], [singleton(5 ^ [])]]))).
% 35.05/34.56 %-----------------------------------------------------
% 35.15/34.56
% 35.15/34.56 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------