%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET612+3 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n013.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:54:45 EDT 2022
% Result : Theorem 2.59s 3.48s
% Output : Proof 2.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET612+3 : TPTP v8.1.0. Released v2.2.0.
% 0.07/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n013.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Mon Jul 11 06:48:44 EDT 2022
% 0.12/0.34 % CPUTime :
% 2.59/3.48 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.59/3.49 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.59/3.50
% 2.59/3.50 %-----------------------------------------------------
% 2.59/3.50 fof(prove_th85, conjecture, ! [_42114, _42117, _42120] : difference(_42114, union(_42117, _42120)) = intersection(difference(_42114, _42117), difference(_42114, _42120)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_th85)).
% 2.59/3.50 fof(union_defn, axiom, ! [_42360, _42363, _42366] : (member(_42366, union(_42360, _42363)) <=> member(_42366, _42360) | member(_42366, _42363)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', union_defn)).
% 2.59/3.50 fof(intersection_defn, axiom, ! [_42585, _42588, _42591] : (member(_42591, intersection(_42585, _42588)) <=> member(_42591, _42585) & member(_42591, _42588)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', intersection_defn)).
% 2.59/3.50 fof(difference_defn, axiom, ! [_42810, _42813, _42816] : (member(_42816, difference(_42810, _42813)) <=> member(_42816, _42810) & ~ member(_42816, _42813)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', difference_defn)).
% 2.59/3.50 fof(commutativity_of_union, axiom, ! [_43048, _43051] : union(_43048, _43051) = union(_43051, _43048), file('/export/starexec/sandbox/benchmark/theBenchmark.p', commutativity_of_union)).
% 2.59/3.50 fof(equal_member_defn, axiom, ! [_43201, _43204] : (_43201 = _43204 <=> ! [_43218] : (member(_43218, _43201) <=> member(_43218, _43204))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', equal_member_defn)).
% 2.59/3.50
% 2.59/3.50 cnf(1, plain, [difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))], clausify(prove_th85)).
% 2.59/3.50 cnf(2, plain, [-(_7544 = _7544)], theory(equality)).
% 2.59/3.50 cnf(3, plain, [_7697 = _7742, -(_7742 = _7697)], theory(equality)).
% 2.59/3.50 cnf(4, plain, [-(member(_8519, _8650)), member(_8452, _8585), _8452 = _8519, _8585 = _8650], theory(equality)).
% 2.59/3.50 cnf(5, plain, [-(member(_11765, union(_11648, _11707))), member(_11765, _11648)], clausify(union_defn)).
% 2.59/3.50 cnf(6, plain, [-(member(_11765, union(_11648, _11707))), member(_11765, _11707)], clausify(union_defn)).
% 2.59/3.50 cnf(7, plain, [member(_11765, union(_11648, _11707)), -(member(_11765, _11648)), -(member(_11765, _11707))], clausify(union_defn)).
% 2.59/3.50 cnf(8, plain, [member(_12278, intersection(_12161, _12220)), -(member(_12278, _12161))], clausify(intersection_defn)).
% 2.59/3.50 cnf(9, plain, [member(_12278, intersection(_12161, _12220)), -(member(_12278, _12220))], clausify(intersection_defn)).
% 2.59/3.50 cnf(10, plain, [-(member(_12278, intersection(_12161, _12220))), member(_12278, _12161), member(_12278, _12220)], clausify(intersection_defn)).
% 2.59/3.50 cnf(11, plain, [member(_12795, difference(_12674, _12735)), -(member(_12795, _12674))], clausify(difference_defn)).
% 2.59/3.50 cnf(12, plain, [member(_12795, difference(_12674, _12735)), member(_12795, _12735)], clausify(difference_defn)).
% 2.59/3.50 cnf(13, plain, [-(member(_12795, difference(_12674, _12735))), member(_12795, _12674), -(member(_12795, _12735))], clausify(difference_defn)).
% 2.59/3.50 cnf(14, plain, [-(union(_14852, _14897) = union(_14897, _14852))], clausify(commutativity_of_union)).
% 2.59/3.50 cnf(15, plain, [-(_16097 = _16153), member(2 ^ [_16153, _16097], _16097), member(2 ^ [_16153, _16097], _16153)], clausify(equal_member_defn)).
% 2.59/3.50 cnf(16, plain, [-(_16097 = _16153), -(member(2 ^ [_16153, _16097], _16097)), -(member(2 ^ [_16153, _16097], _16153))], clausify(equal_member_defn)).
% 2.59/3.50
% 2.59/3.50 cnf('1',plain,[difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))],start(1)).
% 2.59/3.50 cnf('1.1',plain,[-(difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ []))), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))],extension(15,bind([[_16097, _16153], [difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))]]))).
% 2.59/3.50 cnf('1.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ [])))), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ []), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(4 ^ [], 5 ^ [])))],extension(13,bind([[_12674, _12795, _12735], [3 ^ [], 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(4 ^ [], 5 ^ [])]]))).
% 2.59/3.50 cnf('1.1.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ [])), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(3 ^ [], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))))],extension(7,bind([[_11648, _11765, _11707], [3 ^ [], 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))]]))).
% 2.59/3.50 cnf('1.1.1.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(3 ^ [], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))))), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), 3 ^ [])), 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))] = 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), 3 ^ []) = union(3 ^ [], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))],extension(4,bind([[_8452, _8519, _8585, _8650], [2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), 3 ^ []), union(3 ^ [], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))]]))).
% 2.59/3.50 cnf('1.1.1.1.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), 3 ^ []))), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))],extension(5,bind([[_11707, _11765, _11648], [3 ^ [], 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))]]))).
% 2.59/3.50 cnf('1.1.1.1.1.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))), -(difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ []))))],extension(16,bind([[_16153, _16097], [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))]]))).
% 2.59/3.50 cnf('1.1.1.1.1.1.1.1',plain,[difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))],extension(1)).
% 2.59/3.50 cnf('1.1.1.1.1.1.1.2',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ [])))],reduction('1.1')).
% 2.59/3.50 cnf('1.1.1.1.1.2',plain,[-(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))] = 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))])],extension(2,bind([[_7544], [2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))]]]))).
% 2.59/3.50 cnf('1.1.1.1.1.3',plain,[-(union(intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), 3 ^ []) = union(3 ^ [], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))), union(3 ^ [], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))) = union(intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), 3 ^ [])],extension(3,bind([[_7697, _7742], [union(3 ^ [], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))), union(intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), 3 ^ [])]]))).
% 2.59/3.50 cnf('1.1.1.1.1.3.1',plain,[-(union(3 ^ [], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))) = union(intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), 3 ^ []))],extension(14,bind([[_14897, _14852], [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), 3 ^ []]]))).
% 2.59/3.50 cnf('1.1.1.1.2',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], 4 ^ [])))],extension(8,bind([[_12220, _12278, _12161], [difference(3 ^ [], 5 ^ []), 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], 4 ^ [])]]))).
% 2.59/3.50 cnf('1.1.1.1.2.1',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], 4 ^ [])), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ []))],extension(11,bind([[_12735, _12795, _12674], [4 ^ [], 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ []]]))).
% 2.59/3.50 cnf('1.1.1.1.2.1.1',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ [])],reduction('1.1.1')).
% 2.59/3.50 cnf('1.1.1.2',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(4 ^ [], 5 ^ [])), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 4 ^ [])), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 5 ^ []))],extension(7,bind([[_11648, _11765, _11707], [4 ^ [], 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 5 ^ []]]))).
% 2.59/3.50 cnf('1.1.1.2.1',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 4 ^ []), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], 4 ^ []))],extension(12,bind([[_12795, _12674, _12735], [2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ [], 4 ^ []]]))).
% 2.59/3.50 cnf('1.1.1.2.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], 4 ^ []))), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))],extension(8,bind([[_12278, _12161, _12220], [2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])]]))).
% 2.59/3.50 cnf('1.1.1.2.1.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))), -(difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ []))))],extension(16,bind([[_16153, _16097], [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))]]))).
% 2.59/3.50 cnf('1.1.1.2.1.1.1.1',plain,[difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))],extension(1)).
% 2.59/3.50 cnf('1.1.1.2.1.1.1.2',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ [])))],reduction('1.1')).
% 2.59/3.50 cnf('1.1.1.2.2',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 5 ^ []), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], 5 ^ []))],extension(12,bind([[_12795, _12674, _12735], [2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ [], 5 ^ []]]))).
% 2.59/3.50 cnf('1.1.1.2.2.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], 5 ^ []))), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))],extension(9,bind([[_12278, _12161, _12220], [2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])]]))).
% 2.59/3.50 cnf('1.1.1.2.2.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))), -(difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ []))))],extension(16,bind([[_16153, _16097], [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))]]))).
% 2.59/3.50 cnf('1.1.1.2.2.1.1.1',plain,[difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))],extension(1)).
% 2.59/3.50 cnf('1.1.1.2.2.1.1.2',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ [])))],reduction('1.1')).
% 2.59/3.50 cnf('1.1.2',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], 4 ^ [])), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], 5 ^ []))],extension(10,bind([[_12161, _12278, _12220], [difference(3 ^ [], 4 ^ []), 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], 5 ^ [])]]))).
% 2.59/3.50 cnf('1.1.2.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], 4 ^ []))), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ []), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 4 ^ []))],extension(13,bind([[_12674, _12795, _12735], [3 ^ [], 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 4 ^ []]]))).
% 2.59/3.50 cnf('1.1.2.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ [])), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(3 ^ [], difference(3 ^ [], union(4 ^ [], 5 ^ [])))), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ []))))],extension(7,bind([[_11648, _11765, _11707], [3 ^ [], 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ []))]]))).
% 2.59/3.50 cnf('1.1.2.1.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(3 ^ [], difference(3 ^ [], union(4 ^ [], 5 ^ []))))), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ [])))],extension(6,bind([[_11648, _11765, _11707], [3 ^ [], 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ []))]]))).
% 2.59/3.50 cnf('1.1.2.1.1.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ [])))), -(difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))))],extension(16,bind([[_16097, _16153], [difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))]]))).
% 2.59/3.50 cnf('1.1.2.1.1.1.1.1',plain,[difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))],extension(1)).
% 2.59/3.50 cnf('1.1.2.1.1.1.1.2',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))],reduction('1.1')).
% 2.59/3.50 cnf('1.1.2.1.1.2',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ []))), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ []))],extension(11,bind([[_12735, _12795, _12674], [union(4 ^ [], 5 ^ []), 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ []]]))).
% 2.59/3.50 cnf('1.1.2.1.1.2.1',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ [])],reduction('1.1.2.1')).
% 2.59/3.50 cnf('1.1.2.1.2',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 4 ^ []), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(4 ^ [], 5 ^ [])))],extension(5,bind([[_11765, _11648, _11707], [2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 4 ^ [], 5 ^ []]]))).
% 2.59/3.50 cnf('1.1.2.1.2.1',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(4 ^ [], 5 ^ [])), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ [])))],extension(12,bind([[_12795, _12674, _12735], [2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ [], union(4 ^ [], 5 ^ [])]]))).
% 2.59/3.50 cnf('1.1.2.1.2.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ [])))), -(difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))))],extension(16,bind([[_16097, _16153], [difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))]]))).
% 2.59/3.50 cnf('1.1.2.1.2.1.1.1',plain,[difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))],extension(1)).
% 2.59/3.50 cnf('1.1.2.1.2.1.1.2',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))],reduction('1.1')).
% 2.59/3.50 cnf('1.1.2.2',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], 5 ^ []))), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ []), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 5 ^ []))],extension(13,bind([[_12674, _12795, _12735], [3 ^ [], 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 5 ^ []]]))).
% 2.59/3.50 cnf('1.1.2.2.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ [])), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(3 ^ [], difference(3 ^ [], union(4 ^ [], 5 ^ [])))), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ []))))],extension(7,bind([[_11648, _11765, _11707], [3 ^ [], 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ []))]]))).
% 2.59/3.50 cnf('1.1.2.2.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(3 ^ [], difference(3 ^ [], union(4 ^ [], 5 ^ []))))), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ [])))],extension(6,bind([[_11648, _11765, _11707], [3 ^ [], 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ []))]]))).
% 2.59/3.50 cnf('1.1.2.2.1.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ [])))), -(difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))))],extension(16,bind([[_16097, _16153], [difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))]]))).
% 2.59/3.50 cnf('1.1.2.2.1.1.1.1',plain,[difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))],extension(1)).
% 2.59/3.50 cnf('1.1.2.2.1.1.1.2',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))],reduction('1.1')).
% 2.59/3.50 cnf('1.1.2.2.1.2',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ []))), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ []))],extension(11,bind([[_12735, _12795, _12674], [union(4 ^ [], 5 ^ []), 2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ []]]))).
% 2.59/3.50 cnf('1.1.2.2.1.2.1',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ [])],reduction('1.1.2.2')).
% 2.59/3.50 cnf('1.1.2.2.2',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 5 ^ []), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(4 ^ [], 5 ^ [])))],extension(6,bind([[_11765, _11648, _11707], [2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 4 ^ [], 5 ^ []]]))).
% 2.59/3.50 cnf('1.1.2.2.2.1',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], union(4 ^ [], 5 ^ [])), member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ [])))],extension(12,bind([[_12795, _12674, _12735], [2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], 3 ^ [], union(4 ^ [], 5 ^ [])]]))).
% 2.59/3.50 cnf('1.1.2.2.2.1.1',plain,[-(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], difference(3 ^ [], union(4 ^ [], 5 ^ [])))), -(difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))), -(member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))))],extension(16,bind([[_16097, _16153], [difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))]]))).
% 2.59/3.50 cnf('1.1.2.2.2.1.1.1',plain,[difference(3 ^ [], union(4 ^ [], 5 ^ [])) = intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ []))],extension(1)).
% 2.59/3.50 cnf('1.1.2.2.2.1.1.2',plain,[member(2 ^ [intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ []))], intersection(difference(3 ^ [], 4 ^ []), difference(3 ^ [], 5 ^ [])))],reduction('1.1')).
% 2.59/3.50 %-----------------------------------------------------
% 2.59/3.50
% 2.59/3.50 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------