%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU308+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n013.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:01:53 EDT 2022
% Result : Theorem 36.02s 35.51s
% Output : Proof 36.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU308+1 : TPTP v8.1.0. Released v3.3.0.
% 0.06/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n013.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 : Sun Jun 19 01:31:59 EDT 2022
% 0.12/0.33 % CPUTime :
% 36.02/35.51 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 36.02/35.52 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 36.02/35.52
% 36.02/35.52 %-----------------------------------------------------
% 36.02/35.52 fof(t17_pre_topc, conjecture, ! [_78211] : (one_sorted_str(_78211) => ! [_78226] : (element(_78226, powerset(the_carrier(_78211))) => subset_complement(the_carrier(_78211), _78226) = subset_difference(the_carrier(_78211), cast_as_carrier_subset(_78211), _78226))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t17_pre_topc)).
% 36.02/35.52 fof(t4_subset, axiom, ! [_78624, _78627, _78630] : (in(_78624, _78627) & element(_78627, powerset(_78630)) => element(_78624, _78630)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t4_subset)).
% 36.02/35.52 fof(reflexivity_r1_tarski, axiom, ! [_78819, _78822] : subset(_78819, _78819), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity_r1_tarski)).
% 36.02/35.52 fof(t2_subset, axiom, ! [_78941, _78944] : (element(_78941, _78944) => empty(_78944) | in(_78941, _78944)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t2_subset)).
% 36.02/35.52 fof(redefinition_k6_subset_1, axiom, ! [_79114, _79117, _79120] : (element(_79117, powerset(_79114)) & element(_79120, powerset(_79114)) => subset_difference(_79114, _79117, _79120) = set_difference(_79117, _79120)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', redefinition_k6_subset_1)).
% 36.02/35.52 fof(fc1_subset_1, axiom, ! [_79355] : ~ empty(powerset(_79355)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc1_subset_1)).
% 36.02/35.52 fof(t3_subset, axiom, ! [_79472, _79475] : (element(_79472, powerset(_79475)) <=> subset(_79472, _79475)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t3_subset)).
% 36.02/35.52 fof(d3_pre_topc, axiom, ! [_79627] : (one_sorted_str(_79627) => cast_as_carrier_subset(_79627) = the_carrier(_79627)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d3_pre_topc)).
% 36.02/35.52 fof(d5_subset_1, axiom, ! [_79769, _79772] : (element(_79772, powerset(_79769)) => subset_complement(_79769, _79772) = set_difference(_79769, _79772)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d5_subset_1)).
% 36.02/35.52
% 36.02/35.52 cnf(1, plain, [-(one_sorted_str(20 ^ []))], clausify(t17_pre_topc)).
% 36.02/35.52 cnf(2, plain, [-(element(21 ^ [], powerset(the_carrier(20 ^ []))))], clausify(t17_pre_topc)).
% 36.02/35.52 cnf(3, plain, [subset_complement(the_carrier(20 ^ []), 21 ^ []) = subset_difference(the_carrier(20 ^ []), cast_as_carrier_subset(20 ^ []), 21 ^ [])], clausify(t17_pre_topc)).
% 36.02/35.52 cnf(4, plain, [_33237 = _33286, -(the_carrier(_33237) = the_carrier(_33286))], theory(equality)).
% 36.02/35.52 cnf(5, plain, [-(subset_difference(_32222, _32391, _32556) = subset_difference(_32307, _32474, _32637)), _32222 = _32307, _32391 = _32474, _32556 = _32637], theory(equality)).
% 36.02/35.52 cnf(6, plain, [-(_23373 = _23373)], theory(equality)).
% 36.02/35.52 cnf(7, plain, [_23526 = _23571, -(_23571 = _23526)], theory(equality)).
% 36.02/35.52 cnf(8, plain, [-(_23805 = _23916), _23805 = _23861, _23861 = _23916], theory(equality)).
% 36.02/35.52 cnf(9, plain, [-(subset(_26583, _26714)), subset(_26516, _26649), _26516 = _26583, _26649 = _26714], theory(equality)).
% 36.02/35.52 cnf(10, plain, [-(element(_43961, _44076)), in(_43961, _44019), element(_44019, powerset(_44076))], clausify(t4_subset)).
% 36.02/35.52 cnf(11, plain, [-(subset(_44937, _44937))], clausify(reflexivity_r1_tarski)).
% 36.02/35.52 cnf(12, plain, [element(_46315, _46365), -(empty(_46365)), -(in(_46315, _46365))], clausify(t2_subset)).
% 36.02/35.52 cnf(13, plain, [-(subset_difference(_48411, _48478, _48544) = set_difference(_48478, _48544)), element(_48478, powerset(_48411)), element(_48544, powerset(_48411))], clausify(redefinition_k6_subset_1)).
% 36.02/35.52 cnf(14, plain, [empty(powerset(_51023))], clausify(fc1_subset_1)).
% 36.02/35.52 cnf(15, plain, [-(element(_51211, powerset(_51258))), subset(_51211, _51258)], clausify(t3_subset)).
% 36.02/35.52 cnf(16, plain, [one_sorted_str(_51541), -(cast_as_carrier_subset(_51541) = the_carrier(_51541))], clausify(d3_pre_topc)).
% 36.02/35.52 cnf(17, plain, [element(_51852, powerset(_51799)), -(subset_complement(_51799, _51852) = set_difference(_51799, _51852))], clausify(d5_subset_1)).
% 36.02/35.52
% 36.02/35.52 cnf('1',plain,[-(element(21 ^ [], powerset(the_carrier(20 ^ []))))],start(2)).
% 36.02/35.52 cnf('1.1',plain,[element(21 ^ [], powerset(the_carrier(20 ^ []))), -(subset_difference(the_carrier(20 ^ []), the_carrier(20 ^ []), 21 ^ []) = set_difference(the_carrier(20 ^ []), 21 ^ [])), element(the_carrier(20 ^ []), powerset(the_carrier(20 ^ [])))],extension(13,bind([[_48544, _48478, _48411], [21 ^ [], the_carrier(20 ^ []), the_carrier(20 ^ [])]]))).
% 36.02/35.52 cnf('1.1.1',plain,[subset_difference(the_carrier(20 ^ []), the_carrier(20 ^ []), 21 ^ []) = set_difference(the_carrier(20 ^ []), 21 ^ []), -(subset_difference(the_carrier(20 ^ []), cast_as_carrier_subset(20 ^ []), 21 ^ []) = set_difference(the_carrier(20 ^ []), 21 ^ [])), subset_difference(the_carrier(20 ^ []), cast_as_carrier_subset(20 ^ []), 21 ^ []) = subset_difference(the_carrier(20 ^ []), the_carrier(20 ^ []), 21 ^ [])],extension(8,bind([[_23916, _23805, _23861], [set_difference(the_carrier(20 ^ []), 21 ^ []), subset_difference(the_carrier(20 ^ []), cast_as_carrier_subset(20 ^ []), 21 ^ []), subset_difference(the_carrier(20 ^ []), the_carrier(20 ^ []), 21 ^ [])]]))).
% 36.02/35.52 cnf('1.1.1.1',plain,[subset_difference(the_carrier(20 ^ []), cast_as_carrier_subset(20 ^ []), 21 ^ []) = set_difference(the_carrier(20 ^ []), 21 ^ []), -(set_difference(the_carrier(20 ^ []), 21 ^ []) = subset_difference(the_carrier(20 ^ []), cast_as_carrier_subset(20 ^ []), 21 ^ []))],extension(7,bind([[_23571, _23526], [set_difference(the_carrier(20 ^ []), 21 ^ []), subset_difference(the_carrier(20 ^ []), cast_as_carrier_subset(20 ^ []), 21 ^ [])]]))).
% 36.02/35.52 cnf('1.1.1.1.1',plain,[set_difference(the_carrier(20 ^ []), 21 ^ []) = subset_difference(the_carrier(20 ^ []), cast_as_carrier_subset(20 ^ []), 21 ^ []), -(subset_complement(the_carrier(20 ^ []), 21 ^ []) = subset_difference(the_carrier(20 ^ []), cast_as_carrier_subset(20 ^ []), 21 ^ [])), subset_complement(the_carrier(20 ^ []), 21 ^ []) = set_difference(the_carrier(20 ^ []), 21 ^ [])],extension(8,bind([[_23916, _23805, _23861], [subset_difference(the_carrier(20 ^ []), cast_as_carrier_subset(20 ^ []), 21 ^ []), subset_complement(the_carrier(20 ^ []), 21 ^ []), set_difference(the_carrier(20 ^ []), 21 ^ [])]]))).
% 36.02/35.52 cnf('1.1.1.1.1.1',plain,[subset_complement(the_carrier(20 ^ []), 21 ^ []) = subset_difference(the_carrier(20 ^ []), cast_as_carrier_subset(20 ^ []), 21 ^ [])],extension(3)).
% 36.02/35.52 cnf('1.1.1.1.1.2',plain,[-(subset_complement(the_carrier(20 ^ []), 21 ^ []) = set_difference(the_carrier(20 ^ []), 21 ^ [])), element(21 ^ [], powerset(the_carrier(20 ^ [])))],extension(17,bind([[_51852, _51799], [21 ^ [], the_carrier(20 ^ [])]]))).
% 36.02/35.52 cnf('1.1.1.1.1.2.1',plain,[-(element(21 ^ [], powerset(the_carrier(20 ^ []))))],extension(2)).
% 36.02/35.52 cnf('1.1.1.2',plain,[-(subset_difference(the_carrier(20 ^ []), cast_as_carrier_subset(20 ^ []), 21 ^ []) = subset_difference(the_carrier(20 ^ []), the_carrier(20 ^ []), 21 ^ [])), the_carrier(20 ^ []) = the_carrier(20 ^ []), cast_as_carrier_subset(20 ^ []) = the_carrier(20 ^ []), 21 ^ [] = 21 ^ []],extension(5,bind([[_32222, _32307, _32391, _32474, _32556, _32637], [the_carrier(20 ^ []), the_carrier(20 ^ []), cast_as_carrier_subset(20 ^ []), the_carrier(20 ^ []), 21 ^ [], 21 ^ []]]))).
% 36.02/35.52 cnf('1.1.1.2.1',plain,[-(the_carrier(20 ^ []) = the_carrier(20 ^ [])), 20 ^ [] = 20 ^ []],extension(4,bind([[_33237, _33286], [20 ^ [], 20 ^ []]]))).
% 36.02/35.52 cnf('1.1.1.2.1.1',plain,[-(20 ^ [] = 20 ^ [])],extension(6,bind([[_23373], [20 ^ []]]))).
% 36.02/35.52 cnf('1.1.1.2.2',plain,[-(cast_as_carrier_subset(20 ^ []) = the_carrier(20 ^ [])), one_sorted_str(20 ^ [])],extension(16,bind([[_51541], [20 ^ []]]))).
% 36.02/35.52 cnf('1.1.1.2.2.1',plain,[-(one_sorted_str(20 ^ []))],extension(1)).
% 36.02/35.52 cnf('1.1.1.2.3',plain,[-(21 ^ [] = 21 ^ [])],extension(6,bind([[_23373], [21 ^ []]]))).
% 36.02/35.52 cnf('1.1.2',plain,[-(element(the_carrier(20 ^ []), powerset(the_carrier(20 ^ [])))), in(the_carrier(20 ^ []), powerset(the_carrier(20 ^ []))), element(powerset(the_carrier(20 ^ [])), powerset(powerset(the_carrier(20 ^ []))))],extension(10,bind([[_43961, _44019, _44076], [the_carrier(20 ^ []), powerset(the_carrier(20 ^ [])), powerset(the_carrier(20 ^ []))]]))).
% 36.02/35.52 cnf('1.1.2.1',plain,[-(in(the_carrier(20 ^ []), powerset(the_carrier(20 ^ [])))), element(the_carrier(20 ^ []), powerset(the_carrier(20 ^ []))), -(empty(powerset(the_carrier(20 ^ []))))],extension(12,bind([[_46315, _46365], [the_carrier(20 ^ []), powerset(the_carrier(20 ^ []))]]))).
% 36.02/35.52 cnf('1.1.2.1.1',plain,[-(element(the_carrier(20 ^ []), powerset(the_carrier(20 ^ [])))), subset(the_carrier(20 ^ []), the_carrier(20 ^ []))],extension(15,bind([[_51211, _51258], [the_carrier(20 ^ []), the_carrier(20 ^ [])]]))).
% 36.02/35.52 cnf('1.1.2.1.1.1',plain,[-(subset(the_carrier(20 ^ []), the_carrier(20 ^ [])))],extension(11,bind([[_44937], [the_carrier(20 ^ [])]]))).
% 36.02/35.52 cnf('1.1.2.1.2',plain,[empty(powerset(the_carrier(20 ^ [])))],extension(14,bind([[_51023], [the_carrier(20 ^ [])]]))).
% 36.02/35.52 cnf('1.1.2.2',plain,[-(element(powerset(the_carrier(20 ^ [])), powerset(powerset(the_carrier(20 ^ []))))), subset(powerset(the_carrier(20 ^ [])), powerset(the_carrier(20 ^ [])))],extension(15,bind([[_51211, _51258], [powerset(the_carrier(20 ^ [])), powerset(the_carrier(20 ^ []))]]))).
% 36.02/35.52 cnf('1.1.2.2.1',plain,[-(subset(powerset(the_carrier(20 ^ [])), powerset(the_carrier(20 ^ [])))), subset(powerset(the_carrier(20 ^ [])), powerset(the_carrier(20 ^ []))), powerset(the_carrier(20 ^ [])) = powerset(the_carrier(20 ^ [])), powerset(the_carrier(20 ^ [])) = powerset(the_carrier(20 ^ []))],extension(9,bind([[_26516, _26583, _26649, _26714], [powerset(the_carrier(20 ^ [])), powerset(the_carrier(20 ^ [])), powerset(the_carrier(20 ^ [])), powerset(the_carrier(20 ^ []))]]))).
% 36.02/35.52 cnf('1.1.2.2.1.1',plain,[-(subset(powerset(the_carrier(20 ^ [])), powerset(the_carrier(20 ^ []))))],extension(11,bind([[_44937], [powerset(the_carrier(20 ^ []))]]))).
% 36.02/35.52 cnf('1.1.2.2.1.2',plain,[-(powerset(the_carrier(20 ^ [])) = powerset(the_carrier(20 ^ [])))],extension(6,bind([[_23373], [powerset(the_carrier(20 ^ []))]]))).
% 36.02/35.52 cnf('1.1.2.2.1.3',plain,[-(powerset(the_carrier(20 ^ [])) = powerset(the_carrier(20 ^ [])))],extension(6,bind([[_23373], [powerset(the_carrier(20 ^ []))]]))).
% 36.02/35.52 %-----------------------------------------------------
% 36.02/35.53
% 36.02/35.53 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------