%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET622+3 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n008.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:52 EDT 2022
% Result : Theorem 14.72s 14.93s
% Output : Proof 14.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SET622+3 : TPTP v8.1.0. Released v2.2.0.
% 0.08/0.14 % Command : leancop_casc.sh %s %d
% 0.13/0.35 % Computer : n008.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Sun Jul 10 00:30:38 EDT 2022
% 0.13/0.35 % CPUTime :
% 14.72/14.93 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.72/14.94 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.72/14.95
% 14.72/14.95 %-----------------------------------------------------
% 14.72/14.95 fof(prove_th98, conjecture, ! [_30978, _30981, _30984] : difference(_30978, symmetric_difference(_30981, _30984)) = union(difference(_30978, union(_30981, _30984)), intersection(intersection(_30978, _30981), _30984)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_th98)).
% 14.72/14.95 fof(associativity_of_intersection, axiom, ! [_31279, _31282, _31285] : intersection(intersection(_31279, _31282), _31285) = intersection(_31279, intersection(_31282, _31285)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', associativity_of_intersection)).
% 14.72/14.95 fof(difference_difference_union2, axiom, ! [_31468, _31471, _31474] : difference(_31468, difference(_31471, _31474)) = union(difference(_31468, _31471), intersection(_31468, _31474)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', difference_difference_union2)).
% 14.72/14.95 fof(symmetric_difference_and_difference, axiom, ! [_31673, _31676] : symmetric_difference(_31673, _31676) = difference(union(_31673, _31676), intersection(_31673, _31676)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', symmetric_difference_and_difference)).
% 14.72/14.95
% 14.72/14.95 cnf(1, plain, [difference(3 ^ [], symmetric_difference(4 ^ [], 5 ^ [])) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(intersection(3 ^ [], 4 ^ []), 5 ^ []))], clausify(prove_th98)).
% 14.72/14.95 cnf(2, plain, [-(difference(_10619, _10752) = difference(_10686, _10817)), _10619 = _10686, _10752 = _10817], theory(equality)).
% 14.72/14.95 cnf(3, plain, [-(union(_12481, _12614) = union(_12548, _12679)), _12481 = _12548, _12614 = _12679], theory(equality)).
% 14.72/14.95 cnf(4, plain, [-(_8443 = _8443)], theory(equality)).
% 14.72/14.95 cnf(5, plain, [_8596 = _8641, -(_8641 = _8596)], theory(equality)).
% 14.72/14.95 cnf(6, plain, [-(_8875 = _8986), _8875 = _8931, _8931 = _8986], theory(equality)).
% 14.72/14.95 cnf(7, plain, [-(intersection(intersection(_13186, _13242), _13297) = intersection(_13186, intersection(_13242, _13297)))], clausify(associativity_of_intersection)).
% 14.72/14.95 cnf(8, plain, [-(difference(_13653, difference(_13712, _13770)) = union(difference(_13653, _13712), intersection(_13653, _13770)))], clausify(difference_difference_union2)).
% 14.72/14.95 cnf(9, plain, [-(symmetric_difference(_14166, _14217) = difference(union(_14166, _14217), intersection(_14166, _14217)))], clausify(symmetric_difference_and_difference)).
% 14.72/14.95
% 14.72/14.95 cnf('1',plain,[difference(3 ^ [], symmetric_difference(4 ^ [], 5 ^ [])) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(intersection(3 ^ [], 4 ^ []), 5 ^ []))],start(1)).
% 14.72/14.95 cnf('1.1',plain,[-(difference(3 ^ [], symmetric_difference(4 ^ [], 5 ^ [])) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(intersection(3 ^ [], 4 ^ []), 5 ^ []))), difference(3 ^ [], symmetric_difference(4 ^ [], 5 ^ [])) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ []))), union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ []))) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(intersection(3 ^ [], 4 ^ []), 5 ^ []))],extension(6,bind([[_8875, _8931, _8986], [difference(3 ^ [], symmetric_difference(4 ^ [], 5 ^ [])), union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ []))), union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(intersection(3 ^ [], 4 ^ []), 5 ^ []))]]))).
% 14.72/14.95 cnf('1.1.1',plain,[-(difference(3 ^ [], symmetric_difference(4 ^ [], 5 ^ [])) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ [])))), difference(3 ^ [], symmetric_difference(4 ^ [], 5 ^ [])) = difference(3 ^ [], difference(union(4 ^ [], 5 ^ []), intersection(4 ^ [], 5 ^ []))), difference(3 ^ [], difference(union(4 ^ [], 5 ^ []), intersection(4 ^ [], 5 ^ []))) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ [])))],extension(6,bind([[_8875, _8931, _8986], [difference(3 ^ [], symmetric_difference(4 ^ [], 5 ^ [])), difference(3 ^ [], difference(union(4 ^ [], 5 ^ []), intersection(4 ^ [], 5 ^ []))), union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ [])))]]))).
% 14.72/14.95 cnf('1.1.1.1',plain,[-(difference(3 ^ [], symmetric_difference(4 ^ [], 5 ^ [])) = difference(3 ^ [], difference(union(4 ^ [], 5 ^ []), intersection(4 ^ [], 5 ^ [])))), 3 ^ [] = 3 ^ [], symmetric_difference(4 ^ [], 5 ^ []) = difference(union(4 ^ [], 5 ^ []), intersection(4 ^ [], 5 ^ []))],extension(2,bind([[_10619, _10686, _10752, _10817], [3 ^ [], 3 ^ [], symmetric_difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), intersection(4 ^ [], 5 ^ []))]]))).
% 14.72/14.95 cnf('1.1.1.1.1',plain,[-(3 ^ [] = 3 ^ [])],extension(4,bind([[_8443], [3 ^ []]]))).
% 14.72/14.95 cnf('1.1.1.1.2',plain,[-(symmetric_difference(4 ^ [], 5 ^ []) = difference(union(4 ^ [], 5 ^ []), intersection(4 ^ [], 5 ^ [])))],extension(9,bind([[_14166, _14217], [4 ^ [], 5 ^ []]]))).
% 14.72/14.95 cnf('1.1.1.2',plain,[-(difference(3 ^ [], difference(union(4 ^ [], 5 ^ []), intersection(4 ^ [], 5 ^ []))) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ [])))), difference(3 ^ [], difference(union(4 ^ [], 5 ^ []), intersection(4 ^ [], 5 ^ []))) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ []))), union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ []))) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ [])))],extension(6,bind([[_8875, _8931, _8986], [difference(3 ^ [], difference(union(4 ^ [], 5 ^ []), intersection(4 ^ [], 5 ^ []))), union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ []))), union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ [])))]]))).
% 14.72/14.95 cnf('1.1.1.2.1',plain,[-(difference(3 ^ [], difference(union(4 ^ [], 5 ^ []), intersection(4 ^ [], 5 ^ []))) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ []))))],extension(8,bind([[_13712, _13653, _13770], [union(4 ^ [], 5 ^ []), 3 ^ [], intersection(4 ^ [], 5 ^ [])]]))).
% 14.72/14.95 cnf('1.1.1.2.2',plain,[-(union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ []))) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ []))))],extension(4,bind([[_8443], [union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ [])))]]))).
% 14.72/14.95 cnf('1.1.2',plain,[-(union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ []))) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(intersection(3 ^ [], 4 ^ []), 5 ^ []))), difference(3 ^ [], union(4 ^ [], 5 ^ [])) = difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ [])) = intersection(intersection(3 ^ [], 4 ^ []), 5 ^ [])],extension(3,bind([[_12481, _12548, _12614, _12679], [difference(3 ^ [], union(4 ^ [], 5 ^ [])), difference(3 ^ [], union(4 ^ [], 5 ^ [])), intersection(3 ^ [], intersection(4 ^ [], 5 ^ [])), intersection(intersection(3 ^ [], 4 ^ []), 5 ^ [])]]))).
% 14.72/14.95 cnf('1.1.2.1',plain,[-(difference(3 ^ [], union(4 ^ [], 5 ^ [])) = difference(3 ^ [], union(4 ^ [], 5 ^ []))), 3 ^ [] = 3 ^ [], union(4 ^ [], 5 ^ []) = union(4 ^ [], 5 ^ [])],extension(2,bind([[_10619, _10686, _10752, _10817], [3 ^ [], 3 ^ [], union(4 ^ [], 5 ^ []), union(4 ^ [], 5 ^ [])]]))).
% 14.72/14.95 cnf('1.1.2.1.1',plain,[-(3 ^ [] = 3 ^ [])],extension(4,bind([[_8443], [3 ^ []]]))).
% 14.72/14.95 cnf('1.1.2.1.2',plain,[-(union(4 ^ [], 5 ^ []) = union(4 ^ [], 5 ^ []))],extension(4,bind([[_8443], [union(4 ^ [], 5 ^ [])]]))).
% 14.72/14.95 cnf('1.1.2.2',plain,[-(intersection(3 ^ [], intersection(4 ^ [], 5 ^ [])) = intersection(intersection(3 ^ [], 4 ^ []), 5 ^ [])), intersection(intersection(3 ^ [], 4 ^ []), 5 ^ []) = intersection(3 ^ [], intersection(4 ^ [], 5 ^ []))],extension(5,bind([[_8596, _8641], [intersection(intersection(3 ^ [], 4 ^ []), 5 ^ []), intersection(3 ^ [], intersection(4 ^ [], 5 ^ []))]]))).
% 14.72/14.95 cnf('1.1.2.2.1',plain,[-(intersection(intersection(3 ^ [], 4 ^ []), 5 ^ []) = intersection(3 ^ [], intersection(4 ^ [], 5 ^ [])))],extension(7,bind([[_13186, _13242, _13297], [3 ^ [], 4 ^ [], 5 ^ []]]))).
% 14.72/14.95 %-----------------------------------------------------
% 14.72/14.96
% 14.72/14.96 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------