%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU149+1 : TPTP v8.1.0. Released v3.3.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 12:00:28 EDT 2022
% Result : Theorem 0.31s 1.39s
% Output : Proof 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : SEU149+1 : TPTP v8.1.0. Released v3.3.0.
% 0.11/0.12 % 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.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Mon Jun 20 02:06:45 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.31/1.39 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/1.40 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/1.41
% 0.38/1.41 %-----------------------------------------------------
% 0.38/1.41 fof(t8_zfmisc_1, conjecture, ! [_15571, _15574, _15577] : (singleton(_15571) = unordered_pair(_15574, _15577) => _15571 = _15574), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t8_zfmisc_1)).
% 0.38/1.41 fof(d1_tarski, axiom, ! [_15797, _15800] : (_15800 = singleton(_15797) <=> ! [_15818] : (in(_15818, _15800) <=> _15818 = _15797)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_tarski)).
% 0.38/1.41 fof(d2_tarski, axiom, ! [_16005, _16008, _16011] : (_16011 = unordered_pair(_16005, _16008) <=> ! [_16032] : (in(_16032, _16011) <=> _16032 = _16005 | _16032 = _16008)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_tarski)).
% 0.38/1.41
% 0.38/1.41 cnf(1, plain, [-(singleton(3 ^ []) = unordered_pair(4 ^ [], 5 ^ []))], clausify(t8_zfmisc_1)).
% 0.38/1.41 cnf(2, plain, [3 ^ [] = 4 ^ []], clausify(t8_zfmisc_1)).
% 0.38/1.41 cnf(3, plain, [_6398 = _6447, -(singleton(_6398) = singleton(_6447))], theory(equality)).
% 0.38/1.41 cnf(4, plain, [-(_4861 = _4861)], theory(equality)).
% 0.38/1.41 cnf(5, plain, [_5014 = _5059, -(_5059 = _5014)], theory(equality)).
% 0.38/1.41 cnf(6, plain, [_8090 = singleton(_8032), in(_8222, _8090), -(_8222 = _8032)], clausify(d1_tarski)).
% 0.38/1.41 cnf(7, plain, [_8652 = unordered_pair(_8513, _8583), -(in(_8816, _8652)), _8816 = _8513], clausify(d2_tarski)).
% 0.38/1.41
% 0.38/1.41 cnf('1',plain,[3 ^ [] = 4 ^ []],start(2)).
% 0.38/1.41 cnf('1.1',plain,[-(3 ^ [] = 4 ^ []), 4 ^ [] = 3 ^ []],extension(5,bind([[_5014, _5059], [4 ^ [], 3 ^ []]]))).
% 0.38/1.41 cnf('1.1.1',plain,[-(4 ^ [] = 3 ^ []), singleton(3 ^ []) = singleton(3 ^ []), in(4 ^ [], singleton(3 ^ []))],extension(6,bind([[_8032, _8222, _8090], [3 ^ [], 4 ^ [], singleton(3 ^ [])]]))).
% 0.38/1.41 cnf('1.1.1.1',plain,[-(singleton(3 ^ []) = singleton(3 ^ [])), 3 ^ [] = 3 ^ []],extension(3,bind([[_6398, _6447], [3 ^ [], 3 ^ []]]))).
% 0.38/1.41 cnf('1.1.1.1.1',plain,[-(3 ^ [] = 3 ^ [])],extension(4,bind([[_4861], [3 ^ []]]))).
% 0.38/1.41 cnf('1.1.1.2',plain,[-(in(4 ^ [], singleton(3 ^ []))), singleton(3 ^ []) = unordered_pair(4 ^ [], 5 ^ []), 4 ^ [] = 4 ^ []],extension(7,bind([[_8652, _8583, _8816, _8513], [singleton(3 ^ []), 5 ^ [], 4 ^ [], 4 ^ []]]))).
% 0.38/1.41 cnf('1.1.1.2.1',plain,[-(singleton(3 ^ []) = unordered_pair(4 ^ [], 5 ^ []))],extension(1)).
% 0.38/1.41 cnf('1.1.1.2.2',plain,[-(4 ^ [] = 4 ^ [])],extension(4,bind([[_4861], [4 ^ []]]))).
% 0.38/1.41 %-----------------------------------------------------
% 0.38/1.41
% 0.38/1.41 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------