%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET156+4 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n004.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:51:55 EDT 2022
% Result : Theorem 79.05s 76.90s
% Output : Proof 79.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SET156+4 : TPTP v8.1.0. Released v2.2.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n004.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 : Sat Jul 9 21:09:22 EDT 2022
% 0.12/0.33 % CPUTime :
% 79.05/76.90 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 79.05/76.91 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 79.05/76.91
% 79.05/76.91 %-----------------------------------------------------
% 79.05/76.91 fof(thI25, conjecture, ! [_43283, _43286, _43289] : (subset(_43283, _43289) & subset(_43286, _43289) => equal_set(difference(_43289, intersection(_43283, _43286)), union(difference(_43289, _43283), difference(_43289, _43286)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', thI25)).
% 79.05/76.91 fof(subset, axiom, ! [_43596, _43599] : (subset(_43596, _43599) <=> ! [_43617] : (member(_43617, _43596) => member(_43617, _43599))), file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', subset)).
% 79.05/76.91 fof(equal_set, axiom, ! [_43826, _43829] : (equal_set(_43826, _43829) <=> subset(_43826, _43829) & subset(_43829, _43826)), file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', equal_set)).
% 79.05/76.91 fof(intersection, axiom, ! [_44002, _44005, _44008] : (member(_44002, intersection(_44005, _44008)) <=> member(_44002, _44005) & member(_44002, _44008)), file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', intersection)).
% 79.05/76.91 fof(union, axiom, ! [_44227, _44230, _44233] : (member(_44227, union(_44230, _44233)) <=> member(_44227, _44230) | member(_44227, _44233)), file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', union)).
% 79.05/76.91 fof(difference, axiom, ! [_44453, _44456, _44459] : (member(_44453, difference(_44459, _44456)) <=> member(_44453, _44459) & ~ member(_44453, _44456)), file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', difference)).
% 79.05/76.91
% 79.05/76.91 cnf(1, plain, [-(subset(4 ^ [], 6 ^ []))], clausify(thI25)).
% 79.05/76.91 cnf(2, plain, [equal_set(difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])))], clausify(thI25)).
% 79.05/76.91 cnf(3, plain, [-(_8170 = _8170)], theory(equality)).
% 79.05/76.91 cnf(4, plain, [-(member(_9769, _9900)), member(_9702, _9835), _9702 = _9769, _9835 = _9900], theory(equality)).
% 79.05/76.91 cnf(5, plain, [-(subset(_14928, _14984)), -(member(1 ^ [_14984, _14928], _14928))], clausify(subset)).
% 79.05/76.91 cnf(6, plain, [-(subset(_14928, _14984)), member(1 ^ [_14984, _14928], _14984)], clausify(subset)).
% 79.05/76.91 cnf(7, plain, [subset(_14928, _14984), member(_15098, _14928), -(member(_15098, _14984))], clausify(subset)).
% 79.05/76.91 cnf(8, plain, [-(equal_set(_15389, _15440)), subset(_15389, _15440), subset(_15440, _15389)], clausify(equal_set)).
% 79.05/76.91 cnf(9, plain, [member(_16115, intersection(_16174, _16232)), -(member(_16115, _16174))], clausify(intersection)).
% 79.05/76.91 cnf(10, plain, [member(_16115, intersection(_16174, _16232)), -(member(_16115, _16232))], clausify(intersection)).
% 79.05/76.91 cnf(11, plain, [-(member(_16115, intersection(_16174, _16232))), member(_16115, _16174), member(_16115, _16232)], clausify(intersection)).
% 79.05/76.91 cnf(12, plain, [-(member(_16628, union(_16687, _16745))), member(_16628, _16687)], clausify(union)).
% 79.05/76.91 cnf(13, plain, [-(member(_16628, union(_16687, _16745))), member(_16628, _16745)], clausify(union)).
% 79.05/76.91 cnf(14, plain, [member(_16628, union(_16687, _16745)), -(member(_16628, _16687)), -(member(_16628, _16745))], clausify(union)).
% 79.05/76.91 cnf(15, plain, [member(_17333, difference(_17454, _17394)), -(member(_17333, _17454))], clausify(difference)).
% 79.05/76.91 cnf(16, plain, [member(_17333, difference(_17454, _17394)), member(_17333, _17394)], clausify(difference)).
% 79.05/76.91 cnf(17, plain, [-(member(_17333, difference(_17454, _17394))), member(_17333, _17454), -(member(_17333, _17394))], clausify(difference)).
% 79.05/76.91
% 79.05/76.91 cnf('1',plain,[equal_set(difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])))],start(2)).
% 79.05/76.91 cnf('1.1',plain,[-(equal_set(difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])))), subset(difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))), subset(union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))],extension(8,bind([[_15440, _15389], [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.1',plain,[-(subset(difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])))), -(member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ []))))],extension(5,bind([[_14984, _14928], [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.1.1',plain,[member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ []))), member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], intersection(4 ^ [], 5 ^ []))],extension(16,bind([[_17454, _17333, _17394], [6 ^ [], 1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], intersection(4 ^ [], 5 ^ [])]]))).
% 79.05/76.91 cnf('1.1.1.1.1',plain,[-(member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], intersection(4 ^ [], 5 ^ []))), member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 4 ^ []), member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 5 ^ [])],extension(11,bind([[_16174, _16115, _16232], [4 ^ [], 1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 5 ^ []]]))).
% 79.05/76.91 cnf('1.1.1.1.1.1',plain,[-(member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 4 ^ [])), -(member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], difference(6 ^ [], 4 ^ []))), member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 6 ^ [])],extension(17,bind([[_17394, _17333, _17454], [4 ^ [], 1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 6 ^ []]]))).
% 79.05/76.91 cnf('1.1.1.1.1.1.1',plain,[member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], difference(6 ^ [], 4 ^ [])), -(member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))))],extension(12,bind([[_16628, _16687, _16745], [1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])]]))).
% 79.05/76.91 cnf('1.1.1.1.1.1.1.1',plain,[member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))), -(subset(difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))))],extension(6,bind([[_14928, _14984], [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.1.1.1.1.1.1.1',plain,[subset(difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])))],reduction('1.1')).
% 79.05/76.91 cnf('1.1.1.1.1.1.2',plain,[-(member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 6 ^ [])), member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))],extension(15,bind([[_17333, _17454, _17394], [1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 6 ^ [], intersection(4 ^ [], 5 ^ [])]]))).
% 79.05/76.91 cnf('1.1.1.1.1.1.2.1',plain,[-(member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ []))))],reduction('1.1.1')).
% 79.05/76.91 cnf('1.1.1.1.1.2',plain,[-(member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 5 ^ [])), -(member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], difference(6 ^ [], 5 ^ []))), member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 6 ^ [])],extension(17,bind([[_17394, _17333, _17454], [5 ^ [], 1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 6 ^ []]]))).
% 79.05/76.91 cnf('1.1.1.1.1.2.1',plain,[member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], difference(6 ^ [], 5 ^ [])), -(member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))))],extension(13,bind([[_16628, _16687, _16745], [1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])]]))).
% 79.05/76.91 cnf('1.1.1.1.1.2.1.1',plain,[member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))), -(subset(difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))))],extension(6,bind([[_14928, _14984], [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.1.1.1.2.1.1.1',plain,[subset(difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])))],reduction('1.1')).
% 79.05/76.91 cnf('1.1.1.1.1.2.2',plain,[-(member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 6 ^ [])), subset(4 ^ [], 6 ^ []), member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 4 ^ [])],extension(7,bind([[_14984, _15098, _14928], [6 ^ [], 1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 4 ^ []]]))).
% 79.05/76.91 cnf('1.1.1.1.1.2.2.1',plain,[-(subset(4 ^ [], 6 ^ []))],extension(1)).
% 79.05/76.91 cnf('1.1.1.1.1.2.2.2',plain,[-(member(1 ^ [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))], 4 ^ []))],lemmata('1.1.1.1.1')).
% 79.05/76.91 cnf('1.1.2',plain,[-(subset(union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))), -(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))))],extension(5,bind([[_14984, _14928], [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.2.1',plain,[member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))), -(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], 4 ^ []))), -(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], 5 ^ [])))],extension(14,bind([[_16687, _16628, _16745], [difference(6 ^ [], 4 ^ []), 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], 5 ^ [])]]))).
% 79.05/76.91 cnf('1.1.2.1.1',plain,[member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], 4 ^ [])), -(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], intersection(difference(6 ^ [], 4 ^ []), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))))), member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))],extension(11,bind([[_16174, _16115, _16232], [difference(6 ^ [], 4 ^ []), 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.2.1.1.1',plain,[member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], intersection(difference(6 ^ [], 4 ^ []), difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))), -(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ []))))],extension(10,bind([[_16174, _16115, _16232], [difference(6 ^ [], 4 ^ []), 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.2.1.1.1.1',plain,[member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ []))), -(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))), 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))] = 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ [])) = difference(6 ^ [], intersection(4 ^ [], 5 ^ []))],extension(4,bind([[_9702, _9769, _9835, _9900], [1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.2.1.1.1.1.1',plain,[member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ []))), -(subset(union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))))],extension(6,bind([[_14928, _14984], [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.2.1.1.1.1.1.1',plain,[subset(union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))],reduction('1.1')).
% 79.05/76.91 cnf('1.1.2.1.1.1.1.2',plain,[-(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))] = 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))])],extension(3,bind([[_8170], [1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))]]]))).
% 79.05/76.91 cnf('1.1.2.1.1.1.1.3',plain,[-(difference(6 ^ [], intersection(4 ^ [], 5 ^ [])) = difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))],extension(3,bind([[_8170], [difference(6 ^ [], intersection(4 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.2.1.1.2',plain,[-(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))), member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 6 ^ []), -(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], intersection(4 ^ [], 5 ^ [])))],extension(17,bind([[_17454, _17333, _17394], [6 ^ [], 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], intersection(4 ^ [], 5 ^ [])]]))).
% 79.05/76.91 cnf('1.1.2.1.1.2.1',plain,[-(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 6 ^ [])), member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], 4 ^ []))],extension(15,bind([[_17333, _17454, _17394], [1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 6 ^ [], 4 ^ []]]))).
% 79.05/76.91 cnf('1.1.2.1.1.2.1.1',plain,[-(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], 4 ^ [])))],reduction('1.1.2.1')).
% 79.05/76.91 cnf('1.1.2.1.1.2.2',plain,[member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], intersection(4 ^ [], 5 ^ [])), -(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 4 ^ []))],extension(9,bind([[_16232, _16115, _16174], [5 ^ [], 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 4 ^ []]]))).
% 79.05/76.91 cnf('1.1.2.1.1.2.2.1',plain,[member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 4 ^ []), member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], 4 ^ []))],extension(16,bind([[_17333, _17454, _17394], [1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 6 ^ [], 4 ^ []]]))).
% 79.05/76.91 cnf('1.1.2.1.1.2.2.1.1',plain,[-(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], 4 ^ [])))],reduction('1.1.2.1')).
% 79.05/76.91 cnf('1.1.2.1.2',plain,[member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], 5 ^ [])), -(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], intersection(difference(6 ^ [], 5 ^ []), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))))), member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))],extension(11,bind([[_16174, _16115, _16232], [difference(6 ^ [], 5 ^ []), 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.2.1.2.1',plain,[member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], intersection(difference(6 ^ [], 5 ^ []), difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))), -(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ []))))],extension(10,bind([[_16174, _16115, _16232], [difference(6 ^ [], 5 ^ []), 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.2.1.2.1.1',plain,[member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ []))), -(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))), 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))] = 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ [])) = difference(6 ^ [], intersection(4 ^ [], 5 ^ []))],extension(4,bind([[_9702, _9769, _9835, _9900], [1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.2.1.2.1.1.1',plain,[member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ []))), -(subset(union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))))],extension(6,bind([[_14928, _14984], [union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.2.1.2.1.1.1.1',plain,[subset(union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ [])), difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))],reduction('1.1')).
% 79.05/76.91 cnf('1.1.2.1.2.1.1.2',plain,[-(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))] = 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))])],extension(3,bind([[_8170], [1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))]]]))).
% 79.05/76.91 cnf('1.1.2.1.2.1.1.3',plain,[-(difference(6 ^ [], intersection(4 ^ [], 5 ^ [])) = difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))],extension(3,bind([[_8170], [difference(6 ^ [], intersection(4 ^ [], 5 ^ []))]]))).
% 79.05/76.91 cnf('1.1.2.1.2.2',plain,[-(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], intersection(4 ^ [], 5 ^ [])))), member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 6 ^ []), -(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], intersection(4 ^ [], 5 ^ [])))],extension(17,bind([[_17454, _17333, _17394], [6 ^ [], 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], intersection(4 ^ [], 5 ^ [])]]))).
% 79.05/76.91 cnf('1.1.2.1.2.2.1',plain,[-(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 6 ^ [])), member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], 5 ^ []))],extension(15,bind([[_17333, _17454, _17394], [1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 6 ^ [], 5 ^ []]]))).
% 79.05/76.91 cnf('1.1.2.1.2.2.1.1',plain,[-(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], 5 ^ [])))],reduction('1.1.2.1')).
% 79.05/76.91 cnf('1.1.2.1.2.2.2',plain,[member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], intersection(4 ^ [], 5 ^ [])), -(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 5 ^ []))],extension(10,bind([[_16174, _16115, _16232], [4 ^ [], 1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 5 ^ []]]))).
% 79.05/76.91 cnf('1.1.2.1.2.2.2.1',plain,[member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 5 ^ []), member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], 5 ^ []))],extension(16,bind([[_17333, _17454, _17394], [1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], 6 ^ [], 5 ^ []]]))).
% 79.05/76.91 cnf('1.1.2.1.2.2.2.1.1',plain,[-(member(1 ^ [difference(6 ^ [], intersection(4 ^ [], 5 ^ [])), union(difference(6 ^ [], 4 ^ []), difference(6 ^ [], 5 ^ []))], difference(6 ^ [], 5 ^ [])))],reduction('1.1.2.1')).
% 79.05/76.91 %-----------------------------------------------------
% 79.05/76.92
% 79.05/76.92 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------