%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU169+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n016.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 12:00:42 EDT 2022
% Result : Theorem 0.34s 1.43s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SEU169+1 : TPTP v8.1.0. Released v3.3.0.
% 0.08/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.35 % Computer : n016.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 : Sat Jun 18 22:58:53 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.34/1.43 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/1.43 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/1.44
% 0.34/1.44 %-----------------------------------------------------
% 0.34/1.44 fof(l3_subset_1, conjecture, ! [_23821, _23824] : (element(_23824, powerset(_23821)) => ! [_23846] : (in(_23846, _23824) => in(_23846, _23821))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', l3_subset_1)).
% 0.34/1.44 fof(d1_zfmisc_1, axiom, ! [_24076, _24079] : (_24079 = powerset(_24076) <=> ! [_24097] : (in(_24097, _24079) <=> subset(_24097, _24076))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_zfmisc_1)).
% 0.34/1.44 fof(d2_subset_1, axiom, ! [_24288, _24291] : ((~ empty(_24288) => (element(_24291, _24288) <=> in(_24291, _24288))) & (empty(_24288) => (element(_24291, _24288) <=> empty(_24291)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d2_subset_1)).
% 0.34/1.44 fof(d3_tarski, axiom, ! [_24537, _24540] : (subset(_24537, _24540) <=> ! [_24558] : (in(_24558, _24537) => in(_24558, _24540))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d3_tarski)).
% 0.34/1.44 fof(fc1_subset_1, axiom, ! [_24742] : ~ empty(powerset(_24742)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fc1_subset_1)).
% 0.34/1.44
% 0.34/1.44 cnf(1, plain, [-(element(8 ^ [], powerset(7 ^ [])))], clausify(l3_subset_1)).
% 0.34/1.44 cnf(2, plain, [-(in(9 ^ [], 8 ^ []))], clausify(l3_subset_1)).
% 0.34/1.44 cnf(3, plain, [in(9 ^ [], 7 ^ [])], clausify(l3_subset_1)).
% 0.34/1.44 cnf(4, plain, [-(_7681 = _7681)], theory(equality)).
% 0.34/1.44 cnf(5, plain, [_11583 = powerset(_11525), in(_11715, _11583), -(subset(_11715, _11525))], clausify(d1_zfmisc_1)).
% 0.34/1.44 cnf(6, plain, [-(empty(_12006)), element(_12074, _12006), -(in(_12074, _12006))], clausify(d2_subset_1)).
% 0.34/1.44 cnf(7, plain, [subset(_12611, _12667), in(_12781, _12611), -(in(_12781, _12667))], clausify(d3_tarski)).
% 0.34/1.44 cnf(8, plain, [empty(powerset(_13696))], clausify(fc1_subset_1)).
% 0.34/1.44
% 0.34/1.44 cnf('1',plain,[empty(powerset(7 ^ []))],start(8,bind([[_13696], [7 ^ []]]))).
% 0.34/1.44 cnf('1.1',plain,[-(empty(powerset(7 ^ []))), element(8 ^ [], powerset(7 ^ [])), -(in(8 ^ [], powerset(7 ^ [])))],extension(6,bind([[_12074, _12006], [8 ^ [], powerset(7 ^ [])]]))).
% 0.34/1.44 cnf('1.1.1',plain,[-(element(8 ^ [], powerset(7 ^ [])))],extension(1)).
% 0.34/1.44 cnf('1.1.2',plain,[in(8 ^ [], powerset(7 ^ [])), powerset(7 ^ []) = powerset(7 ^ []), -(subset(8 ^ [], 7 ^ []))],extension(5,bind([[_11583, _11715, _11525], [powerset(7 ^ []), 8 ^ [], 7 ^ []]]))).
% 0.34/1.44 cnf('1.1.2.1',plain,[-(powerset(7 ^ []) = powerset(7 ^ []))],extension(4,bind([[_7681], [powerset(7 ^ [])]]))).
% 0.34/1.44 cnf('1.1.2.2',plain,[subset(8 ^ [], 7 ^ []), in(9 ^ [], 8 ^ []), -(in(9 ^ [], 7 ^ []))],extension(7,bind([[_12611, _12781, _12667], [8 ^ [], 9 ^ [], 7 ^ []]]))).
% 0.34/1.44 cnf('1.1.2.2.1',plain,[-(in(9 ^ [], 8 ^ []))],extension(2)).
% 0.34/1.44 cnf('1.1.2.2.2',plain,[in(9 ^ [], 7 ^ [])],extension(3)).
% 0.34/1.44 %-----------------------------------------------------
% 0.34/1.44
% 0.34/1.45 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------