%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET636+3 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n009.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:55:02 EDT 2022
% Result : Theorem 0.65s 1.40s
% Output : Proof 0.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET636+3 : TPTP v8.1.0. Released v2.2.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n009.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Mon Jul 11 04:10:22 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.65/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.65/1.41 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.65/1.42
% 0.65/1.42 %-----------------------------------------------------
% 0.65/1.42 fof(prove_th118, conjecture, ! [_30420, _30423] : (disjoint(_30420, _30423) <=> intersection(_30420, _30423) = empty_set), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_th118)).
% 0.65/1.42 fof(intersection_defn, axiom, ! [_30653, _30656, _30659] : (member(_30659, intersection(_30653, _30656)) <=> member(_30659, _30653) & member(_30659, _30656)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', intersection_defn)).
% 0.65/1.42 fof(intersect_defn, axiom, ! [_30878, _30881] : (intersect(_30878, _30881) <=> ? [_30899] : (member(_30899, _30878) & member(_30899, _30881))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', intersect_defn)).
% 0.65/1.42 fof(empty_set_defn, axiom, ! [_31106] : ~ member(_31106, empty_set), file('/export/starexec/sandbox/benchmark/theBenchmark.p', empty_set_defn)).
% 0.65/1.42 fof(disjoint_defn, axiom, ! [_31220, _31223] : (disjoint(_31220, _31223) <=> ~ intersect(_31220, _31223)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', disjoint_defn)).
% 0.65/1.42 fof(equal_member_defn, axiom, ! [_31396, _31399] : (_31396 = _31399 <=> ! [_31413] : (member(_31413, _31396) <=> member(_31413, _31399))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', equal_member_defn)).
% 0.65/1.42
% 0.65/1.42 cnf(1, plain, [-(8 ^ []), disjoint(5 ^ [], 6 ^ [])], clausify(prove_th118)).
% 0.65/1.42 cnf(2, plain, [-(8 ^ []), -(intersection(5 ^ [], 6 ^ []) = empty_set)], clausify(prove_th118)).
% 0.65/1.42 cnf(3, plain, [-(7 ^ []), intersection(5 ^ [], 6 ^ []) = empty_set], clausify(prove_th118)).
% 0.65/1.42 cnf(4, plain, [-(7 ^ []), -(disjoint(5 ^ [], 6 ^ []))], clausify(prove_th118)).
% 0.65/1.42 cnf(5, plain, [7 ^ [], 8 ^ []], clausify(prove_th118)).
% 0.65/1.42 cnf(6, plain, [-(_6831 = _6831)], theory(equality)).
% 0.65/1.42 cnf(7, plain, [-(member(_9383, _9514)), member(_9316, _9449), _9316 = _9383, _9449 = _9514], theory(equality)).
% 0.65/1.42 cnf(8, plain, [member(_11396, intersection(_11279, _11338)), -(member(_11396, _11279))], clausify(intersection_defn)).
% 0.65/1.42 cnf(9, plain, [member(_11396, intersection(_11279, _11338)), -(member(_11396, _11338))], clausify(intersection_defn)).
% 0.65/1.42 cnf(10, plain, [-(member(_11396, intersection(_11279, _11338))), member(_11396, _11279), member(_11396, _11338)], clausify(intersection_defn)).
% 0.65/1.42 cnf(11, plain, [intersect(_11792, _11848), -(member(1 ^ [_11848, _11792], _11792))], clausify(intersect_defn)).
% 0.65/1.42 cnf(12, plain, [intersect(_11792, _11848), -(member(1 ^ [_11848, _11792], _11848))], clausify(intersect_defn)).
% 0.65/1.42 cnf(13, plain, [-(intersect(_11792, _11848)), member(_11963, _11792), member(_11963, _11848)], clausify(intersect_defn)).
% 0.65/1.42 cnf(14, plain, [member(_12254, empty_set)], clausify(empty_set_defn)).
% 0.65/1.42 cnf(15, plain, [disjoint(_12446, _12493), intersect(_12446, _12493)], clausify(disjoint_defn)).
% 0.65/1.42 cnf(16, plain, [-(disjoint(_12446, _12493)), -(intersect(_12446, _12493))], clausify(disjoint_defn)).
% 0.65/1.42 cnf(17, plain, [_14719 = _14775, member(_14889, _14719), -(member(_14889, _14775))], clausify(equal_member_defn)).
% 0.65/1.42 cnf(18, plain, [-(_14719 = _14775), -(member(4 ^ [_14775, _14719], _14719)), -(member(4 ^ [_14775, _14719], _14775))], clausify(equal_member_defn)).
% 0.65/1.42
% 0.65/1.42 cnf('1',plain,[7 ^ [], 8 ^ []],start(5)).
% 0.65/1.42 cnf('1.1',plain,[-(7 ^ []), intersection(5 ^ [], 6 ^ []) = empty_set],extension(3)).
% 0.65/1.42 cnf('1.1.1',plain,[-(intersection(5 ^ [], 6 ^ []) = empty_set), -(member(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], intersection(5 ^ [], 6 ^ []))), -(member(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], empty_set))],extension(18,bind([[_14719, _14775], [intersection(5 ^ [], 6 ^ []), empty_set]]))).
% 0.65/1.42 cnf('1.1.1.1',plain,[member(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], intersection(5 ^ [], 6 ^ [])), -(member(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], 5 ^ []))],extension(8,bind([[_11338, _11396, _11279], [6 ^ [], 4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], 5 ^ []]]))).
% 0.65/1.42 cnf('1.1.1.1.1',plain,[member(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], 5 ^ []), -(intersect(5 ^ [], 6 ^ [])), member(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], 6 ^ [])],extension(13,bind([[_11792, _11963, _11848], [5 ^ [], 4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], 6 ^ []]]))).
% 0.65/1.42 cnf('1.1.1.1.1.1',plain,[intersect(5 ^ [], 6 ^ []), disjoint(5 ^ [], 6 ^ [])],extension(15,bind([[_12446, _12493], [5 ^ [], 6 ^ []]]))).
% 0.65/1.42 cnf('1.1.1.1.1.1.1',plain,[-(disjoint(5 ^ [], 6 ^ [])), -(7 ^ [])],extension(4)).
% 0.65/1.42 cnf('1.1.1.1.1.1.1.1',plain,[7 ^ []],reduction('1')).
% 0.65/1.42 cnf('1.1.1.1.1.2',plain,[-(member(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], 6 ^ [])), member(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], intersection(5 ^ [], 6 ^ []))],extension(9,bind([[_11396, _11279, _11338], [4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], 5 ^ [], 6 ^ []]]))).
% 0.65/1.42 cnf('1.1.1.1.1.2.1',plain,[-(member(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], intersection(5 ^ [], 6 ^ [])))],reduction('1.1.1')).
% 0.65/1.42 cnf('1.1.1.2',plain,[member(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], empty_set), -(member(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], empty_set)), 4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])] = 4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], empty_set = empty_set],extension(7,bind([[_9316, _9383, _9449, _9514], [4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], 4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], empty_set, empty_set]]))).
% 0.65/1.42 cnf('1.1.1.2.1',plain,[member(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], empty_set), -(member(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], empty_set)), 4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])] = 4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], empty_set = empty_set],extension(7,bind([[_9316, _9383, _9449, _9514], [4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], 4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], empty_set, empty_set]]))).
% 0.65/1.42 cnf('1.1.1.2.1.1',plain,[member(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])], empty_set)],extension(14,bind([[_12254], [4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])]]]))).
% 0.65/1.42 cnf('1.1.1.2.1.2',plain,[-(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])] = 4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])])],extension(6,bind([[_6831], [4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])]]]))).
% 0.65/1.42 cnf('1.1.1.2.1.3',plain,[-(empty_set = empty_set)],extension(6,bind([[_6831], [empty_set]]))).
% 0.65/1.42 cnf('1.1.1.2.2',plain,[-(4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])] = 4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])])],extension(6,bind([[_6831], [4 ^ [empty_set, intersection(5 ^ [], 6 ^ [])]]]))).
% 0.65/1.42 cnf('1.1.1.2.3',plain,[-(empty_set = empty_set)],extension(6,bind([[_6831], [empty_set]]))).
% 0.65/1.42 cnf('1.2',plain,[-(8 ^ []), -(intersection(5 ^ [], 6 ^ []) = empty_set)],extension(2)).
% 0.65/1.42 cnf('1.2.1',plain,[intersection(5 ^ [], 6 ^ []) = empty_set, member(1 ^ [6 ^ [], 5 ^ []], intersection(5 ^ [], 6 ^ [])), -(member(1 ^ [6 ^ [], 5 ^ []], empty_set))],extension(17,bind([[_14719, _14889, _14775], [intersection(5 ^ [], 6 ^ []), 1 ^ [6 ^ [], 5 ^ []], empty_set]]))).
% 0.65/1.42 cnf('1.2.1.1',plain,[-(member(1 ^ [6 ^ [], 5 ^ []], intersection(5 ^ [], 6 ^ []))), member(1 ^ [6 ^ [], 5 ^ []], 5 ^ []), member(1 ^ [6 ^ [], 5 ^ []], 6 ^ [])],extension(10,bind([[_11279, _11396, _11338], [5 ^ [], 1 ^ [6 ^ [], 5 ^ []], 6 ^ []]]))).
% 0.65/1.42 cnf('1.2.1.1.1',plain,[-(member(1 ^ [6 ^ [], 5 ^ []], 5 ^ [])), intersect(5 ^ [], 6 ^ [])],extension(11,bind([[_11792, _11848], [5 ^ [], 6 ^ []]]))).
% 0.65/1.42 cnf('1.2.1.1.1.1',plain,[-(intersect(5 ^ [], 6 ^ [])), -(disjoint(5 ^ [], 6 ^ []))],extension(16,bind([[_12446, _12493], [5 ^ [], 6 ^ []]]))).
% 0.65/1.42 cnf('1.2.1.1.1.1.1',plain,[disjoint(5 ^ [], 6 ^ []), -(8 ^ [])],extension(1)).
% 0.65/1.42 cnf('1.2.1.1.1.1.1.1',plain,[8 ^ []],reduction('1')).
% 0.65/1.42 cnf('1.2.1.1.2',plain,[-(member(1 ^ [6 ^ [], 5 ^ []], 6 ^ [])), intersect(5 ^ [], 6 ^ [])],extension(12,bind([[_11792, _11848], [5 ^ [], 6 ^ []]]))).
% 0.65/1.42 cnf('1.2.1.1.2.1',plain,[-(intersect(5 ^ [], 6 ^ [])), -(disjoint(5 ^ [], 6 ^ []))],extension(16,bind([[_12446, _12493], [5 ^ [], 6 ^ []]]))).
% 0.65/1.42 cnf('1.2.1.1.2.1.1',plain,[disjoint(5 ^ [], 6 ^ []), -(8 ^ [])],extension(1)).
% 0.65/1.42 cnf('1.2.1.1.2.1.1.1',plain,[8 ^ []],reduction('1')).
% 0.65/1.42 cnf('1.2.1.2',plain,[member(1 ^ [6 ^ [], 5 ^ []], empty_set), -(member(1 ^ [6 ^ [], 5 ^ []], intersection(empty_set, empty_set))), member(1 ^ [6 ^ [], 5 ^ []], empty_set)],extension(10,bind([[_11279, _11396, _11338], [empty_set, 1 ^ [6 ^ [], 5 ^ []], empty_set]]))).
% 0.65/1.42 cnf('1.2.1.2.1',plain,[member(1 ^ [6 ^ [], 5 ^ []], intersection(empty_set, empty_set)), -(member(1 ^ [6 ^ [], 5 ^ []], empty_set))],extension(8,bind([[_11338, _11396, _11279], [empty_set, 1 ^ [6 ^ [], 5 ^ []], empty_set]]))).
% 0.65/1.42 cnf('1.2.1.2.1.1',plain,[member(1 ^ [6 ^ [], 5 ^ []], empty_set)],extension(14,bind([[_12254], [1 ^ [6 ^ [], 5 ^ []]]]))).
% 0.65/1.42 cnf('1.2.1.2.2',plain,[-(member(1 ^ [6 ^ [], 5 ^ []], empty_set))],reduction('1.2.1')).
% 0.65/1.42 %-----------------------------------------------------
% 0.65/1.42
% 0.65/1.42 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------