%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET889+1 : TPTP v8.1.0. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n029.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 02:56:50 EDT 2022
% Result : Theorem 0.44s 1.41s
% Output : Proof 0.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SET889+1 : TPTP v8.1.0. Bugfixed v4.0.0.
% 0.11/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n029.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.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Sun Jul 10 04:22:46 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.44/1.41 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.44/1.42 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.44/1.42
% 0.44/1.42 %-----------------------------------------------------
% 0.44/1.42 fof(t30_zfmisc_1, conjecture, ! [_28339] : powerset(singleton(_28339)) = unordered_pair(empty_set, singleton(_28339)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t30_zfmisc_1)).
% 0.44/1.42 fof(d1_zfmisc_1, axiom, ! [_28518, _28521] : (_28521 = powerset(_28518) <=> ! [_28539] : (in(_28539, _28521) <=> subset(_28539, _28518))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_zfmisc_1)).
% 0.44/1.42 fof(l4_zfmisc_1, axiom, ! [_28747, _28750] : (subset(_28747, singleton(_28750)) <=> _28747 = empty_set | _28747 = singleton(_28750)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l4_zfmisc_1)).
% 0.44/1.42 fof(d2_tarski, axiom, ! [_28958, _28961, _28964] : (_28964 = unordered_pair(_28958, _28961) <=> ! [_28985] : (in(_28985, _28964) <=> _28985 = _28958 | _28985 = _28961)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_tarski)).
% 0.44/1.42
% 0.44/1.42 cnf(1, plain, [powerset(singleton(6 ^ [])) = unordered_pair(empty_set, singleton(6 ^ []))], clausify(t30_zfmisc_1)).
% 0.44/1.42 cnf(2, plain, [_8732 = _8781, -(powerset(_8732) = powerset(_8781))], theory(equality)).
% 0.44/1.42 cnf(3, plain, [-(_6212 = _6212)], theory(equality)).
% 0.44/1.42 cnf(4, plain, [_10768 = powerset(_10710), in(_10900, _10768), -(subset(_10900, _10710))], clausify(d1_zfmisc_1)).
% 0.44/1.42 cnf(5, plain, [_10768 = powerset(_10710), -(in(_10900, _10768)), subset(_10900, _10710)], clausify(d1_zfmisc_1)).
% 0.44/1.42 cnf(6, plain, [-(subset(_11988, singleton(_12043))), _11988 = empty_set], clausify(l4_zfmisc_1)).
% 0.44/1.42 cnf(7, plain, [-(subset(_11988, singleton(_12043))), _11988 = singleton(_12043)], clausify(l4_zfmisc_1)).
% 0.44/1.42 cnf(8, plain, [subset(_11988, singleton(_12043)), -(_11988 = empty_set), -(_11988 = singleton(_12043))], clausify(l4_zfmisc_1)).
% 0.44/1.42 cnf(9, plain, [-(_11330 = unordered_pair(_11191, _11261)), in(2 ^ [_11330, _11261, _11191], _11330), 2 ^ [_11330, _11261, _11191] = _11191], clausify(d2_tarski)).
% 0.44/1.42 cnf(10, plain, [-(_11330 = unordered_pair(_11191, _11261)), in(2 ^ [_11330, _11261, _11191], _11330), 2 ^ [_11330, _11261, _11191] = _11261], clausify(d2_tarski)).
% 0.44/1.42 cnf(11, plain, [-(_11330 = unordered_pair(_11191, _11261)), -(in(2 ^ [_11330, _11261, _11191], _11330)), -(2 ^ [_11330, _11261, _11191] = _11191), -(2 ^ [_11330, _11261, _11191] = _11261)], clausify(d2_tarski)).
% 0.44/1.42
% 0.44/1.42 cnf('1',plain,[powerset(singleton(6 ^ [])) = unordered_pair(empty_set, singleton(6 ^ []))],start(1)).
% 0.44/1.42 cnf('1.1',plain,[-(powerset(singleton(6 ^ [])) = unordered_pair(empty_set, singleton(6 ^ []))), -(in(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], powerset(singleton(6 ^ [])))), -(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set] = empty_set), -(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set] = singleton(6 ^ []))],extension(11,bind([[_11330, _11191, _11261], [powerset(singleton(6 ^ [])), empty_set, singleton(6 ^ [])]]))).
% 0.44/1.42 cnf('1.1.1',plain,[in(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], powerset(singleton(6 ^ []))), powerset(singleton(6 ^ [])) = powerset(singleton(6 ^ [])), -(subset(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], singleton(6 ^ [])))],extension(4,bind([[_10768, _10900, _10710], [powerset(singleton(6 ^ [])), 2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], singleton(6 ^ [])]]))).
% 0.44/1.42 cnf('1.1.1.1',plain,[-(powerset(singleton(6 ^ [])) = powerset(singleton(6 ^ []))), singleton(6 ^ []) = singleton(6 ^ [])],extension(2,bind([[_8732, _8781], [singleton(6 ^ []), singleton(6 ^ [])]]))).
% 0.44/1.42 cnf('1.1.1.1.1',plain,[-(singleton(6 ^ []) = singleton(6 ^ []))],extension(3,bind([[_6212], [singleton(6 ^ [])]]))).
% 0.44/1.42 cnf('1.1.1.2',plain,[subset(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], singleton(6 ^ [])), -(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set] = empty_set), -(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set] = singleton(6 ^ []))],extension(8,bind([[_11988, _12043], [2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], 6 ^ []]]))).
% 0.44/1.42 cnf('1.1.1.2.1',plain,[2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set] = empty_set, -(powerset(singleton(6 ^ [])) = unordered_pair(empty_set, singleton(6 ^ []))), in(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], powerset(singleton(6 ^ [])))],extension(9,bind([[_11261, _11191, _11330], [singleton(6 ^ []), empty_set, powerset(singleton(6 ^ []))]]))).
% 0.44/1.42 cnf('1.1.1.2.1.1',plain,[powerset(singleton(6 ^ [])) = unordered_pair(empty_set, singleton(6 ^ []))],extension(1)).
% 0.44/1.42 cnf('1.1.1.2.1.2',plain,[-(in(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], powerset(singleton(6 ^ []))))],reduction('1.1')).
% 0.44/1.42 cnf('1.1.1.2.2',plain,[2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set] = singleton(6 ^ []), -(powerset(singleton(6 ^ [])) = unordered_pair(empty_set, singleton(6 ^ []))), in(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], powerset(singleton(6 ^ [])))],extension(10,bind([[_11261, _11191, _11330], [singleton(6 ^ []), empty_set, powerset(singleton(6 ^ []))]]))).
% 0.44/1.42 cnf('1.1.1.2.2.1',plain,[powerset(singleton(6 ^ [])) = unordered_pair(empty_set, singleton(6 ^ []))],extension(1)).
% 0.44/1.42 cnf('1.1.1.2.2.2',plain,[-(in(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], powerset(singleton(6 ^ []))))],reduction('1.1')).
% 0.44/1.42 cnf('1.1.2',plain,[2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set] = empty_set, -(subset(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], singleton(6 ^ [])))],extension(6,bind([[_11988, _12043], [2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], 6 ^ []]]))).
% 0.44/1.42 cnf('1.1.2.1',plain,[subset(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], singleton(6 ^ [])), powerset(singleton(6 ^ [])) = powerset(singleton(6 ^ [])), -(in(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], powerset(singleton(6 ^ []))))],extension(5,bind([[_10710, _10900, _10768], [singleton(6 ^ []), 2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], powerset(singleton(6 ^ []))]]))).
% 0.44/1.42 cnf('1.1.2.1.1',plain,[-(powerset(singleton(6 ^ [])) = powerset(singleton(6 ^ [])))],extension(3,bind([[_6212], [powerset(singleton(6 ^ []))]]))).
% 0.44/1.42 cnf('1.1.2.1.2',plain,[in(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], powerset(singleton(6 ^ []))), -(powerset(singleton(6 ^ [])) = unordered_pair(empty_set, singleton(6 ^ []))), 2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set] = empty_set],extension(9,bind([[_11330, _11261, _11191], [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set]]))).
% 0.44/1.42 cnf('1.1.2.1.2.1',plain,[powerset(singleton(6 ^ [])) = unordered_pair(empty_set, singleton(6 ^ []))],extension(1)).
% 0.44/1.42 cnf('1.1.2.1.2.2',plain,[-(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set] = empty_set)],reduction('1.1')).
% 0.44/1.42 cnf('1.1.3',plain,[2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set] = singleton(6 ^ []), -(powerset(singleton(6 ^ [])) = unordered_pair(empty_set, singleton(6 ^ []))), in(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], powerset(singleton(6 ^ [])))],extension(10,bind([[_11261, _11191, _11330], [singleton(6 ^ []), empty_set, powerset(singleton(6 ^ []))]]))).
% 0.44/1.42 cnf('1.1.3.1',plain,[powerset(singleton(6 ^ [])) = unordered_pair(empty_set, singleton(6 ^ []))],extension(1)).
% 0.44/1.42 cnf('1.1.3.2',plain,[-(in(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], powerset(singleton(6 ^ [])))), powerset(singleton(6 ^ [])) = powerset(singleton(6 ^ [])), subset(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], singleton(6 ^ []))],extension(5,bind([[_10768, _10900, _10710], [powerset(singleton(6 ^ [])), 2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], singleton(6 ^ [])]]))).
% 0.44/1.42 cnf('1.1.3.2.1',plain,[-(powerset(singleton(6 ^ [])) = powerset(singleton(6 ^ [])))],extension(3,bind([[_6212], [powerset(singleton(6 ^ []))]]))).
% 0.44/1.42 cnf('1.1.3.2.2',plain,[-(subset(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], singleton(6 ^ []))), 2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set] = singleton(6 ^ [])],extension(7,bind([[_11988, _12043], [2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set], 6 ^ []]]))).
% 0.44/1.42 cnf('1.1.3.2.2.1',plain,[-(2 ^ [powerset(singleton(6 ^ [])), singleton(6 ^ []), empty_set] = singleton(6 ^ []))],reduction('1.1')).
% 0.44/1.42 %-----------------------------------------------------
% 0.44/1.43
% 0.44/1.43 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------