%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU136+2 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n026.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:21 EDT 2022
% Result : Theorem 7.75s 8.65s
% Output : Proof 7.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : SEU136+2 : TPTP v8.1.0. Released v3.3.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n026.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 Jun 19 12:00:25 EDT 2022
% 0.12/0.33 % CPUTime :
% 7.75/8.65 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.75/8.65 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.75/8.66
% 7.75/8.66 %-----------------------------------------------------
% 7.75/8.66 fof(t40_xboole_1, conjecture, ! [_68230, _68233] : set_difference(set_union2(_68230, _68233), _68233) = set_difference(_68230, _68233), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t40_xboole_1)).
% 7.75/8.66 fof(d2_xboole_0, axiom, ! [_68454, _68457, _68460] : (_68460 = set_union2(_68454, _68457) <=> ! [_68481] : (in(_68481, _68460) <=> in(_68481, _68454) | in(_68481, _68457))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_xboole_0)).
% 7.75/8.66 fof(d4_xboole_0, axiom, ! [_68734, _68737, _68740] : (_68740 = set_difference(_68734, _68737) <=> ! [_68761] : (in(_68761, _68740) <=> in(_68761, _68734) & ~ in(_68761, _68737))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d4_xboole_0)).
% 7.75/8.66
% 7.75/8.66 cnf(1, plain, [set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ []) = set_difference(11 ^ [], 12 ^ [])], clausify(t40_xboole_1)).
% 7.75/8.66 cnf(2, plain, [-(set_difference(_21243, _21376) = set_difference(_21310, _21441)), _21243 = _21310, _21376 = _21441], theory(equality)).
% 7.75/8.66 cnf(3, plain, [-(set_union2(_22481, _22614) = set_union2(_22548, _22679)), _22481 = _22548, _22614 = _22679], theory(equality)).
% 7.75/8.66 cnf(4, plain, [-(_18084 = _18084)], theory(equality)).
% 7.75/8.66 cnf(5, plain, [_18237 = _18282, -(_18282 = _18237)], theory(equality)).
% 7.75/8.66 cnf(6, plain, [_24980 = set_union2(_24841, _24911), -(in(_25144, _24980)), in(_25144, _24841)], clausify(d2_xboole_0)).
% 7.75/8.66 cnf(7, plain, [_24980 = set_union2(_24841, _24911), in(_25144, _24980), -(in(_25144, _24841)), -(in(_25144, _24911))], clausify(d2_xboole_0)).
% 7.75/8.66 cnf(8, plain, [_26815 = set_difference(_26672, _26744), in(_26981, _26815), -(in(_26981, _26672))], clausify(d4_xboole_0)).
% 7.75/8.66 cnf(9, plain, [_26815 = set_difference(_26672, _26744), in(_26981, _26815), in(_26981, _26744)], clausify(d4_xboole_0)).
% 7.75/8.66 cnf(10, plain, [_26815 = set_difference(_26672, _26744), -(in(_26981, _26815)), in(_26981, _26672), -(in(_26981, _26744))], clausify(d4_xboole_0)).
% 7.75/8.66 cnf(11, plain, [-(_26815 = set_difference(_26672, _26744)), -(in(5 ^ [_26815, _26744, _26672], _26815)), -(in(5 ^ [_26815, _26744, _26672], _26672))], clausify(d4_xboole_0)).
% 7.75/8.66 cnf(12, plain, [-(_26815 = set_difference(_26672, _26744)), -(in(5 ^ [_26815, _26744, _26672], _26815)), in(5 ^ [_26815, _26744, _26672], _26744)], clausify(d4_xboole_0)).
% 7.75/8.66 cnf(13, plain, [-(_26815 = set_difference(_26672, _26744)), in(5 ^ [_26815, _26744, _26672], _26815), in(5 ^ [_26815, _26744, _26672], _26672), -(in(5 ^ [_26815, _26744, _26672], _26744))], clausify(d4_xboole_0)).
% 7.75/8.66
% 7.75/8.66 cnf('1',plain,[set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ []) = set_difference(11 ^ [], 12 ^ [])],start(1)).
% 7.75/8.66 cnf('1.1',plain,[-(set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ []) = set_difference(11 ^ [], 12 ^ [])), set_difference(11 ^ [], 12 ^ []) = set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ [])],extension(5,bind([[_18237, _18282], [set_difference(11 ^ [], 12 ^ []), set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ [])]]))).
% 7.75/8.66 cnf('1.1.1',plain,[-(set_difference(11 ^ [], 12 ^ []) = set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ [])), in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ [])), in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_union2(11 ^ [], 12 ^ [])), -(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 12 ^ []))],extension(13,bind([[_26815, _26672, _26744], [set_difference(11 ^ [], 12 ^ []), set_union2(11 ^ [], 12 ^ []), 12 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.1',plain,[-(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ []))), set_difference(11 ^ [], 12 ^ []) = set_difference(11 ^ [], 12 ^ []), in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 11 ^ []), -(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 12 ^ []))],extension(10,bind([[_26815, _26672, _26981, _26744], [set_difference(11 ^ [], 12 ^ []), 11 ^ [], 5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 12 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.1.1',plain,[-(set_difference(11 ^ [], 12 ^ []) = set_difference(11 ^ [], 12 ^ [])), 11 ^ [] = 11 ^ [], 12 ^ [] = 12 ^ []],extension(2,bind([[_21243, _21310, _21376, _21441], [11 ^ [], 11 ^ [], 12 ^ [], 12 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.1.1.1',plain,[-(11 ^ [] = 11 ^ [])],extension(4,bind([[_18084], [11 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.1.1.2',plain,[-(12 ^ [] = 12 ^ [])],extension(4,bind([[_18084], [12 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.1.2',plain,[-(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 11 ^ [])), set_union2(11 ^ [], 12 ^ []) = set_union2(11 ^ [], 12 ^ []), in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_union2(11 ^ [], 12 ^ [])), -(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 12 ^ []))],extension(7,bind([[_24841, _24980, _25144, _24911], [11 ^ [], set_union2(11 ^ [], 12 ^ []), 5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 12 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.1.2.1',plain,[-(set_union2(11 ^ [], 12 ^ []) = set_union2(11 ^ [], 12 ^ []))],extension(4,bind([[_18084], [set_union2(11 ^ [], 12 ^ [])]]))).
% 7.75/8.66 cnf('1.1.1.1.2.2',plain,[-(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_union2(11 ^ [], 12 ^ []))), -(set_difference(11 ^ [], 12 ^ []) = set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ [])), -(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ [])))],extension(11,bind([[_26744, _26672, _26815], [12 ^ [], set_union2(11 ^ [], 12 ^ []), set_difference(11 ^ [], 12 ^ [])]]))).
% 7.75/8.66 cnf('1.1.1.1.2.2.1',plain,[set_difference(11 ^ [], 12 ^ []) = set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ [])],reduction('1.1')).
% 7.75/8.66 cnf('1.1.1.1.2.2.2',plain,[in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ []))],reduction('1.1.1')).
% 7.75/8.66 cnf('1.1.1.1.2.3',plain,[in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 12 ^ []), -(set_difference(11 ^ [], 12 ^ []) = set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ [])), -(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ [])))],extension(12,bind([[_26744, _26672, _26815], [12 ^ [], set_union2(11 ^ [], 12 ^ []), set_difference(11 ^ [], 12 ^ [])]]))).
% 7.75/8.66 cnf('1.1.1.1.2.3.1',plain,[set_difference(11 ^ [], 12 ^ []) = set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ [])],reduction('1.1')).
% 7.75/8.66 cnf('1.1.1.1.2.3.2',plain,[in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ []))],reduction('1.1.1')).
% 7.75/8.66 cnf('1.1.1.1.3',plain,[in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 12 ^ []), set_difference(11 ^ [], 12 ^ []) = set_difference(11 ^ [], 12 ^ []), in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ []))],extension(9,bind([[_26672, _26744, _26981, _26815], [11 ^ [], 12 ^ [], 5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ [])]]))).
% 7.75/8.66 cnf('1.1.1.1.3.1',plain,[-(set_difference(11 ^ [], 12 ^ []) = set_difference(11 ^ [], 12 ^ []))],extension(4,bind([[_18084], [set_difference(11 ^ [], 12 ^ [])]]))).
% 7.75/8.66 cnf('1.1.1.1.3.2',plain,[-(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ []))), -(set_difference(11 ^ [], 12 ^ []) = set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ [])), in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 12 ^ [])],extension(12,bind([[_26815, _26672, _26744], [set_difference(11 ^ [], 12 ^ []), set_union2(11 ^ [], 12 ^ []), 12 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.1.3.2.1',plain,[set_difference(11 ^ [], 12 ^ []) = set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ [])],reduction('1.1')).
% 7.75/8.66 cnf('1.1.1.1.3.2.2',plain,[-(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 12 ^ []))],reduction('1.1.1.1')).
% 7.75/8.66 cnf('1.1.1.2',plain,[-(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_union2(11 ^ [], 12 ^ []))), set_union2(11 ^ [], 12 ^ []) = set_union2(11 ^ [], 12 ^ []), in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 11 ^ [])],extension(6,bind([[_24980, _24911, _25144, _24841], [set_union2(11 ^ [], 12 ^ []), 12 ^ [], 5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 11 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.2.1',plain,[-(set_union2(11 ^ [], 12 ^ []) = set_union2(11 ^ [], 12 ^ [])), 11 ^ [] = 11 ^ [], 12 ^ [] = 12 ^ []],extension(3,bind([[_22481, _22548, _22614, _22679], [11 ^ [], 11 ^ [], 12 ^ [], 12 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.2.1.1',plain,[-(11 ^ [] = 11 ^ [])],extension(4,bind([[_18084], [11 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.2.1.2',plain,[-(12 ^ [] = 12 ^ [])],extension(4,bind([[_18084], [12 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.2.2',plain,[-(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 11 ^ [])), set_difference(11 ^ [], 12 ^ []) = set_difference(11 ^ [], 12 ^ []), in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ []))],extension(8,bind([[_26672, _26744, _26981, _26815], [11 ^ [], 12 ^ [], 5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ [])]]))).
% 7.75/8.66 cnf('1.1.1.2.2.1',plain,[-(set_difference(11 ^ [], 12 ^ []) = set_difference(11 ^ [], 12 ^ []))],extension(4,bind([[_18084], [set_difference(11 ^ [], 12 ^ [])]]))).
% 7.75/8.66 cnf('1.1.1.2.2.2',plain,[-(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ []))), -(set_difference(11 ^ [], 12 ^ []) = set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ [])), -(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_union2(11 ^ [], 12 ^ [])))],extension(11,bind([[_26815, _26744, _26672], [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])]]))).
% 7.75/8.66 cnf('1.1.1.2.2.2.1',plain,[set_difference(11 ^ [], 12 ^ []) = set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ [])],reduction('1.1')).
% 7.75/8.66 cnf('1.1.1.2.2.2.2',plain,[in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_union2(11 ^ [], 12 ^ []))],reduction('1.1.1')).
% 7.75/8.66 cnf('1.1.1.3',plain,[in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 12 ^ []), set_difference(11 ^ [], 12 ^ []) = set_difference(11 ^ [], 12 ^ []), in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ []))],extension(9,bind([[_26672, _26744, _26981, _26815], [11 ^ [], 12 ^ [], 5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ [])]]))).
% 7.75/8.66 cnf('1.1.1.3.1',plain,[-(set_difference(11 ^ [], 12 ^ []) = set_difference(11 ^ [], 12 ^ [])), 11 ^ [] = 11 ^ [], 12 ^ [] = 12 ^ []],extension(2,bind([[_21243, _21310, _21376, _21441], [11 ^ [], 11 ^ [], 12 ^ [], 12 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.3.1.1',plain,[-(11 ^ [] = 11 ^ [])],extension(4,bind([[_18084], [11 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.3.1.2',plain,[-(12 ^ [] = 12 ^ [])],extension(4,bind([[_18084], [12 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.3.2',plain,[-(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], set_difference(11 ^ [], 12 ^ []))), -(set_difference(11 ^ [], 12 ^ []) = set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ [])), in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 12 ^ [])],extension(12,bind([[_26815, _26672, _26744], [set_difference(11 ^ [], 12 ^ []), set_union2(11 ^ [], 12 ^ []), 12 ^ []]]))).
% 7.75/8.66 cnf('1.1.1.3.2.1',plain,[set_difference(11 ^ [], 12 ^ []) = set_difference(set_union2(11 ^ [], 12 ^ []), 12 ^ [])],reduction('1.1')).
% 7.75/8.66 cnf('1.1.1.3.2.2',plain,[-(in(5 ^ [set_difference(11 ^ [], 12 ^ []), 12 ^ [], set_union2(11 ^ [], 12 ^ [])], 12 ^ []))],reduction('1.1.1')).
% 7.75/8.66 %-----------------------------------------------------
% 7.75/8.66
% 7.75/8.66 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------