%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU162+2 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n006.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:37 EDT 2022
% Result : Theorem 8.21s 8.69s
% Output : Proof 8.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU162+2 : TPTP v8.1.0. Released v3.3.0.
% 0.11/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n006.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Mon Jun 20 01:06:25 EDT 2022
% 0.13/0.34 % CPUTime :
% 8.21/8.69 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.21/8.70 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.21/8.71
% 8.21/8.71 %-----------------------------------------------------
% 8.21/8.71 fof(t65_zfmisc_1, conjecture, ! [_107364, _107367] : (set_difference(_107364, singleton(_107367)) = _107364 <=> ~ in(_107367, _107364)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t65_zfmisc_1)).
% 8.21/8.71 fof(d10_xboole_0, axiom, ! [_107628, _107631] : (_107628 = _107631 <=> subset(_107628, _107631) & subset(_107631, _107628)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d10_xboole_0)).
% 8.21/8.71 fof(d1_tarski, axiom, ! [_107799, _107802] : (_107802 = singleton(_107799) <=> ! [_107820] : (in(_107820, _107802) <=> _107820 = _107799)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_tarski)).
% 8.21/8.71 fof(d4_xboole_0, axiom, ! [_108048, _108051, _108054] : (_108054 = set_difference(_108048, _108051) <=> ! [_108075] : (in(_108075, _108054) <=> in(_108075, _108048) & ~ in(_108075, _108051))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d4_xboole_0)).
% 8.21/8.71 fof(l3_zfmisc_1, lemma, ! [_108335, _108338, _108341] : (subset(_108335, _108338) => in(_108341, _108335) | subset(_108335, set_difference(_108338, singleton(_108341)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l3_zfmisc_1)).
% 8.21/8.71 fof(reflexivity_r1_tarski, axiom, ! [_108554, _108557] : subset(_108554, _108554), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity_r1_tarski)).
% 8.21/8.71 fof(t36_xboole_1, lemma, ! [_108689, _108692] : subset(set_difference(_108689, _108692), _108689), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t36_xboole_1)).
% 8.21/8.71
% 8.21/8.71 cnf(1, plain, [-(25 ^ []), set_difference(22 ^ [], singleton(23 ^ [])) = 22 ^ []], clausify(t65_zfmisc_1)).
% 8.21/8.71 cnf(2, plain, [-(25 ^ []), in(23 ^ [], 22 ^ [])], clausify(t65_zfmisc_1)).
% 8.21/8.71 cnf(3, plain, [-(24 ^ []), -(in(23 ^ [], 22 ^ []))], clausify(t65_zfmisc_1)).
% 8.21/8.71 cnf(4, plain, [-(24 ^ []), -(set_difference(22 ^ [], singleton(23 ^ [])) = 22 ^ [])], clausify(t65_zfmisc_1)).
% 8.21/8.71 cnf(5, plain, [24 ^ [], 25 ^ []], clausify(t65_zfmisc_1)).
% 8.21/8.71 cnf(6, plain, [-(_33507 = _33507)], theory(equality)).
% 8.21/8.71 cnf(7, plain, [_33660 = _33705, -(_33705 = _33660)], theory(equality)).
% 8.21/8.71 cnf(8, plain, [-(_43772 = _43823), subset(_43772, _43823), subset(_43823, _43772)], clausify(d10_xboole_0)).
% 8.21/8.71 cnf(9, plain, [_44226 = singleton(_44168), -(in(_44358, _44226)), _44358 = _44168], clausify(d1_tarski)).
% 8.21/8.71 cnf(10, plain, [_49788 = set_difference(_49645, _49717), in(_49954, _49788), in(_49954, _49717)], clausify(d4_xboole_0)).
% 8.21/8.71 cnf(11, plain, [subset(_56640, _56701), -(in(_56761, _56640)), -(subset(_56640, set_difference(_56701, singleton(_56761))))], clausify(l3_zfmisc_1)).
% 8.21/8.71 cnf(12, plain, [-(subset(_58910, _58910))], clausify(reflexivity_r1_tarski)).
% 8.21/8.71 cnf(13, plain, [-(subset(set_difference(_64921, _64963), _64921))], clausify(t36_xboole_1)).
% 8.21/8.71
% 8.21/8.71 cnf('1',plain,[24 ^ [], 25 ^ []],start(5)).
% 8.21/8.71 cnf('1.1',plain,[-(24 ^ []), -(in(23 ^ [], 22 ^ []))],extension(3)).
% 8.21/8.71 cnf('1.1.1',plain,[in(23 ^ [], 22 ^ []), 22 ^ [] = set_difference(22 ^ [], singleton(23 ^ [])), in(23 ^ [], singleton(23 ^ []))],extension(10,bind([[_49788, _49645, _49954, _49717], [22 ^ [], 22 ^ [], 23 ^ [], singleton(23 ^ [])]]))).
% 8.21/8.71 cnf('1.1.1.1',plain,[-(22 ^ [] = set_difference(22 ^ [], singleton(23 ^ []))), set_difference(22 ^ [], singleton(23 ^ [])) = 22 ^ []],extension(7,bind([[_33660, _33705], [set_difference(22 ^ [], singleton(23 ^ [])), 22 ^ []]]))).
% 8.21/8.71 cnf('1.1.1.1.1',plain,[-(set_difference(22 ^ [], singleton(23 ^ [])) = 22 ^ []), -(24 ^ [])],extension(4)).
% 8.21/8.71 cnf('1.1.1.1.1.1',plain,[24 ^ []],reduction('1')).
% 8.21/8.71 cnf('1.1.1.2',plain,[-(in(23 ^ [], singleton(23 ^ []))), singleton(23 ^ []) = singleton(23 ^ []), 23 ^ [] = 23 ^ []],extension(9,bind([[_44226, _44358, _44168], [singleton(23 ^ []), 23 ^ [], 23 ^ []]]))).
% 8.21/8.71 cnf('1.1.1.2.1',plain,[-(singleton(23 ^ []) = singleton(23 ^ []))],extension(6,bind([[_33507], [singleton(23 ^ [])]]))).
% 8.21/8.71 cnf('1.1.1.2.2',plain,[-(23 ^ [] = 23 ^ [])],extension(6,bind([[_33507], [23 ^ []]]))).
% 8.21/8.71 cnf('1.2',plain,[-(25 ^ []), set_difference(22 ^ [], singleton(23 ^ [])) = 22 ^ []],extension(1)).
% 8.21/8.71 cnf('1.2.1',plain,[-(set_difference(22 ^ [], singleton(23 ^ [])) = 22 ^ []), subset(set_difference(22 ^ [], singleton(23 ^ [])), 22 ^ []), subset(22 ^ [], set_difference(22 ^ [], singleton(23 ^ [])))],extension(8,bind([[_43823, _43772], [22 ^ [], set_difference(22 ^ [], singleton(23 ^ []))]]))).
% 8.21/8.71 cnf('1.2.1.1',plain,[-(subset(set_difference(22 ^ [], singleton(23 ^ [])), 22 ^ []))],extension(13,bind([[_64963, _64921], [singleton(23 ^ []), 22 ^ []]]))).
% 8.21/8.71 cnf('1.2.1.2',plain,[-(subset(22 ^ [], set_difference(22 ^ [], singleton(23 ^ [])))), subset(22 ^ [], 22 ^ []), -(in(23 ^ [], 22 ^ []))],extension(11,bind([[_56701, _56761, _56640], [22 ^ [], 23 ^ [], 22 ^ []]]))).
% 8.21/8.71 cnf('1.2.1.2.1',plain,[-(subset(22 ^ [], 22 ^ []))],extension(12,bind([[_58910], [22 ^ []]]))).
% 8.21/8.71 cnf('1.2.1.2.2',plain,[in(23 ^ [], 22 ^ []), -(25 ^ [])],extension(2)).
% 8.21/8.71 cnf('1.2.1.2.2.1',plain,[25 ^ []],reduction('1')).
% 8.21/8.71 %-----------------------------------------------------
% 8.21/8.71
% 8.32/8.71 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------