%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET617+3 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n014.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:48 EDT 2022
% Result : Theorem 27.21s 27.37s
% Output : Proof 27.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SET617+3 : TPTP v8.1.0. Released v2.2.0.
% 0.03/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n014.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Sun Jul 10 07:59:20 EDT 2022
% 0.13/0.35 % CPUTime :
% 27.21/27.37 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.21/27.37 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.21/27.38
% 27.21/27.38 %-----------------------------------------------------
% 27.21/27.38 fof(prove_th92, conjecture, ! [_29478] : (symmetric_difference(_29478, empty_set) = _29478 & symmetric_difference(empty_set, _29478) = _29478), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_th92)).
% 27.21/27.38 fof(symmetric_difference_defn, axiom, ! [_29637, _29640] : symmetric_difference(_29637, _29640) = union(difference(_29637, _29640), difference(_29640, _29637)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', symmetric_difference_defn)).
% 27.21/27.38 fof(union_empty_set, axiom, ! [_29815] : union(_29815, empty_set) = _29815, file('/export/starexec/sandbox/benchmark/theBenchmark.p', union_empty_set)).
% 27.21/27.38 fof(no_difference_with_empty_set1, axiom, ! [_29934] : difference(_29934, empty_set) = _29934, file('/export/starexec/sandbox/benchmark/theBenchmark.p', no_difference_with_empty_set1)).
% 27.21/27.38 fof(no_difference_with_empty_set2, axiom, ! [_30053] : difference(empty_set, _30053) = empty_set, file('/export/starexec/sandbox/benchmark/theBenchmark.p', no_difference_with_empty_set2)).
% 27.21/27.38 fof(equal_defn, axiom, ! [_30173, _30176] : (_30173 = _30176 <=> subset(_30173, _30176) & subset(_30176, _30173)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', equal_defn)).
% 27.21/27.38 fof(commutativity_of_symmetric_difference, axiom, ! [_30357, _30360] : symmetric_difference(_30357, _30360) = symmetric_difference(_30360, _30357), file('/export/starexec/sandbox/benchmark/theBenchmark.p', commutativity_of_symmetric_difference)).
% 27.21/27.38 fof(reflexivity_of_subset, axiom, ! [_30503] : subset(_30503, _30503), file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity_of_subset)).
% 27.21/27.38 fof(subset_defn, axiom, ! [_30614, _30617] : (subset(_30614, _30617) <=> ! [_30635] : (member(_30635, _30614) => member(_30635, _30617))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', subset_defn)).
% 27.21/27.38 fof(equal_member_defn, axiom, ! [_30818, _30821] : (_30818 = _30821 <=> ! [_30835] : (member(_30835, _30818) <=> member(_30835, _30821))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', equal_member_defn)).
% 27.21/27.38
% 27.21/27.38 cnf(1, plain, [symmetric_difference(4 ^ [], empty_set) = 4 ^ [], symmetric_difference(empty_set, 4 ^ []) = 4 ^ []], clausify(prove_th92)).
% 27.21/27.38 cnf(2, plain, [-(symmetric_difference(_11036, _11087) = union(difference(_11036, _11087), difference(_11087, _11036)))], clausify(symmetric_difference_defn)).
% 27.21/27.38 cnf(3, plain, [-(union(_11432, empty_set) = _11432)], clausify(union_empty_set)).
% 27.21/27.38 cnf(4, plain, [-(difference(_11646, empty_set) = _11646)], clausify(no_difference_with_empty_set1)).
% 27.21/27.38 cnf(5, plain, [-(difference(empty_set, _11860) = empty_set)], clausify(no_difference_with_empty_set2)).
% 27.21/27.38 cnf(6, plain, [_12266 = _12317, -(subset(_12266, _12317))], clausify(equal_defn)).
% 27.21/27.38 cnf(7, plain, [-(_12266 = _12317), subset(_12266, _12317), subset(_12317, _12266)], clausify(equal_defn)).
% 27.21/27.38 cnf(8, plain, [-(symmetric_difference(_12972, _13017) = symmetric_difference(_13017, _12972))], clausify(commutativity_of_symmetric_difference)).
% 27.21/27.38 cnf(9, plain, [-(subset(_14204, _14204))], clausify(reflexivity_of_subset)).
% 27.21/27.38 cnf(10, plain, [subset(_13743, _13799), member(_13913, _13743), -(member(_13913, _13799))], clausify(subset_defn)).
% 27.21/27.38 cnf(11, plain, [_13282 = _13338, member(_13452, _13282), -(member(_13452, _13338))], clausify(equal_member_defn)).
% 27.21/27.38 cnf(12, plain, [-(_13282 = _13338), member(1 ^ [_13338, _13282], _13282), member(1 ^ [_13338, _13282], _13338)], clausify(equal_member_defn)).
% 27.21/27.38 cnf(13, plain, [-(_13282 = _13338), -(member(1 ^ [_13338, _13282], _13282)), -(member(1 ^ [_13338, _13282], _13338))], clausify(equal_member_defn)).
% 27.21/27.38 cnf(14, plain, [-(union(_10346, _10479) = union(_10413, _10544)), _10346 = _10413, _10479 = _10544], theory(equality)).
% 27.21/27.38 cnf(15, plain, [-(_6588 = _6588)], theory(equality)).
% 27.21/27.38 cnf(16, plain, [_6741 = _6786, -(_6786 = _6741)], theory(equality)).
% 27.21/27.38 cnf(17, plain, [-(_7020 = _7131), _7020 = _7076, _7076 = _7131], theory(equality)).
% 27.21/27.38 cnf(18, plain, [-(member(_7892, _8023)), member(_7825, _7958), _7825 = _7892, _7958 = _8023], theory(equality)).
% 27.21/27.38
% 27.21/27.38 cnf('1',plain,[symmetric_difference(4 ^ [], empty_set) = 4 ^ [], symmetric_difference(empty_set, 4 ^ []) = 4 ^ []],start(1)).
% 27.21/27.38 cnf('1.1',plain,[-(symmetric_difference(4 ^ [], empty_set) = 4 ^ []), symmetric_difference(4 ^ [], empty_set) = union(difference(4 ^ [], empty_set), difference(empty_set, 4 ^ [])), union(difference(4 ^ [], empty_set), difference(empty_set, 4 ^ [])) = 4 ^ []],extension(17,bind([[_7020, _7076, _7131], [symmetric_difference(4 ^ [], empty_set), union(difference(4 ^ [], empty_set), difference(empty_set, 4 ^ [])), 4 ^ []]]))).
% 27.21/27.38 cnf('1.1.1',plain,[-(symmetric_difference(4 ^ [], empty_set) = union(difference(4 ^ [], empty_set), difference(empty_set, 4 ^ [])))],extension(2,bind([[_11087, _11036], [empty_set, 4 ^ []]]))).
% 27.21/27.38 cnf('1.1.2',plain,[-(union(difference(4 ^ [], empty_set), difference(empty_set, 4 ^ [])) = 4 ^ []), union(difference(4 ^ [], empty_set), difference(empty_set, 4 ^ [])) = union(4 ^ [], empty_set), union(4 ^ [], empty_set) = 4 ^ []],extension(17,bind([[_7020, _7076, _7131], [union(difference(4 ^ [], empty_set), difference(empty_set, 4 ^ [])), union(4 ^ [], empty_set), 4 ^ []]]))).
% 27.21/27.38 cnf('1.1.2.1',plain,[-(union(difference(4 ^ [], empty_set), difference(empty_set, 4 ^ [])) = union(4 ^ [], empty_set)), difference(4 ^ [], empty_set) = 4 ^ [], difference(empty_set, 4 ^ []) = empty_set],extension(14,bind([[_10346, _10413, _10479, _10544], [difference(4 ^ [], empty_set), 4 ^ [], difference(empty_set, 4 ^ []), empty_set]]))).
% 27.21/27.38 cnf('1.1.2.1.1',plain,[-(difference(4 ^ [], empty_set) = 4 ^ [])],extension(4,bind([[_11646], [4 ^ []]]))).
% 27.21/27.38 cnf('1.1.2.1.2',plain,[-(difference(empty_set, 4 ^ []) = empty_set)],extension(5,bind([[_11860], [4 ^ []]]))).
% 27.21/27.38 cnf('1.1.2.2',plain,[-(union(4 ^ [], empty_set) = 4 ^ [])],extension(3,bind([[_11432], [4 ^ []]]))).
% 27.21/27.38 cnf('1.2',plain,[-(symmetric_difference(empty_set, 4 ^ []) = 4 ^ []), member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], symmetric_difference(empty_set, 4 ^ [])), member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 4 ^ [])],extension(12,bind([[_13282, _13338], [symmetric_difference(empty_set, 4 ^ []), 4 ^ []]]))).
% 27.21/27.38 cnf('1.2.1',plain,[-(member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], symmetric_difference(empty_set, 4 ^ []))), subset(symmetric_difference(4 ^ [], empty_set), symmetric_difference(empty_set, 4 ^ [])), member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], symmetric_difference(4 ^ [], empty_set))],extension(10,bind([[_13799, _13913, _13743], [symmetric_difference(empty_set, 4 ^ []), 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], symmetric_difference(4 ^ [], empty_set)]]))).
% 27.21/27.38 cnf('1.2.1.1',plain,[-(subset(symmetric_difference(4 ^ [], empty_set), symmetric_difference(empty_set, 4 ^ []))), symmetric_difference(4 ^ [], empty_set) = symmetric_difference(empty_set, 4 ^ [])],extension(6,bind([[_12266, _12317], [symmetric_difference(4 ^ [], empty_set), symmetric_difference(empty_set, 4 ^ [])]]))).
% 27.21/27.38 cnf('1.2.1.1.1',plain,[-(symmetric_difference(4 ^ [], empty_set) = symmetric_difference(empty_set, 4 ^ []))],extension(8,bind([[_13017, _12972], [empty_set, 4 ^ []]]))).
% 27.21/27.38 cnf('1.2.1.2',plain,[-(member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], symmetric_difference(4 ^ [], empty_set))), member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 4 ^ []), 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])] = 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 4 ^ [] = symmetric_difference(4 ^ [], empty_set)],extension(18,bind([[_7825, _7892, _7958, _8023], [1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 4 ^ [], symmetric_difference(4 ^ [], empty_set)]]))).
% 27.21/27.38 cnf('1.2.1.2.1',plain,[-(member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 4 ^ [])), -(symmetric_difference(empty_set, 4 ^ []) = 4 ^ []), -(member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], symmetric_difference(empty_set, 4 ^ [])))],extension(13,bind([[_13338, _13282], [4 ^ [], symmetric_difference(empty_set, 4 ^ [])]]))).
% 27.21/27.38 cnf('1.2.1.2.1.1',plain,[symmetric_difference(empty_set, 4 ^ []) = 4 ^ []],reduction('1')).
% 27.21/27.38 cnf('1.2.1.2.1.2',plain,[member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], symmetric_difference(empty_set, 4 ^ []))],reduction('1.2')).
% 27.21/27.38 cnf('1.2.1.2.2',plain,[-(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])] = 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])])],extension(15,bind([[_6588], [1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])]]]))).
% 27.21/27.38 cnf('1.2.1.2.3',plain,[-(4 ^ [] = symmetric_difference(4 ^ [], empty_set)), symmetric_difference(4 ^ [], empty_set) = 4 ^ []],extension(16,bind([[_6741, _6786], [symmetric_difference(4 ^ [], empty_set), 4 ^ []]]))).
% 27.21/27.38 cnf('1.2.1.2.3.1',plain,[-(symmetric_difference(4 ^ [], empty_set) = 4 ^ [])],lemmata('1')).
% 27.21/27.38 cnf('1.2.2',plain,[-(member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 4 ^ [])), member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], symmetric_difference(4 ^ [], empty_set)), 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])] = 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], symmetric_difference(4 ^ [], empty_set) = 4 ^ []],extension(18,bind([[_7825, _7892, _7958, _8023], [1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], symmetric_difference(4 ^ [], empty_set), 4 ^ []]]))).
% 27.21/27.38 cnf('1.2.2.1',plain,[-(member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], symmetric_difference(4 ^ [], empty_set))), symmetric_difference(empty_set, 4 ^ []) = symmetric_difference(4 ^ [], empty_set), member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], symmetric_difference(empty_set, 4 ^ []))],extension(11,bind([[_13338, _13452, _13282], [symmetric_difference(4 ^ [], empty_set), 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], symmetric_difference(empty_set, 4 ^ [])]]))).
% 27.21/27.38 cnf('1.2.2.1.1',plain,[-(symmetric_difference(empty_set, 4 ^ []) = symmetric_difference(4 ^ [], empty_set))],extension(8,bind([[_13017, _12972], [4 ^ [], empty_set]]))).
% 27.21/27.38 cnf('1.2.2.1.2',plain,[-(member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], symmetric_difference(empty_set, 4 ^ []))), -(symmetric_difference(empty_set, 4 ^ []) = 4 ^ []), -(member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 4 ^ []))],extension(13,bind([[_13282, _13338], [symmetric_difference(empty_set, 4 ^ []), 4 ^ []]]))).
% 27.21/27.38 cnf('1.2.2.1.2.1',plain,[symmetric_difference(empty_set, 4 ^ []) = 4 ^ []],reduction('1')).
% 27.21/27.38 cnf('1.2.2.1.2.2',plain,[member(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 4 ^ [])],reduction('1.2')).
% 27.21/27.38 cnf('1.2.2.2',plain,[-(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])] = 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])]), subset(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])]), subset(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])])],extension(7,bind([[_12317, _12266], [1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])]]]))).
% 27.21/27.38 cnf('1.2.2.2.1',plain,[-(subset(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])]))],extension(9,bind([[_14204], [1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])]]]))).
% 27.21/27.38 cnf('1.2.2.2.2',plain,[-(subset(1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])], 1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])]))],extension(9,bind([[_14204], [1 ^ [4 ^ [], symmetric_difference(empty_set, 4 ^ [])]]]))).
% 27.21/27.38 cnf('1.2.2.3',plain,[-(symmetric_difference(4 ^ [], empty_set) = 4 ^ [])],lemmata('1')).
% 27.21/27.38 %-----------------------------------------------------
% 27.21/27.38
% 27.21/27.39 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------