%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU172+2 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n029.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:43 EDT 2022
% Result : Theorem 14.34s 14.84s
% Output : Proof 14.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SEU172+2 : TPTP v8.1.0. Released v3.3.0.
% 0.12/0.12 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n029.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 : Sun Jun 19 06:17:14 EDT 2022
% 0.13/0.33 % CPUTime :
% 14.34/14.84 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.34/14.85 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.34/14.85
% 14.34/14.85 %-----------------------------------------------------
% 14.34/14.85 fof(t54_subset_1, conjecture, ! [_136463, _136466, _136469] : (element(_136469, powerset(_136463)) => ~ (in(_136466, subset_complement(_136463, _136469)) & in(_136466, _136469))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t54_subset_1)).
% 14.34/14.85 fof(d2_subset_1, axiom, ! [_136740, _136743] : ((~ empty(_136740) => (element(_136743, _136740) <=> in(_136743, _136740))) & (empty(_136740) => (element(_136743, _136740) <=> empty(_136743)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_subset_1)).
% 14.34/14.85 fof(d4_xboole_0, axiom, ! [_137034, _137037, _137040] : (_137040 = set_difference(_137034, _137037) <=> ! [_137061] : (in(_137061, _137040) <=> in(_137061, _137034) & ~ in(_137061, _137037))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d4_xboole_0)).
% 14.34/14.85 fof(d5_subset_1, axiom, ! [_137300, _137303] : (element(_137303, powerset(_137300)) => subset_complement(_137300, _137303) = set_difference(_137300, _137303)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d5_subset_1)).
% 14.34/14.85 fof(t7_boole, axiom, ! [_137585, _137588] : ~ (in(_137585, _137588) & empty(_137588)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t7_boole)).
% 14.34/14.85
% 14.34/14.85 cnf(1, plain, [-(element(30 ^ [], powerset(28 ^ [])))], clausify(t54_subset_1)).
% 14.34/14.85 cnf(2, plain, [-(in(29 ^ [], subset_complement(28 ^ [], 30 ^ [])))], clausify(t54_subset_1)).
% 14.34/14.85 cnf(3, plain, [-(in(29 ^ [], 30 ^ []))], clausify(t54_subset_1)).
% 14.34/14.85 cnf(4, plain, [-(empty(_58316)), element(_58384, _58316), -(in(_58384, _58316))], clausify(d2_subset_1)).
% 14.34/14.85 cnf(5, plain, [-(empty(_58316)), -(element(_58384, _58316)), in(_58384, _58316)], clausify(d2_subset_1)).
% 14.34/14.85 cnf(6, plain, [_63255 = set_difference(_63112, _63184), in(_63421, _63255), in(_63421, _63184)], clausify(d4_xboole_0)).
% 14.34/14.85 cnf(7, plain, [element(_63874, powerset(_63821)), -(subset_complement(_63821, _63874) = set_difference(_63821, _63874))], clausify(d5_subset_1)).
% 14.34/14.85 cnf(8, plain, [in(_94016, _94062), empty(_94062)], clausify(t7_boole)).
% 14.34/14.85
% 14.34/14.85 cnf('1',plain,[in(29 ^ [], subset_complement(28 ^ [], 30 ^ [])), empty(subset_complement(28 ^ [], 30 ^ []))],start(8,bind([[_94016, _94062], [29 ^ [], subset_complement(28 ^ [], 30 ^ [])]]))).
% 14.34/14.85 cnf('1.1',plain,[-(in(29 ^ [], subset_complement(28 ^ [], 30 ^ [])))],extension(2)).
% 14.34/14.85 cnf('1.2',plain,[-(empty(subset_complement(28 ^ [], 30 ^ []))), element(29 ^ [], subset_complement(28 ^ [], 30 ^ [])), -(in(29 ^ [], subset_complement(28 ^ [], 30 ^ [])))],extension(4,bind([[_58384, _58316], [29 ^ [], subset_complement(28 ^ [], 30 ^ [])]]))).
% 14.34/14.85 cnf('1.2.1',plain,[-(element(29 ^ [], subset_complement(28 ^ [], 30 ^ []))), -(empty(subset_complement(28 ^ [], 30 ^ []))), in(29 ^ [], subset_complement(28 ^ [], 30 ^ []))],extension(5,bind([[_58384, _58316], [29 ^ [], subset_complement(28 ^ [], 30 ^ [])]]))).
% 14.34/14.85 cnf('1.2.1.1',plain,[empty(subset_complement(28 ^ [], 30 ^ []))],reduction('1')).
% 14.34/14.85 cnf('1.2.1.2',plain,[-(in(29 ^ [], subset_complement(28 ^ [], 30 ^ [])))],extension(2)).
% 14.34/14.85 cnf('1.2.2',plain,[in(29 ^ [], subset_complement(28 ^ [], 30 ^ [])), subset_complement(28 ^ [], 30 ^ []) = set_difference(28 ^ [], 30 ^ []), in(29 ^ [], 30 ^ [])],extension(6,bind([[_63255, _63112, _63421, _63184], [subset_complement(28 ^ [], 30 ^ []), 28 ^ [], 29 ^ [], 30 ^ []]]))).
% 14.34/14.85 cnf('1.2.2.1',plain,[-(subset_complement(28 ^ [], 30 ^ []) = set_difference(28 ^ [], 30 ^ [])), element(30 ^ [], powerset(28 ^ []))],extension(7,bind([[_63874, _63821], [30 ^ [], 28 ^ []]]))).
% 14.34/14.85 cnf('1.2.2.1.1',plain,[-(element(30 ^ [], powerset(28 ^ [])))],extension(1)).
% 14.34/14.85 cnf('1.2.2.2',plain,[-(in(29 ^ [], 30 ^ []))],extension(3)).
% 14.34/14.85 %-----------------------------------------------------
% 14.34/14.85
% 14.34/14.86 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------