%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET679+3 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n018.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:20 EDT 2022
% Result : Theorem 217.76s 210.46s
% Output : Proof 217.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET679+3 : TPTP v8.1.0. Released v2.2.0.
% 0.13/0.13 % Command : leancop_casc.sh %s %d
% 0.14/0.34 % Computer : n018.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Sun Jul 10 16:15:27 EDT 2022
% 0.20/0.34 % CPUTime :
% 217.76/210.46 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 217.76/210.47 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 217.76/210.47
% 217.76/210.47 %-----------------------------------------------------
% 217.76/210.47 fof(prove_relset_1_46, conjecture, ! [_56978] : (~ empty(_56978) & ilf_type(_56978, set_type) => not_equal(identity_relation_of(_56978), empty_set)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_relset_1_46)).
% 217.76/210.47 fof(p6, axiom, ! [_57150] : (ilf_type(_57150, set_type) => ! [_57168] : (ilf_type(_57168, set_type) => (_57150 = _57168 <=> ! [_57192] : (ilf_type(_57192, set_type) => (member(_57192, _57150) <=> member(_57192, _57168)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p6)).
% 217.76/210.47 fof(p22, axiom, ! [_57457] : ilf_type(_57457, set_type), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p22)).
% 217.76/210.47 fof(p2, axiom, ! [_57574] : (ilf_type(_57574, set_type) => ~ member(_57574, empty_set)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p2)).
% 217.76/210.47 fof(p4, axiom, ! [_57723] : (ilf_type(_57723, set_type) => ! [_57741] : (ilf_type(_57741, set_type) => ! [_57759] : (ilf_type(_57759, set_type) => (member(ordered_pair(_57741, _57759), identity_relation_of(_57723)) <=> member(_57741, _57723) & _57741 = _57759)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p4)).
% 217.76/210.47 fof(p7, axiom, ! [_58056] : (ilf_type(_58056, set_type) => ! [_58074] : (ilf_type(_58074, set_type) => (not_equal(_58056, _58074) <=> (! _58056) = _58074))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p7)).
% 217.76/210.47 fof(p8, axiom, ! [_58293] : (ilf_type(_58293, set_type) => (empty(_58293) <=> ! [_58318] : (ilf_type(_58318, set_type) => ~ member(_58318, _58293)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', p8)).
% 217.76/210.47
% 217.76/210.47 cnf(1, plain, [not_equal(identity_relation_of(10 ^ []), empty_set)], clausify(prove_relset_1_46)).
% 217.76/210.47 cnf(2, plain, [ilf_type(_22392, set_type), ilf_type(_22525, set_type), _22392 = _22525, ilf_type(_22710, set_type), member(_22710, _22392), -(member(_22710, _22525))], clausify(p6)).
% 217.76/210.47 cnf(3, plain, [-(ilf_type(_30221, set_type))], clausify(p22)).
% 217.76/210.47 cnf(4, plain, [ilf_type(_20810, set_type), member(_20810, empty_set)], clausify(p2)).
% 217.76/210.47 cnf(5, plain, [ilf_type(_21327, set_type), ilf_type(_21465, set_type), ilf_type(_21596, set_type), -(member(ordered_pair(_21465, _21596), identity_relation_of(_21327))), member(_21465, _21327), _21465 = _21596], clausify(p4)).
% 217.76/210.47 cnf(6, plain, [ilf_type(_23111, set_type), ilf_type(_23229, set_type), -(not_equal(_23111, _23229)), -(_23111 = _23229)], clausify(p7)).
% 217.76/210.47 cnf(7, plain, [empty(10 ^ [])], clausify(prove_relset_1_46)).
% 217.76/210.47 cnf(8, plain, [ilf_type(_23607, set_type), -(empty(_23607)), -(member(2 ^ [_23607], _23607))], clausify(p8)).
% 217.76/210.47 cnf(9, plain, [-(_13464 = _13464)], theory(equality)).
% 217.76/210.47
% 217.76/210.47 cnf('1',plain,[not_equal(identity_relation_of(10 ^ []), empty_set)],start(1)).
% 217.76/210.47 cnf('1.1',plain,[-(not_equal(identity_relation_of(10 ^ []), empty_set)), ilf_type(identity_relation_of(10 ^ []), set_type), ilf_type(empty_set, set_type), -(identity_relation_of(10 ^ []) = empty_set)],extension(6,bind([[_23111, _23229], [identity_relation_of(10 ^ []), empty_set]]))).
% 217.76/210.47 cnf('1.1.1',plain,[-(ilf_type(identity_relation_of(10 ^ []), set_type))],extension(3,bind([[_30221], [identity_relation_of(10 ^ [])]]))).
% 217.76/210.47 cnf('1.1.2',plain,[-(ilf_type(empty_set, set_type))],extension(3,bind([[_30221], [empty_set]]))).
% 217.76/210.47 cnf('1.1.3',plain,[identity_relation_of(10 ^ []) = empty_set, ilf_type(identity_relation_of(10 ^ []), set_type), ilf_type(empty_set, set_type), ilf_type(ordered_pair(2 ^ [10 ^ []], 2 ^ [10 ^ []]), set_type), member(ordered_pair(2 ^ [10 ^ []], 2 ^ [10 ^ []]), identity_relation_of(10 ^ [])), -(member(ordered_pair(2 ^ [10 ^ []], 2 ^ [10 ^ []]), empty_set))],extension(2,bind([[_22392, _22710, _22525], [identity_relation_of(10 ^ []), ordered_pair(2 ^ [10 ^ []], 2 ^ [10 ^ []]), empty_set]]))).
% 217.76/210.47 cnf('1.1.3.1',plain,[-(ilf_type(identity_relation_of(10 ^ []), set_type))],extension(3,bind([[_30221], [identity_relation_of(10 ^ [])]]))).
% 217.76/210.47 cnf('1.1.3.2',plain,[-(ilf_type(empty_set, set_type))],extension(3,bind([[_30221], [empty_set]]))).
% 217.76/210.47 cnf('1.1.3.3',plain,[-(ilf_type(ordered_pair(2 ^ [10 ^ []], 2 ^ [10 ^ []]), set_type))],extension(3,bind([[_30221], [ordered_pair(2 ^ [10 ^ []], 2 ^ [10 ^ []])]]))).
% 217.76/210.47 cnf('1.1.3.4',plain,[-(member(ordered_pair(2 ^ [10 ^ []], 2 ^ [10 ^ []]), identity_relation_of(10 ^ []))), ilf_type(10 ^ [], set_type), ilf_type(2 ^ [10 ^ []], set_type), ilf_type(2 ^ [10 ^ []], set_type), member(2 ^ [10 ^ []], 10 ^ []), 2 ^ [10 ^ []] = 2 ^ [10 ^ []]],extension(5,bind([[_21327, _21465, _21596], [10 ^ [], 2 ^ [10 ^ []], 2 ^ [10 ^ []]]]))).
% 217.76/210.47 cnf('1.1.3.4.1',plain,[-(ilf_type(10 ^ [], set_type))],extension(3,bind([[_30221], [10 ^ []]]))).
% 217.76/210.47 cnf('1.1.3.4.2',plain,[-(ilf_type(2 ^ [10 ^ []], set_type))],extension(3,bind([[_30221], [2 ^ [10 ^ []]]]))).
% 217.76/210.47 cnf('1.1.3.4.3',plain,[-(ilf_type(2 ^ [10 ^ []], set_type))],extension(3,bind([[_30221], [2 ^ [10 ^ []]]]))).
% 217.76/210.47 cnf('1.1.3.4.4',plain,[-(member(2 ^ [10 ^ []], 10 ^ [])), ilf_type(10 ^ [], set_type), -(empty(10 ^ []))],extension(8,bind([[_23607], [10 ^ []]]))).
% 217.76/210.47 cnf('1.1.3.4.4.1',plain,[-(ilf_type(10 ^ [], set_type))],extension(3,bind([[_30221], [10 ^ []]]))).
% 217.76/210.47 cnf('1.1.3.4.4.2',plain,[empty(10 ^ [])],extension(7)).
% 217.76/210.47 cnf('1.1.3.4.5',plain,[-(2 ^ [10 ^ []] = 2 ^ [10 ^ []])],extension(9,bind([[_13464], [2 ^ [10 ^ []]]]))).
% 217.76/210.47 cnf('1.1.3.5',plain,[member(ordered_pair(2 ^ [10 ^ []], 2 ^ [10 ^ []]), empty_set), ilf_type(ordered_pair(2 ^ [10 ^ []], 2 ^ [10 ^ []]), set_type)],extension(4,bind([[_20810], [ordered_pair(2 ^ [10 ^ []], 2 ^ [10 ^ []])]]))).
% 217.76/210.47 cnf('1.1.3.5.1',plain,[-(ilf_type(ordered_pair(2 ^ [10 ^ []], 2 ^ [10 ^ []]), set_type))],extension(3,bind([[_30221], [ordered_pair(2 ^ [10 ^ []], 2 ^ [10 ^ []])]]))).
% 217.76/210.47 %-----------------------------------------------------
% 217.76/210.48
% 217.76/210.48 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------