%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET986+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n011.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:57:30 EDT 2022
% Result : Theorem 36.16s 35.63s
% Output : Proof 36.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SET986+1 : TPTP v8.1.0. Released v3.2.0.
% 0.06/0.13 % Command : leancop_casc.sh %s %d
% 0.14/0.34 % Computer : n011.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Sat Jul 9 19:56:41 EDT 2022
% 0.14/0.34 % CPUTime :
% 36.16/35.63 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 36.16/35.64 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 36.16/35.64
% 36.16/35.64 %-----------------------------------------------------
% 36.16/35.64 fof(d4_xboole_0, axiom, ! [_44112, _44115, _44118] : (_44118 = set_difference(_44112, _44115) <=> ! [_44139] : (in(_44139, _44118) <=> in(_44139, _44112) & ~ in(_44139, _44115))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d4_xboole_0)).
% 36.16/35.64 fof(d2_xboole_0, axiom, ! [_44398, _44401, _44404] : (_44404 = set_union2(_44398, _44401) <=> ! [_44425] : (in(_44425, _44404) <=> in(_44425, _44398) | in(_44425, _44401))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_xboole_0)).
% 36.16/35.64 fof(d1_tarski, axiom, ! [_44743, _44746] : (_44746 = singleton(_44743) <=> ! [_44764] : (in(_44764, _44746) <=> _44764 = _44743)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_tarski)).
% 36.16/35.64 fof(t140_zfmisc_1, conjecture, ! [_44950, _44953] : (in(_44950, _44953) => set_union2(set_difference(_44953, singleton(_44950)), singleton(_44950)) = _44953), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t140_zfmisc_1)).
% 36.16/35.64
% 36.16/35.64 cnf(1, plain, [-(13 ^ [_15311, _15145, _15074, _15002]), -(in(_15311, _15002))], clausify(d4_xboole_0)).
% 36.16/35.64 cnf(2, plain, [-(14 ^ [_15145, _15074, _15002]), -(in(_15311, _15145)), in(_15311, _15002), -(in(_15311, _15074))], clausify(d4_xboole_0)).
% 36.16/35.64 cnf(3, plain, [-(14 ^ [_15145, _15074, _15002]), in(_15311, _15145), 13 ^ [_15311, _15145, _15074, _15002]], clausify(d4_xboole_0)).
% 36.16/35.64 cnf(4, plain, [-(10 ^ [_13995, _13926, _13856]), -(in(8 ^ [_13995, _13926, _13856], _13856)), -(in(8 ^ [_13995, _13926, _13856], _13926))], clausify(d2_xboole_0)).
% 36.16/35.64 cnf(5, plain, [-(10 ^ [_13995, _13926, _13856]), in(8 ^ [_13995, _13926, _13856], _13995)], clausify(d2_xboole_0)).
% 36.16/35.64 cnf(6, plain, [-(9 ^ [_13995, _13926, _13856]), in(8 ^ [_13995, _13926, _13856], _13926)], clausify(d2_xboole_0)).
% 36.16/35.64 cnf(7, plain, [-(9 ^ [_13995, _13926, _13856]), in(8 ^ [_13995, _13926, _13856], _13856)], clausify(d2_xboole_0)).
% 36.16/35.64 cnf(8, plain, [-(9 ^ [_13995, _13926, _13856]), -(in(8 ^ [_13995, _13926, _13856], _13995))], clausify(d2_xboole_0)).
% 36.16/35.64 cnf(9, plain, [-(6 ^ [_14159, _13995, _13926, _13856]), in(_14159, _13926)], clausify(d2_xboole_0)).
% 36.16/35.64 cnf(10, plain, [-(7 ^ [_13995, _13926, _13856]), in(_14159, _13995), -(in(_14159, _13856)), -(in(_14159, _13926))], clausify(d2_xboole_0)).
% 36.16/35.64 cnf(11, plain, [-(7 ^ [_13995, _13926, _13856]), -(in(_14159, _13995)), 6 ^ [_14159, _13995, _13926, _13856]], clausify(d2_xboole_0)).
% 36.16/35.64 cnf(12, plain, [-(2 ^ [_13433, _13375]), in(_13565, _13433), -(_13565 = _13375)], clausify(d1_tarski)).
% 36.16/35.64 cnf(13, plain, [-(in(21 ^ [], 22 ^ []))], clausify(t140_zfmisc_1)).
% 36.16/35.64 cnf(14, plain, [set_union2(set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ [])) = 22 ^ []], clausify(t140_zfmisc_1)).
% 36.16/35.64 cnf(15, plain, [-(set_difference(_10706, _10839) = set_difference(_10773, _10904)), _10706 = _10773, _10839 = _10904], theory(equality)).
% 36.16/35.64 cnf(16, plain, [_11944 = _11993, -(singleton(_11944) = singleton(_11993))], theory(equality)).
% 36.16/35.64 cnf(17, plain, [-(set_union2(_11330, _11463) = set_union2(_11397, _11528)), _11330 = _11397, _11463 = _11528], theory(equality)).
% 36.16/35.64 cnf(18, plain, [-(_8186 = _8186)], theory(equality)).
% 36.16/35.64 cnf(19, plain, [_8339 = _8384, -(_8384 = _8339)], theory(equality)).
% 36.16/35.64 cnf(20, plain, [-(in(_9490, _9621)), in(_9423, _9556), _9423 = _9490, _9556 = _9621], theory(equality)).
% 36.16/35.64 cnf(21, plain, [_13433 = singleton(_13375), 2 ^ [_13433, _13375]], clausify(d1_tarski)).
% 36.16/35.64 cnf(22, plain, [-(_13995 = set_union2(_13856, _13926)), 9 ^ [_13995, _13926, _13856], 10 ^ [_13995, _13926, _13856]], clausify(d2_xboole_0)).
% 36.16/35.64 cnf(23, plain, [_13995 = set_union2(_13856, _13926), 7 ^ [_13995, _13926, _13856]], clausify(d2_xboole_0)).
% 36.16/35.64 cnf(24, plain, [_15145 = set_difference(_15002, _15074), 14 ^ [_15145, _15074, _15002]], clausify(d4_xboole_0)).
% 36.16/35.64
% 36.16/35.64 cnf('1',plain,[set_union2(set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ [])) = 22 ^ []],start(14)).
% 36.16/35.64 cnf('1.1',plain,[-(set_union2(set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ [])) = 22 ^ []), 22 ^ [] = set_union2(set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ []))],extension(19,bind([[_8339, _8384], [22 ^ [], set_union2(set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ []))]]))).
% 36.16/35.64 cnf('1.1.1',plain,[-(22 ^ [] = set_union2(set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ []))), 9 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], 10 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))]],extension(22,bind([[_13995, _13926, _13856], [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))]]))).
% 36.16/35.64 cnf('1.1.1.1',plain,[-(9 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))]), in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], singleton(21 ^ []))],extension(6,bind([[_13995, _13856, _13926], [22 ^ [], set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ [])]]))).
% 36.16/35.64 cnf('1.1.1.1.1',plain,[-(in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], singleton(21 ^ []))), -(7 ^ [set_union2(singleton(21 ^ []), 22 ^ []), 22 ^ [], singleton(21 ^ [])]), in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], set_union2(singleton(21 ^ []), 22 ^ [])), -(in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], 22 ^ []))],extension(10,bind([[_13856, _13995, _14159, _13926], [singleton(21 ^ []), set_union2(singleton(21 ^ []), 22 ^ []), 8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], 22 ^ []]]))).
% 36.16/35.64 cnf('1.1.1.1.1.1',plain,[7 ^ [set_union2(singleton(21 ^ []), 22 ^ []), 22 ^ [], singleton(21 ^ [])], set_union2(singleton(21 ^ []), 22 ^ []) = set_union2(singleton(21 ^ []), 22 ^ [])],extension(23,bind([[_13995, _13856, _13926], [set_union2(singleton(21 ^ []), 22 ^ []), singleton(21 ^ []), 22 ^ []]]))).
% 36.16/35.64 cnf('1.1.1.1.1.1.1',plain,[-(set_union2(singleton(21 ^ []), 22 ^ []) = set_union2(singleton(21 ^ []), 22 ^ [])), singleton(21 ^ []) = singleton(21 ^ []), 22 ^ [] = 22 ^ []],extension(17,bind([[_11330, _11397, _11463, _11528], [singleton(21 ^ []), singleton(21 ^ []), 22 ^ [], 22 ^ []]]))).
% 36.16/35.64 cnf('1.1.1.1.1.1.1.1',plain,[-(singleton(21 ^ []) = singleton(21 ^ []))],extension(18,bind([[_8186], [singleton(21 ^ [])]]))).
% 36.16/35.64 cnf('1.1.1.1.1.1.1.2',plain,[-(22 ^ [] = 22 ^ [])],extension(18,bind([[_8186], [22 ^ []]]))).
% 36.16/35.64 cnf('1.1.1.1.1.2',plain,[-(in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], set_union2(singleton(21 ^ []), 22 ^ []))), -(7 ^ [set_union2(singleton(21 ^ []), 22 ^ []), 22 ^ [], singleton(21 ^ [])]), 6 ^ [8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], set_union2(singleton(21 ^ []), 22 ^ []), 22 ^ [], singleton(21 ^ [])]],extension(11,bind([[_14159, _13995, _13926, _13856], [8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], set_union2(singleton(21 ^ []), 22 ^ []), 22 ^ [], singleton(21 ^ [])]]))).
% 36.16/35.64 cnf('1.1.1.1.1.2.1',plain,[7 ^ [set_union2(singleton(21 ^ []), 22 ^ []), 22 ^ [], singleton(21 ^ [])], set_union2(singleton(21 ^ []), 22 ^ []) = set_union2(singleton(21 ^ []), 22 ^ [])],extension(23,bind([[_13995, _13856, _13926], [set_union2(singleton(21 ^ []), 22 ^ []), singleton(21 ^ []), 22 ^ []]]))).
% 36.16/35.64 cnf('1.1.1.1.1.2.1.1',plain,[-(set_union2(singleton(21 ^ []), 22 ^ []) = set_union2(singleton(21 ^ []), 22 ^ []))],extension(18,bind([[_8186], [set_union2(singleton(21 ^ []), 22 ^ [])]]))).
% 36.16/35.64 cnf('1.1.1.1.1.2.2',plain,[-(6 ^ [8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], set_union2(singleton(21 ^ []), 22 ^ []), 22 ^ [], singleton(21 ^ [])]), in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], 22 ^ [])],extension(9,bind([[_13995, _13856, _14159, _13926], [set_union2(singleton(21 ^ []), 22 ^ []), singleton(21 ^ []), 8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], 22 ^ []]]))).
% 36.16/35.64 cnf('1.1.1.1.1.2.2.1',plain,[-(in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], 22 ^ [])), -(9 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))])],extension(8,bind([[_13995, _13926, _13856], [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))]]))).
% 36.16/35.64 cnf('1.1.1.1.1.2.2.1.1',plain,[9 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))]],reduction('1.1.1')).
% 36.16/35.64 cnf('1.1.1.1.1.3',plain,[in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], 22 ^ []), -(14 ^ [set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ []), 22 ^ []]), -(in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], set_difference(22 ^ [], singleton(21 ^ [])))), -(in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], singleton(21 ^ [])))],extension(2,bind([[_15002, _15145, _15311, _15074], [22 ^ [], set_difference(22 ^ [], singleton(21 ^ [])), 8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], singleton(21 ^ [])]]))).
% 36.16/35.64 cnf('1.1.1.1.1.3.1',plain,[14 ^ [set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ []), 22 ^ []], set_difference(22 ^ [], singleton(21 ^ [])) = set_difference(22 ^ [], singleton(21 ^ []))],extension(24,bind([[_15145, _15002, _15074], [set_difference(22 ^ [], singleton(21 ^ [])), 22 ^ [], singleton(21 ^ [])]]))).
% 36.16/35.64 cnf('1.1.1.1.1.3.1.1',plain,[-(set_difference(22 ^ [], singleton(21 ^ [])) = set_difference(22 ^ [], singleton(21 ^ [])))],extension(18,bind([[_8186], [set_difference(22 ^ [], singleton(21 ^ []))]]))).
% 36.16/35.64 cnf('1.1.1.1.1.3.2',plain,[in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], set_difference(22 ^ [], singleton(21 ^ []))), -(9 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))])],extension(7,bind([[_13995, _13926, _13856], [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))]]))).
% 36.16/35.64 cnf('1.1.1.1.1.3.2.1',plain,[9 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))]],reduction('1.1.1')).
% 36.16/35.64 cnf('1.1.1.1.1.3.3',plain,[in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], singleton(21 ^ []))],reduction('1.1.1.1')).
% 36.16/35.64 cnf('1.1.1.2',plain,[-(10 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))]), -(in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], set_difference(22 ^ [], singleton(21 ^ [])))), -(in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], singleton(21 ^ [])))],extension(4,bind([[_13995, _13856, _13926], [22 ^ [], set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ [])]]))).
% 36.16/35.64 cnf('1.1.1.2.1',plain,[in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], set_difference(22 ^ [], singleton(21 ^ []))), -(14 ^ [set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ []), 22 ^ []]), 13 ^ [8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ []), 22 ^ []]],extension(3,bind([[_15311, _15145, _15074, _15002], [8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ []), 22 ^ []]]))).
% 36.16/35.64 cnf('1.1.1.2.1.1',plain,[14 ^ [set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ []), 22 ^ []], set_difference(22 ^ [], singleton(21 ^ [])) = set_difference(22 ^ [], singleton(21 ^ []))],extension(24,bind([[_15145, _15002, _15074], [set_difference(22 ^ [], singleton(21 ^ [])), 22 ^ [], singleton(21 ^ [])]]))).
% 36.16/35.64 cnf('1.1.1.2.1.1.1',plain,[-(set_difference(22 ^ [], singleton(21 ^ [])) = set_difference(22 ^ [], singleton(21 ^ []))), 22 ^ [] = 22 ^ [], singleton(21 ^ []) = singleton(21 ^ [])],extension(15,bind([[_10706, _10773, _10839, _10904], [22 ^ [], 22 ^ [], singleton(21 ^ []), singleton(21 ^ [])]]))).
% 36.16/35.64 cnf('1.1.1.2.1.1.1.1',plain,[-(22 ^ [] = 22 ^ [])],extension(18,bind([[_8186], [22 ^ []]]))).
% 36.16/35.64 cnf('1.1.1.2.1.1.1.2',plain,[-(singleton(21 ^ []) = singleton(21 ^ []))],extension(18,bind([[_8186], [singleton(21 ^ [])]]))).
% 36.16/35.64 cnf('1.1.1.2.1.2',plain,[-(13 ^ [8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ []), 22 ^ []]), -(in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], 22 ^ []))],extension(1,bind([[_15145, _15074, _15311, _15002], [set_difference(22 ^ [], singleton(21 ^ [])), singleton(21 ^ []), 8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], 22 ^ []]]))).
% 36.16/35.64 cnf('1.1.1.2.1.2.1',plain,[in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], 22 ^ []), -(10 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))])],extension(5,bind([[_13995, _13926, _13856], [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))]]))).
% 36.16/35.64 cnf('1.1.1.2.1.2.1.1',plain,[10 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))]],reduction('1.1.1')).
% 36.16/35.64 cnf('1.1.1.2.2',plain,[in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], singleton(21 ^ [])), -(2 ^ [singleton(21 ^ []), 21 ^ []]), -(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))] = 21 ^ [])],extension(12,bind([[_13433, _13565, _13375], [singleton(21 ^ []), 8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], 21 ^ []]]))).
% 36.16/35.64 cnf('1.1.1.2.2.1',plain,[2 ^ [singleton(21 ^ []), 21 ^ []], singleton(21 ^ []) = singleton(21 ^ [])],extension(21,bind([[_13433, _13375], [singleton(21 ^ []), 21 ^ []]]))).
% 36.16/35.64 cnf('1.1.1.2.2.1.1',plain,[-(singleton(21 ^ []) = singleton(21 ^ [])), 21 ^ [] = 21 ^ []],extension(16,bind([[_11944, _11993], [21 ^ [], 21 ^ []]]))).
% 36.16/35.64 cnf('1.1.1.2.2.1.1.1',plain,[-(21 ^ [] = 21 ^ [])],extension(18,bind([[_8186], [21 ^ []]]))).
% 36.16/35.64 cnf('1.1.1.2.2.2',plain,[8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))] = 21 ^ [], -(21 ^ [] = 8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))])],extension(19,bind([[_8384, _8339], [21 ^ [], 8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))]]]))).
% 36.16/35.64 cnf('1.1.1.2.2.2.1',plain,[21 ^ [] = 8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], -(in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], 22 ^ [])), in(21 ^ [], 22 ^ []), 22 ^ [] = 22 ^ []],extension(20,bind([[_9490, _9423, _9556, _9621], [8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], 21 ^ [], 22 ^ [], 22 ^ []]]))).
% 36.16/35.64 cnf('1.1.1.2.2.2.1.1',plain,[in(8 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))], 22 ^ []), -(10 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))])],extension(5,bind([[_13995, _13926, _13856], [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))]]))).
% 36.16/35.64 cnf('1.1.1.2.2.2.1.1.1',plain,[10 ^ [22 ^ [], singleton(21 ^ []), set_difference(22 ^ [], singleton(21 ^ []))]],reduction('1.1.1')).
% 36.16/35.64 cnf('1.1.1.2.2.2.1.2',plain,[-(in(21 ^ [], 22 ^ []))],extension(13)).
% 36.16/35.64 cnf('1.1.1.2.2.2.1.3',plain,[-(22 ^ [] = 22 ^ [])],extension(18,bind([[_8186], [22 ^ []]]))).
% 36.16/35.64 %-----------------------------------------------------
% 36.16/35.65
% 36.16/35.65 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------