%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET902+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n013.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:55 EDT 2022
% Result : Theorem 244.48s 236.68s
% Output : Proof 244.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : SET902+1 : TPTP v8.1.0. Released v3.2.0.
% 0.10/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n013.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.12/0.33 % DateTime : Sun Jul 10 02:15:14 EDT 2022
% 0.12/0.33 % CPUTime :
% 244.48/236.68 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 244.48/236.69 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 244.48/236.69
% 244.48/236.69 %-----------------------------------------------------
% 244.48/236.69 fof(t43_zfmisc_1, conjecture, ! [_36682, _36685, _36688] : ~ (singleton(_36682) = set_union2(_36685, _36688) & ~ (_36685 = singleton(_36682) & _36688 = singleton(_36682)) & ~ (_36685 = empty_set & _36688 = singleton(_36682)) & ~ (_36685 = singleton(_36682) & _36688 = empty_set)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t43_zfmisc_1)).
% 244.48/236.69 fof(commutativity_k2_xboole_0, axiom, ! [_37040, _37043] : set_union2(_37040, _37043) = set_union2(_37043, _37040), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', commutativity_k2_xboole_0)).
% 244.48/236.69 fof(t7_xboole_1, axiom, ! [_37188, _37191] : subset(_37188, set_union2(_37188, _37191)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t7_xboole_1)).
% 244.48/236.69 fof(l4_zfmisc_1, axiom, ! [_37322, _37325] : (subset(_37322, singleton(_37325)) <=> _37322 = empty_set | _37322 = singleton(_37325)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l4_zfmisc_1)).
% 244.48/236.69 fof(idempotence_k2_xboole_0, axiom, ! [_37531, _37534] : set_union2(_37531, _37531) = _37531, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', idempotence_k2_xboole_0)).
% 244.48/236.69 fof(l1_zfmisc_1, axiom, ! [_37722] : (! singleton(_37722)) = empty_set, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l1_zfmisc_1)).
% 244.48/236.69
% 244.48/236.69 cnf(1, plain, [4 ^ [] = singleton(3 ^ []), 5 ^ [] = singleton(3 ^ [])], clausify(t43_zfmisc_1)).
% 244.48/236.69 cnf(2, plain, [-(set_union2(_9286, _9331) = set_union2(_9331, _9286))], clausify(commutativity_k2_xboole_0)).
% 244.48/236.69 cnf(3, plain, [-(subset(_11853, set_union2(_11853, _11895)))], clausify(t7_xboole_1)).
% 244.48/236.69 cnf(4, plain, [subset(_10879, singleton(_10934)), -(_10879 = empty_set), -(_10879 = singleton(_10934))], clausify(l4_zfmisc_1)).
% 244.48/236.69 cnf(5, plain, [-(_6411 = _6411)], theory(equality)).
% 244.48/236.69 cnf(6, plain, [4 ^ [] = empty_set, 5 ^ [] = singleton(3 ^ [])], clausify(t43_zfmisc_1)).
% 244.48/236.69 cnf(7, plain, [-(set_union2(_10402, _10402) = _10402)], clausify(idempotence_k2_xboole_0)).
% 244.48/236.69 cnf(8, plain, [_6564 = _6609, -(_6609 = _6564)], theory(equality)).
% 244.48/236.69 cnf(9, plain, [_8906 = _8955, -(singleton(_8906) = singleton(_8955))], theory(equality)).
% 244.48/236.69 cnf(10, plain, [-(_6843 = _6954), _6843 = _6899, _6899 = _6954], theory(equality)).
% 244.48/236.69 cnf(11, plain, [-(singleton(3 ^ []) = set_union2(4 ^ [], 5 ^ []))], clausify(t43_zfmisc_1)).
% 244.48/236.69 cnf(12, plain, [4 ^ [] = singleton(3 ^ []), 5 ^ [] = empty_set], clausify(t43_zfmisc_1)).
% 244.48/236.69 cnf(13, plain, [singleton(_10669) = empty_set], clausify(l1_zfmisc_1)).
% 244.48/236.69 cnf(14, plain, [-(subset(_10879, singleton(_10934))), _10879 = empty_set], clausify(l4_zfmisc_1)).
% 244.48/236.69 cnf(15, plain, [-(subset(_7705, _7836)), subset(_7638, _7771), _7638 = _7705, _7771 = _7836], theory(equality)).
% 244.48/236.69 cnf(16, plain, [-(set_union2(_8292, _8425) = set_union2(_8359, _8490)), _8292 = _8359, _8425 = _8490], theory(equality)).
% 244.48/236.69
% 244.48/236.69 cnf('1',plain,[4 ^ [] = singleton(3 ^ []), 5 ^ [] = singleton(3 ^ [])],start(1)).
% 244.48/236.69 cnf('1.1',plain,[-(4 ^ [] = singleton(3 ^ [])), subset(4 ^ [], singleton(3 ^ [])), -(4 ^ [] = empty_set)],extension(4,bind([[_10934, _10879], [3 ^ [], 4 ^ []]]))).
% 244.48/236.69 cnf('1.1.1',plain,[-(subset(4 ^ [], singleton(3 ^ []))), 4 ^ [] = empty_set],extension(14,bind([[_10934, _10879], [3 ^ [], 4 ^ []]]))).
% 244.48/236.69 cnf('1.1.1.1',plain,[-(4 ^ [] = empty_set), subset(4 ^ [], singleton(3 ^ [])), -(4 ^ [] = singleton(3 ^ []))],extension(4,bind([[_10879, _10934], [4 ^ [], 3 ^ []]]))).
% 244.48/236.69 cnf('1.1.1.1.1',plain,[-(subset(4 ^ [], singleton(3 ^ []))), subset(4 ^ [], set_union2(4 ^ [], 5 ^ [])), 4 ^ [] = 4 ^ [], set_union2(4 ^ [], 5 ^ []) = singleton(3 ^ [])],extension(15,bind([[_7638, _7705, _7771, _7836], [4 ^ [], 4 ^ [], set_union2(4 ^ [], 5 ^ []), singleton(3 ^ [])]]))).
% 244.48/236.69 cnf('1.1.1.1.1.1',plain,[-(subset(4 ^ [], set_union2(4 ^ [], 5 ^ [])))],extension(3,bind([[_11853, _11895], [4 ^ [], 5 ^ []]]))).
% 244.48/236.69 cnf('1.1.1.1.1.2',plain,[-(4 ^ [] = 4 ^ [])],extension(5,bind([[_6411], [4 ^ []]]))).
% 244.48/236.69 cnf('1.1.1.1.1.3',plain,[-(set_union2(4 ^ [], 5 ^ []) = singleton(3 ^ [])), singleton(3 ^ []) = set_union2(4 ^ [], 5 ^ [])],extension(8,bind([[_6564, _6609], [singleton(3 ^ []), set_union2(4 ^ [], 5 ^ [])]]))).
% 244.48/236.69 cnf('1.1.1.1.1.3.1',plain,[-(singleton(3 ^ []) = set_union2(4 ^ [], 5 ^ []))],extension(11)).
% 244.48/236.69 cnf('1.1.1.1.2',plain,[4 ^ [] = singleton(3 ^ [])],reduction('1')).
% 244.48/236.69 cnf('1.1.2',plain,[4 ^ [] = empty_set, -(empty_set = 4 ^ [])],extension(8,bind([[_6609, _6564], [empty_set, 4 ^ []]]))).
% 244.48/236.69 cnf('1.1.2.1',plain,[empty_set = 4 ^ [], -(set_union2(empty_set, empty_set) = set_union2(5 ^ [], 4 ^ [])), empty_set = 5 ^ []],extension(16,bind([[_8425, _8490, _8292, _8359], [empty_set, 4 ^ [], empty_set, 5 ^ []]]))).
% 244.48/236.69 cnf('1.1.2.1.1',plain,[set_union2(empty_set, empty_set) = set_union2(5 ^ [], 4 ^ []), -(set_union2(empty_set, empty_set) = singleton(3 ^ [])), set_union2(5 ^ [], 4 ^ []) = singleton(3 ^ [])],extension(10,bind([[_6843, _6899, _6954], [set_union2(empty_set, empty_set), set_union2(5 ^ [], 4 ^ []), singleton(3 ^ [])]]))).
% 244.48/236.69 cnf('1.1.2.1.1.1',plain,[set_union2(empty_set, empty_set) = singleton(3 ^ []), -(4 ^ [] = singleton(3 ^ [])), 4 ^ [] = set_union2(empty_set, empty_set)],extension(10,bind([[_6954, _6843, _6899], [singleton(3 ^ []), 4 ^ [], set_union2(empty_set, empty_set)]]))).
% 244.48/236.69 cnf('1.1.2.1.1.1.1',plain,[4 ^ [] = singleton(3 ^ [])],reduction('1')).
% 244.48/236.69 cnf('1.1.2.1.1.1.2',plain,[-(4 ^ [] = set_union2(empty_set, empty_set)), 4 ^ [] = empty_set, empty_set = set_union2(empty_set, empty_set)],extension(10,bind([[_6843, _6899, _6954], [4 ^ [], empty_set, set_union2(empty_set, empty_set)]]))).
% 244.48/236.69 cnf('1.1.2.1.1.1.2.1',plain,[-(4 ^ [] = empty_set)],reduction('1.1')).
% 244.48/236.69 cnf('1.1.2.1.1.1.2.2',plain,[-(empty_set = set_union2(empty_set, empty_set)), set_union2(empty_set, empty_set) = empty_set],extension(8,bind([[_6564, _6609], [set_union2(empty_set, empty_set), empty_set]]))).
% 244.48/236.69 cnf('1.1.2.1.1.1.2.2.1',plain,[-(set_union2(empty_set, empty_set) = empty_set)],extension(7,bind([[_10402], [empty_set]]))).
% 244.48/236.69 cnf('1.1.2.1.1.2',plain,[-(set_union2(5 ^ [], 4 ^ []) = singleton(3 ^ [])), set_union2(5 ^ [], 4 ^ []) = set_union2(4 ^ [], 5 ^ []), set_union2(4 ^ [], 5 ^ []) = singleton(3 ^ [])],extension(10,bind([[_6843, _6899, _6954], [set_union2(5 ^ [], 4 ^ []), set_union2(4 ^ [], 5 ^ []), singleton(3 ^ [])]]))).
% 244.48/236.69 cnf('1.1.2.1.1.2.1',plain,[-(set_union2(5 ^ [], 4 ^ []) = set_union2(4 ^ [], 5 ^ []))],extension(2,bind([[_9331, _9286], [4 ^ [], 5 ^ []]]))).
% 244.48/236.69 cnf('1.1.2.1.1.2.2',plain,[-(set_union2(4 ^ [], 5 ^ []) = singleton(3 ^ [])), singleton(3 ^ []) = set_union2(4 ^ [], 5 ^ [])],extension(8,bind([[_6564, _6609], [singleton(3 ^ []), set_union2(4 ^ [], 5 ^ [])]]))).
% 244.48/236.69 cnf('1.1.2.1.1.2.2.1',plain,[-(singleton(3 ^ []) = set_union2(4 ^ [], 5 ^ []))],extension(11)).
% 244.48/236.69 cnf('1.1.2.1.2',plain,[-(empty_set = 5 ^ []), 5 ^ [] = empty_set],extension(8,bind([[_6564, _6609], [5 ^ [], empty_set]]))).
% 244.48/236.69 cnf('1.1.2.1.2.1',plain,[-(5 ^ [] = empty_set), subset(5 ^ [], singleton(3 ^ [])), -(5 ^ [] = singleton(3 ^ []))],extension(4,bind([[_10879, _10934], [5 ^ [], 3 ^ []]]))).
% 244.48/236.69 cnf('1.1.2.1.2.1.1',plain,[-(subset(5 ^ [], singleton(3 ^ []))), subset(5 ^ [], set_union2(5 ^ [], 4 ^ [])), 5 ^ [] = 5 ^ [], set_union2(5 ^ [], 4 ^ []) = singleton(3 ^ [])],extension(15,bind([[_7638, _7705, _7771, _7836], [5 ^ [], 5 ^ [], set_union2(5 ^ [], 4 ^ []), singleton(3 ^ [])]]))).
% 244.48/236.69 cnf('1.1.2.1.2.1.1.1',plain,[-(subset(5 ^ [], set_union2(5 ^ [], 4 ^ [])))],extension(3,bind([[_11853, _11895], [5 ^ [], 4 ^ []]]))).
% 244.48/236.69 cnf('1.1.2.1.2.1.1.2',plain,[-(5 ^ [] = 5 ^ [])],extension(5,bind([[_6411], [5 ^ []]]))).
% 244.48/236.69 cnf('1.1.2.1.2.1.1.3',plain,[-(set_union2(5 ^ [], 4 ^ []) = singleton(3 ^ [])), set_union2(5 ^ [], 4 ^ []) = set_union2(4 ^ [], 5 ^ []), set_union2(4 ^ [], 5 ^ []) = singleton(3 ^ [])],extension(10,bind([[_6843, _6899, _6954], [set_union2(5 ^ [], 4 ^ []), set_union2(4 ^ [], 5 ^ []), singleton(3 ^ [])]]))).
% 244.48/236.69 cnf('1.1.2.1.2.1.1.3.1',plain,[-(set_union2(5 ^ [], 4 ^ []) = set_union2(4 ^ [], 5 ^ []))],extension(2,bind([[_9331, _9286], [4 ^ [], 5 ^ []]]))).
% 244.48/236.69 cnf('1.1.2.1.2.1.1.3.2',plain,[-(set_union2(4 ^ [], 5 ^ []) = singleton(3 ^ [])), singleton(3 ^ []) = set_union2(4 ^ [], 5 ^ [])],extension(8,bind([[_6564, _6609], [singleton(3 ^ []), set_union2(4 ^ [], 5 ^ [])]]))).
% 244.48/236.69 cnf('1.1.2.1.2.1.1.3.2.1',plain,[-(singleton(3 ^ []) = set_union2(4 ^ [], 5 ^ []))],extension(11)).
% 244.48/236.69 cnf('1.1.2.1.2.1.2',plain,[5 ^ [] = singleton(3 ^ []), 4 ^ [] = empty_set],extension(6)).
% 244.48/236.69 cnf('1.1.2.1.2.1.2.1',plain,[-(4 ^ [] = empty_set)],reduction('1.1')).
% 244.48/236.69 cnf('1.2',plain,[-(5 ^ [] = singleton(3 ^ [])), subset(5 ^ [], singleton(3 ^ [])), -(5 ^ [] = empty_set)],extension(4,bind([[_10934, _10879], [3 ^ [], 5 ^ []]]))).
% 244.48/236.69 cnf('1.2.1',plain,[-(subset(5 ^ [], singleton(3 ^ []))), 5 ^ [] = empty_set],extension(14,bind([[_10934, _10879], [3 ^ [], 5 ^ []]]))).
% 244.48/236.69 cnf('1.2.1.1',plain,[-(5 ^ [] = empty_set), subset(5 ^ [], singleton(3 ^ [])), -(5 ^ [] = singleton(3 ^ []))],extension(4,bind([[_10879, _10934], [5 ^ [], 3 ^ []]]))).
% 244.48/236.69 cnf('1.2.1.1.1',plain,[-(subset(5 ^ [], singleton(3 ^ []))), subset(5 ^ [], set_union2(5 ^ [], 4 ^ [])), 5 ^ [] = 5 ^ [], set_union2(5 ^ [], 4 ^ []) = singleton(3 ^ [])],extension(15,bind([[_7638, _7705, _7771, _7836], [5 ^ [], 5 ^ [], set_union2(5 ^ [], 4 ^ []), singleton(3 ^ [])]]))).
% 244.48/236.69 cnf('1.2.1.1.1.1',plain,[-(subset(5 ^ [], set_union2(5 ^ [], 4 ^ [])))],extension(3,bind([[_11853, _11895], [5 ^ [], 4 ^ []]]))).
% 244.48/236.69 cnf('1.2.1.1.1.2',plain,[-(5 ^ [] = 5 ^ [])],extension(5,bind([[_6411], [5 ^ []]]))).
% 244.48/236.69 cnf('1.2.1.1.1.3',plain,[-(set_union2(5 ^ [], 4 ^ []) = singleton(3 ^ [])), set_union2(5 ^ [], 4 ^ []) = set_union2(4 ^ [], 5 ^ []), set_union2(4 ^ [], 5 ^ []) = singleton(3 ^ [])],extension(10,bind([[_6843, _6899, _6954], [set_union2(5 ^ [], 4 ^ []), set_union2(4 ^ [], 5 ^ []), singleton(3 ^ [])]]))).
% 244.48/236.69 cnf('1.2.1.1.1.3.1',plain,[-(set_union2(5 ^ [], 4 ^ []) = set_union2(4 ^ [], 5 ^ []))],extension(2,bind([[_9331, _9286], [4 ^ [], 5 ^ []]]))).
% 244.48/236.69 cnf('1.2.1.1.1.3.2',plain,[-(set_union2(4 ^ [], 5 ^ []) = singleton(3 ^ [])), singleton(3 ^ []) = set_union2(4 ^ [], 5 ^ [])],extension(8,bind([[_6564, _6609], [singleton(3 ^ []), set_union2(4 ^ [], 5 ^ [])]]))).
% 244.48/236.69 cnf('1.2.1.1.1.3.2.1',plain,[-(singleton(3 ^ []) = set_union2(4 ^ [], 5 ^ []))],extension(11)).
% 244.48/236.69 cnf('1.2.1.1.2',plain,[5 ^ [] = singleton(3 ^ [])],reduction('1')).
% 244.48/236.69 cnf('1.2.2',plain,[5 ^ [] = empty_set, -(empty_set = 5 ^ [])],extension(8,bind([[_6609, _6564], [empty_set, 5 ^ []]]))).
% 244.48/236.69 cnf('1.2.2.1',plain,[empty_set = 5 ^ [], -(singleton(empty_set) = singleton(5 ^ []))],extension(9,bind([[_8906, _8955], [empty_set, 5 ^ []]]))).
% 244.48/236.69 cnf('1.2.2.1.1',plain,[singleton(empty_set) = singleton(5 ^ []), -(empty_set = singleton(5 ^ [])), empty_set = singleton(empty_set)],extension(10,bind([[_6954, _6843, _6899], [singleton(5 ^ []), empty_set, singleton(empty_set)]]))).
% 244.48/236.69 cnf('1.2.2.1.1.1',plain,[empty_set = singleton(5 ^ []), -(singleton(5 ^ []) = empty_set)],extension(8,bind([[_6609, _6564], [singleton(5 ^ []), empty_set]]))).
% 244.48/236.69 cnf('1.2.2.1.1.1.1',plain,[singleton(5 ^ []) = empty_set],extension(13,bind([[_10669], [5 ^ []]]))).
% 244.48/236.69 cnf('1.2.2.1.1.2',plain,[-(empty_set = singleton(empty_set)), subset(empty_set, singleton(empty_set)), -(empty_set = empty_set)],extension(4,bind([[_10934, _10879], [empty_set, empty_set]]))).
% 244.48/236.69 cnf('1.2.2.1.1.2.1',plain,[-(subset(empty_set, singleton(empty_set))), empty_set = empty_set],extension(14,bind([[_10934, _10879], [empty_set, empty_set]]))).
% 244.48/236.69 cnf('1.2.2.1.1.2.1.1',plain,[-(empty_set = empty_set)],extension(5,bind([[_6411], [empty_set]]))).
% 244.48/236.69 cnf('1.2.2.1.1.2.2',plain,[empty_set = empty_set, -(subset(empty_set, singleton(3 ^ [])))],extension(14,bind([[_10879, _10934], [empty_set, 3 ^ []]]))).
% 244.48/236.69 cnf('1.2.2.1.1.2.2.1',plain,[subset(empty_set, singleton(3 ^ [])), -(subset(5 ^ [], singleton(3 ^ []))), empty_set = 5 ^ [], singleton(3 ^ []) = singleton(3 ^ [])],extension(15,bind([[_7638, _7705, _7771, _7836], [empty_set, 5 ^ [], singleton(3 ^ []), singleton(3 ^ [])]]))).
% 244.48/236.69 cnf('1.2.2.1.1.2.2.1.1',plain,[subset(5 ^ [], singleton(3 ^ [])), -(5 ^ [] = empty_set), -(5 ^ [] = singleton(3 ^ []))],extension(4,bind([[_10879, _10934], [5 ^ [], 3 ^ []]]))).
% 244.48/236.69 cnf('1.2.2.1.1.2.2.1.1.1',plain,[5 ^ [] = empty_set, 4 ^ [] = singleton(3 ^ [])],extension(12)).
% 244.48/236.69 cnf('1.2.2.1.1.2.2.1.1.1.1',plain,[-(4 ^ [] = singleton(3 ^ []))],lemmata('1')).
% 244.48/236.69 cnf('1.2.2.1.1.2.2.1.1.2',plain,[5 ^ [] = singleton(3 ^ [])],reduction('1')).
% 244.48/236.69 cnf('1.2.2.1.1.2.2.1.2',plain,[-(empty_set = 5 ^ [])],reduction('1.2.2')).
% 244.48/236.69 cnf('1.2.2.1.1.2.2.1.3',plain,[-(singleton(3 ^ []) = singleton(3 ^ []))],extension(5,bind([[_6411], [singleton(3 ^ [])]]))).
% 244.48/236.69 %-----------------------------------------------------
% 244.48/236.70
% 244.48/236.70 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------