%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET887+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n017.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:49 EDT 2022
% Result : Theorem 8.22s 8.64s
% Output : Proof 8.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET887+1 : TPTP v8.1.0. Released v3.2.0.
% 0.13/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n017.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 : Sun Jul 10 16:09:18 EDT 2022
% 0.13/0.34 % CPUTime :
% 8.22/8.64 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.22/8.65 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.22/8.66
% 8.22/8.66 %-----------------------------------------------------
% 8.22/8.66 fof(t28_zfmisc_1, conjecture, ! [_26600, _26603, _26606, _26609] : ~ (subset(unordered_pair(_26600, _26603), unordered_pair(_26606, _26609)) & (! _26600) = _26606 & (! _26600) = _26609), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t28_zfmisc_1)).
% 8.22/8.66 fof(d1_xboole_0, axiom, ! [_26895] : (_26895 = empty_set <=> ! [_26909] : ~ in(_26909, _26895)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_xboole_0)).
% 8.22/8.66 fof(d2_tarski, axiom, ! [_27064, _27067, _27070] : (_27070 = unordered_pair(_27064, _27067) <=> ! [_27091] : (in(_27091, _27070) <=> _27091 = _27064 | _27091 = _27067)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d2_tarski)).
% 8.22/8.66 fof(t8_zfmisc_1, axiom, ! [_27320, _27323, _27326] : (singleton(_27320) = unordered_pair(_27323, _27326) => _27320 = _27323), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t8_zfmisc_1)).
% 8.22/8.66 fof(t10_zfmisc_1, axiom, ! [_27494, _27497, _27500, _27503] : ~ (unordered_pair(_27494, _27497) = unordered_pair(_27500, _27503) & (! _27494) = _27500 & (! _27494) = _27503), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t10_zfmisc_1)).
% 8.22/8.66 fof(l46_zfmisc_1, axiom, ! [_27735, _27738, _27741] : (subset(_27735, unordered_pair(_27738, _27741)) <=> ~ ((! _27735) = empty_set & (! _27735) = singleton(_27738) & (! _27735) = singleton(_27741) & (! _27735) = unordered_pair(_27738, _27741))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', l46_zfmisc_1)).
% 8.22/8.66
% 8.22/8.66 cnf(1, plain, [-(subset(unordered_pair(5 ^ [], 6 ^ []), unordered_pair(7 ^ [], 8 ^ [])))], clausify(t28_zfmisc_1)).
% 8.22/8.66 cnf(2, plain, [5 ^ [] = 7 ^ []], clausify(t28_zfmisc_1)).
% 8.22/8.66 cnf(3, plain, [5 ^ [] = 8 ^ []], clausify(t28_zfmisc_1)).
% 8.22/8.66 cnf(4, plain, [-(_7177 = _7177)], theory(equality)).
% 8.22/8.66 cnf(5, plain, [_7330 = _7375, -(_7375 = _7330)], theory(equality)).
% 8.22/8.66 cnf(6, plain, [_11331 = empty_set, in(_11437, _11331)], clausify(d1_xboole_0)).
% 8.22/8.66 cnf(7, plain, [_11794 = unordered_pair(_11655, _11725), -(in(_11958, _11794)), _11958 = _11655], clausify(d2_tarski)).
% 8.22/8.66 cnf(8, plain, [singleton(_14604) = unordered_pair(_14659, _14713), -(_14604 = _14659)], clausify(t8_zfmisc_1)).
% 8.22/8.66 cnf(9, plain, [unordered_pair(_13897, _13970) = unordered_pair(_14042, _14113), -(_13897 = _14042), -(_13897 = _14113)], clausify(t10_zfmisc_1)).
% 8.22/8.66 cnf(10, plain, [subset(_12452, unordered_pair(_12540, _12627)), -(_12452 = empty_set), -(_12452 = singleton(_12540)), -(_12452 = singleton(_12627)), -(_12452 = unordered_pair(_12540, _12627))], clausify(l46_zfmisc_1)).
% 8.22/8.66
% 8.22/8.66 cnf('1',plain,[empty_set = empty_set, in(5 ^ [], empty_set)],start(6,bind([[_11437, _11331], [5 ^ [], empty_set]]))).
% 8.22/8.66 cnf('1.1',plain,[-(empty_set = empty_set)],extension(4,bind([[_7177], [empty_set]]))).
% 8.22/8.66 cnf('1.2',plain,[-(in(5 ^ [], empty_set)), empty_set = unordered_pair(5 ^ [], 6 ^ []), 5 ^ [] = 5 ^ []],extension(7,bind([[_11794, _11725, _11958, _11655], [empty_set, 6 ^ [], 5 ^ [], 5 ^ []]]))).
% 8.22/8.66 cnf('1.2.1',plain,[-(empty_set = unordered_pair(5 ^ [], 6 ^ [])), unordered_pair(5 ^ [], 6 ^ []) = empty_set],extension(5,bind([[_7330, _7375], [unordered_pair(5 ^ [], 6 ^ []), empty_set]]))).
% 8.22/8.66 cnf('1.2.1.1',plain,[-(unordered_pair(5 ^ [], 6 ^ []) = empty_set), subset(unordered_pair(5 ^ [], 6 ^ []), unordered_pair(7 ^ [], 8 ^ [])), -(unordered_pair(5 ^ [], 6 ^ []) = singleton(7 ^ [])), -(unordered_pair(5 ^ [], 6 ^ []) = singleton(8 ^ [])), -(unordered_pair(5 ^ [], 6 ^ []) = unordered_pair(7 ^ [], 8 ^ []))],extension(10,bind([[_12452, _12540, _12627], [unordered_pair(5 ^ [], 6 ^ []), 7 ^ [], 8 ^ []]]))).
% 8.22/8.66 cnf('1.2.1.1.1',plain,[-(subset(unordered_pair(5 ^ [], 6 ^ []), unordered_pair(7 ^ [], 8 ^ [])))],extension(1)).
% 8.22/8.66 cnf('1.2.1.1.2',plain,[unordered_pair(5 ^ [], 6 ^ []) = singleton(7 ^ []), -(singleton(7 ^ []) = unordered_pair(5 ^ [], 6 ^ []))],extension(5,bind([[_7375, _7330], [singleton(7 ^ []), unordered_pair(5 ^ [], 6 ^ [])]]))).
% 8.22/8.66 cnf('1.2.1.1.2.1',plain,[singleton(7 ^ []) = unordered_pair(5 ^ [], 6 ^ []), -(7 ^ [] = 5 ^ [])],extension(8,bind([[_14713, _14604, _14659], [6 ^ [], 7 ^ [], 5 ^ []]]))).
% 8.22/8.66 cnf('1.2.1.1.2.1.1',plain,[7 ^ [] = 5 ^ [], -(5 ^ [] = 7 ^ [])],extension(5,bind([[_7375, _7330], [5 ^ [], 7 ^ []]]))).
% 8.22/8.66 cnf('1.2.1.1.2.1.1.1',plain,[5 ^ [] = 7 ^ []],extension(2)).
% 8.22/8.66 cnf('1.2.1.1.3',plain,[unordered_pair(5 ^ [], 6 ^ []) = singleton(8 ^ []), -(singleton(8 ^ []) = unordered_pair(5 ^ [], 6 ^ []))],extension(5,bind([[_7375, _7330], [singleton(8 ^ []), unordered_pair(5 ^ [], 6 ^ [])]]))).
% 8.22/8.66 cnf('1.2.1.1.3.1',plain,[singleton(8 ^ []) = unordered_pair(5 ^ [], 6 ^ []), -(8 ^ [] = 5 ^ [])],extension(8,bind([[_14713, _14604, _14659], [6 ^ [], 8 ^ [], 5 ^ []]]))).
% 8.22/8.66 cnf('1.2.1.1.3.1.1',plain,[8 ^ [] = 5 ^ [], -(5 ^ [] = 8 ^ [])],extension(5,bind([[_7375, _7330], [5 ^ [], 8 ^ []]]))).
% 8.22/8.66 cnf('1.2.1.1.3.1.1.1',plain,[5 ^ [] = 8 ^ []],extension(3)).
% 8.22/8.66 cnf('1.2.1.1.4',plain,[unordered_pair(5 ^ [], 6 ^ []) = unordered_pair(7 ^ [], 8 ^ []), -(5 ^ [] = 7 ^ []), -(5 ^ [] = 8 ^ [])],extension(9,bind([[_13970, _14042, _13897, _14113], [6 ^ [], 7 ^ [], 5 ^ [], 8 ^ []]]))).
% 8.22/8.66 cnf('1.2.1.1.4.1',plain,[5 ^ [] = 7 ^ []],extension(2)).
% 8.22/8.66 cnf('1.2.1.1.4.2',plain,[5 ^ [] = 8 ^ []],extension(3)).
% 8.22/8.66 cnf('1.2.2',plain,[-(5 ^ [] = 5 ^ [])],extension(4,bind([[_7177], [5 ^ []]]))).
% 8.22/8.66 %-----------------------------------------------------
% 8.22/8.66
% 8.22/8.66 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------