%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUM388+1 : TPTP v8.1.0. Released v3.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 : Mon Jul 18 11:40:28 EDT 2022
% Result : Theorem 0.33s 1.40s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : NUM388+1 : TPTP v8.1.0. Released v3.2.0.
% 0.12/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n009.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Thu Jul 7 10:29:22 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.33/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.40 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.41
% 0.33/1.41 %-----------------------------------------------------
% 0.33/1.41 fof(t19_ordinal1, conjecture, ! [_42189] : (ordinal(_42189) => ! [_42204] : (ordinal(_42204) => ! [_42219] : (epsilon_transitive(_42219) => in(_42219, _42189) & in(_42189, _42204) => in(_42219, _42204)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t19_ordinal1)).
% 0.33/1.41 fof(cc1_ordinal1, axiom, ! [_42511] : (ordinal(_42511) => epsilon_transitive(_42511) & epsilon_connected(_42511)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', cc1_ordinal1)).
% 0.33/1.41 fof(d2_ordinal1, axiom, ! [_42659] : (epsilon_transitive(_42659) <=> ! [_42674] : (in(_42674, _42659) => subset(_42674, _42659))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d2_ordinal1)).
% 0.33/1.41 fof(t2_subset, axiom, ! [_42879, _42882] : (element(_42879, _42882) => empty(_42882) | in(_42879, _42882)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t2_subset)).
% 0.33/1.41 fof(t3_subset, axiom, ! [_43047, _43050] : (element(_43047, powerset(_43050)) <=> subset(_43047, _43050)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t3_subset)).
% 0.33/1.41 fof(t4_subset, axiom, ! [_43202, _43205, _43208] : (in(_43202, _43205) & element(_43205, powerset(_43208)) => element(_43202, _43208)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t4_subset)).
% 0.33/1.41 fof(t5_subset, axiom, ! [_43396, _43399, _43402] : ~ (in(_43396, _43399) & element(_43399, powerset(_43402)) & empty(_43402)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t5_subset)).
% 0.33/1.41
% 0.33/1.41 cnf(1, plain, [-(ordinal(15 ^ []))], clausify(t19_ordinal1)).
% 0.33/1.41 cnf(2, plain, [-(in(16 ^ [], 14 ^ []))], clausify(t19_ordinal1)).
% 0.33/1.41 cnf(3, plain, [-(in(14 ^ [], 15 ^ []))], clausify(t19_ordinal1)).
% 0.33/1.41 cnf(4, plain, [in(16 ^ [], 15 ^ [])], clausify(t19_ordinal1)).
% 0.33/1.41 cnf(5, plain, [ordinal(_19650), -(epsilon_transitive(_19650))], clausify(cc1_ordinal1)).
% 0.33/1.41 cnf(6, plain, [epsilon_transitive(_20838), in(_20926, _20838), -(subset(_20926, _20838))], clausify(d2_ordinal1)).
% 0.33/1.41 cnf(7, plain, [element(_24991, _25041), -(empty(_25041)), -(in(_24991, _25041))], clausify(t2_subset)).
% 0.33/1.41 cnf(8, plain, [-(element(_25364, powerset(_25411))), subset(_25364, _25411)], clausify(t3_subset)).
% 0.33/1.41 cnf(9, plain, [-(element(_25694, _25809)), in(_25694, _25752), element(_25752, powerset(_25809))], clausify(t4_subset)).
% 0.33/1.41 cnf(10, plain, [in(_26183, _26242), element(_26242, powerset(_26300)), empty(_26300)], clausify(t5_subset)).
% 0.33/1.41
% 0.33/1.41 cnf('1',plain,[in(16 ^ [], 15 ^ [])],start(4)).
% 0.33/1.41 cnf('1.1',plain,[-(in(16 ^ [], 15 ^ [])), element(16 ^ [], 15 ^ []), -(empty(15 ^ []))],extension(7,bind([[_24991, _25041], [16 ^ [], 15 ^ []]]))).
% 0.33/1.41 cnf('1.1.1',plain,[-(element(16 ^ [], 15 ^ [])), in(16 ^ [], 14 ^ []), element(14 ^ [], powerset(15 ^ []))],extension(9,bind([[_25694, _25752, _25809], [16 ^ [], 14 ^ [], 15 ^ []]]))).
% 0.33/1.41 cnf('1.1.1.1',plain,[-(in(16 ^ [], 14 ^ []))],extension(2)).
% 0.33/1.41 cnf('1.1.1.2',plain,[-(element(14 ^ [], powerset(15 ^ []))), subset(14 ^ [], 15 ^ [])],extension(8,bind([[_25364, _25411], [14 ^ [], 15 ^ []]]))).
% 0.33/1.41 cnf('1.1.1.2.1',plain,[-(subset(14 ^ [], 15 ^ [])), epsilon_transitive(15 ^ []), in(14 ^ [], 15 ^ [])],extension(6,bind([[_20926, _20838], [14 ^ [], 15 ^ []]]))).
% 0.33/1.41 cnf('1.1.1.2.1.1',plain,[-(epsilon_transitive(15 ^ [])), ordinal(15 ^ [])],extension(5,bind([[_19650], [15 ^ []]]))).
% 0.33/1.41 cnf('1.1.1.2.1.1.1',plain,[-(ordinal(15 ^ []))],extension(1)).
% 0.33/1.41 cnf('1.1.1.2.1.2',plain,[-(in(14 ^ [], 15 ^ []))],extension(3)).
% 0.33/1.41 cnf('1.1.2',plain,[empty(15 ^ []), in(16 ^ [], 14 ^ []), element(14 ^ [], powerset(15 ^ []))],extension(10,bind([[_26183, _26242, _26300], [16 ^ [], 14 ^ [], 15 ^ []]]))).
% 0.33/1.41 cnf('1.1.2.1',plain,[-(in(16 ^ [], 14 ^ []))],extension(2)).
% 0.33/1.41 cnf('1.1.2.2',plain,[-(element(14 ^ [], powerset(15 ^ []))), subset(14 ^ [], 15 ^ [])],extension(8,bind([[_25364, _25411], [14 ^ [], 15 ^ []]]))).
% 0.33/1.41 cnf('1.1.2.2.1',plain,[-(subset(14 ^ [], 15 ^ [])), epsilon_transitive(15 ^ []), in(14 ^ [], 15 ^ [])],extension(6,bind([[_20926, _20838], [14 ^ [], 15 ^ []]]))).
% 0.33/1.41 cnf('1.1.2.2.1.1',plain,[-(epsilon_transitive(15 ^ [])), ordinal(15 ^ [])],extension(5,bind([[_19650], [15 ^ []]]))).
% 0.33/1.41 cnf('1.1.2.2.1.1.1',plain,[-(ordinal(15 ^ []))],extension(1)).
% 0.33/1.41 cnf('1.1.2.2.1.2',plain,[-(in(14 ^ [], 15 ^ []))],extension(3)).
% 0.33/1.41 %-----------------------------------------------------
% 0.33/1.42
% 0.33/1.42 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------