%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU101+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n004.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:08 EDT 2022
% Result : Theorem 2.60s 3.45s
% Output : Proof 2.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU101+1 : TPTP v8.1.0. Released v3.2.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n004.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 22:42:53 EDT 2022
% 0.12/0.33 % CPUTime :
% 2.60/3.45 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.60/3.46 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.60/3.46
% 2.60/3.46 %-----------------------------------------------------
% 2.60/3.46 fof(t10_finsub_1, conjecture, ! [_61614] : (preboolean(_61614) <=> ! [_61629, _61632] : (in(_61629, _61614) & in(_61632, _61614) => in(set_union2(_61629, _61632), _61614) & in(set_difference(_61629, _61632), _61614))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t10_finsub_1)).
% 2.60/3.46 fof(cc1_finsub_1, axiom, ! [_62011] : (preboolean(_62011) => cup_closed(_62011) & diff_closed(_62011)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', cc1_finsub_1)).
% 2.60/3.46 fof(cc2_finsub_1, axiom, ! [_62166] : (cup_closed(_62166) & diff_closed(_62166) => preboolean(_62166)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', cc2_finsub_1)).
% 2.60/3.46 fof(d1_finsub_1, axiom, ! [_62309] : (cup_closed(_62309) <=> ! [_62324, _62327] : (in(_62324, _62309) & in(_62327, _62309) => in(set_union2(_62324, _62327), _62309))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_finsub_1)).
% 2.60/3.46 fof(d3_finsub_1, axiom, ! [_62586] : (diff_closed(_62586) <=> ! [_62601, _62604] : (in(_62601, _62586) & in(_62604, _62586) => in(set_difference(_62601, _62604), _62586))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d3_finsub_1)).
% 2.60/3.46
% 2.60/3.46 cnf(1, plain, [-(19 ^ [_47014, _47009]), -(in(set_difference(_47009, _47014), 15 ^ []))], clausify(t10_finsub_1)).
% 2.60/3.46 cnf(2, plain, [-(19 ^ [_47014, _47009]), -(in(set_union2(_47009, _47014), 15 ^ []))], clausify(t10_finsub_1)).
% 2.60/3.46 cnf(3, plain, [-(20 ^ []), 19 ^ [_47014, _47009], in(_47009, 15 ^ []), in(_47014, 15 ^ [])], clausify(t10_finsub_1)).
% 2.60/3.46 cnf(4, plain, [-(20 ^ []), preboolean(15 ^ [])], clausify(t10_finsub_1)).
% 2.60/3.46 cnf(5, plain, [-(18 ^ []), in(set_union2(16 ^ [], 17 ^ []), 15 ^ []), in(set_difference(16 ^ [], 17 ^ []), 15 ^ [])], clausify(t10_finsub_1)).
% 2.60/3.46 cnf(6, plain, [-(18 ^ []), -(in(17 ^ [], 15 ^ []))], clausify(t10_finsub_1)).
% 2.60/3.46 cnf(7, plain, [-(18 ^ []), -(in(16 ^ [], 15 ^ []))], clausify(t10_finsub_1)).
% 2.60/3.46 cnf(8, plain, [-(18 ^ []), -(preboolean(15 ^ []))], clausify(t10_finsub_1)).
% 2.60/3.46 cnf(9, plain, [18 ^ [], 20 ^ []], clausify(t10_finsub_1)).
% 2.60/3.46 cnf(10, plain, [preboolean(_26622), -(cup_closed(_26622))], clausify(cc1_finsub_1)).
% 2.60/3.46 cnf(11, plain, [preboolean(_26622), -(diff_closed(_26622))], clausify(cc1_finsub_1)).
% 2.60/3.46 cnf(12, plain, [-(preboolean(_27255)), cup_closed(_27255), diff_closed(_27255)], clausify(cc2_finsub_1)).
% 2.60/3.46 cnf(13, plain, [-(cup_closed(_27833)), -(in(1 ^ [_27833], _27833))], clausify(d1_finsub_1)).
% 2.60/3.46 cnf(14, plain, [-(cup_closed(_27833)), -(in(2 ^ [_27833], _27833))], clausify(d1_finsub_1)).
% 2.60/3.46 cnf(15, plain, [-(cup_closed(_27833)), in(set_union2(1 ^ [_27833], 2 ^ [_27833]), _27833)], clausify(d1_finsub_1)).
% 2.60/3.46 cnf(16, plain, [cup_closed(_27833), -(in(set_union2(_27935, _27993), _27833)), in(_27935, _27833), in(_27993, _27833)], clausify(d1_finsub_1)).
% 2.60/3.46 cnf(17, plain, [-(diff_closed(_28404)), -(in(3 ^ [_28404], _28404))], clausify(d3_finsub_1)).
% 2.60/3.46 cnf(18, plain, [-(diff_closed(_28404)), -(in(4 ^ [_28404], _28404))], clausify(d3_finsub_1)).
% 2.60/3.46 cnf(19, plain, [-(diff_closed(_28404)), in(set_difference(3 ^ [_28404], 4 ^ [_28404]), _28404)], clausify(d3_finsub_1)).
% 2.60/3.46 cnf(20, plain, [diff_closed(_28404), -(in(set_difference(_28506, _28564), _28404)), in(_28506, _28404), in(_28564, _28404)], clausify(d3_finsub_1)).
% 2.60/3.46
% 2.60/3.46 cnf('1',plain,[18 ^ [], 20 ^ []],start(9)).
% 2.60/3.46 cnf('1.1',plain,[-(18 ^ []), in(set_union2(16 ^ [], 17 ^ []), 15 ^ []), in(set_difference(16 ^ [], 17 ^ []), 15 ^ [])],extension(5)).
% 2.60/3.46 cnf('1.1.1',plain,[-(in(set_union2(16 ^ [], 17 ^ []), 15 ^ [])), cup_closed(15 ^ []), in(16 ^ [], 15 ^ []), in(17 ^ [], 15 ^ [])],extension(16,bind([[_27935, _27993, _27833], [16 ^ [], 17 ^ [], 15 ^ []]]))).
% 2.60/3.46 cnf('1.1.1.1',plain,[-(cup_closed(15 ^ [])), preboolean(15 ^ [])],extension(10,bind([[_26622], [15 ^ []]]))).
% 2.60/3.46 cnf('1.1.1.1.1',plain,[-(preboolean(15 ^ [])), -(18 ^ [])],extension(8)).
% 2.60/3.46 cnf('1.1.1.1.1.1',plain,[18 ^ []],reduction('1')).
% 2.60/3.46 cnf('1.1.1.2',plain,[-(in(16 ^ [], 15 ^ [])), -(18 ^ [])],extension(7)).
% 2.60/3.46 cnf('1.1.1.2.1',plain,[18 ^ []],reduction('1')).
% 2.60/3.46 cnf('1.1.1.3',plain,[-(in(17 ^ [], 15 ^ [])), -(18 ^ [])],extension(6)).
% 2.60/3.46 cnf('1.1.1.3.1',plain,[18 ^ []],reduction('1')).
% 2.60/3.46 cnf('1.1.2',plain,[-(in(set_difference(16 ^ [], 17 ^ []), 15 ^ [])), diff_closed(15 ^ []), in(16 ^ [], 15 ^ []), in(17 ^ [], 15 ^ [])],extension(20,bind([[_28506, _28564, _28404], [16 ^ [], 17 ^ [], 15 ^ []]]))).
% 2.60/3.46 cnf('1.1.2.1',plain,[-(diff_closed(15 ^ [])), preboolean(15 ^ [])],extension(11,bind([[_26622], [15 ^ []]]))).
% 2.60/3.46 cnf('1.1.2.1.1',plain,[-(preboolean(15 ^ [])), -(18 ^ [])],extension(8)).
% 2.60/3.46 cnf('1.1.2.1.1.1',plain,[18 ^ []],reduction('1')).
% 2.60/3.46 cnf('1.1.2.2',plain,[-(in(16 ^ [], 15 ^ [])), -(18 ^ [])],extension(7)).
% 2.60/3.46 cnf('1.1.2.2.1',plain,[18 ^ []],reduction('1')).
% 2.60/3.46 cnf('1.1.2.3',plain,[-(in(17 ^ [], 15 ^ [])), -(18 ^ [])],extension(6)).
% 2.60/3.46 cnf('1.1.2.3.1',plain,[18 ^ []],reduction('1')).
% 2.60/3.46 cnf('1.2',plain,[-(20 ^ []), preboolean(15 ^ [])],extension(4)).
% 2.60/3.46 cnf('1.2.1',plain,[-(preboolean(15 ^ [])), cup_closed(15 ^ []), diff_closed(15 ^ [])],extension(12,bind([[_27255], [15 ^ []]]))).
% 2.60/3.46 cnf('1.2.1.1',plain,[-(cup_closed(15 ^ [])), -(in(1 ^ [15 ^ []], 15 ^ []))],extension(13,bind([[_27833], [15 ^ []]]))).
% 2.60/3.46 cnf('1.2.1.1.1',plain,[in(1 ^ [15 ^ []], 15 ^ []), -(20 ^ []), 19 ^ [2 ^ [15 ^ []], 1 ^ [15 ^ []]], in(2 ^ [15 ^ []], 15 ^ [])],extension(3,bind([[_47009, _47014], [1 ^ [15 ^ []], 2 ^ [15 ^ []]]]))).
% 2.60/3.46 cnf('1.2.1.1.1.1',plain,[20 ^ []],reduction('1')).
% 2.60/3.46 cnf('1.2.1.1.1.2',plain,[-(19 ^ [2 ^ [15 ^ []], 1 ^ [15 ^ []]]), -(in(set_union2(1 ^ [15 ^ []], 2 ^ [15 ^ []]), 15 ^ []))],extension(2,bind([[_47009, _47014], [1 ^ [15 ^ []], 2 ^ [15 ^ []]]]))).
% 2.60/3.46 cnf('1.2.1.1.1.2.1',plain,[in(set_union2(1 ^ [15 ^ []], 2 ^ [15 ^ []]), 15 ^ []), -(cup_closed(15 ^ []))],extension(15,bind([[_27833], [15 ^ []]]))).
% 2.60/3.46 cnf('1.2.1.1.1.2.1.1',plain,[cup_closed(15 ^ [])],reduction('1.2.1')).
% 2.60/3.46 cnf('1.2.1.1.1.3',plain,[-(in(2 ^ [15 ^ []], 15 ^ [])), -(cup_closed(15 ^ []))],extension(14,bind([[_27833], [15 ^ []]]))).
% 2.60/3.46 cnf('1.2.1.1.1.3.1',plain,[cup_closed(15 ^ [])],reduction('1.2.1')).
% 2.60/3.46 cnf('1.2.1.2',plain,[-(diff_closed(15 ^ [])), -(in(3 ^ [15 ^ []], 15 ^ []))],extension(17,bind([[_28404], [15 ^ []]]))).
% 2.60/3.46 cnf('1.2.1.2.1',plain,[in(3 ^ [15 ^ []], 15 ^ []), -(20 ^ []), 19 ^ [4 ^ [15 ^ []], 3 ^ [15 ^ []]], in(4 ^ [15 ^ []], 15 ^ [])],extension(3,bind([[_47009, _47014], [3 ^ [15 ^ []], 4 ^ [15 ^ []]]]))).
% 2.60/3.46 cnf('1.2.1.2.1.1',plain,[20 ^ []],reduction('1')).
% 2.60/3.46 cnf('1.2.1.2.1.2',plain,[-(19 ^ [4 ^ [15 ^ []], 3 ^ [15 ^ []]]), -(in(set_difference(3 ^ [15 ^ []], 4 ^ [15 ^ []]), 15 ^ []))],extension(1,bind([[_47009, _47014], [3 ^ [15 ^ []], 4 ^ [15 ^ []]]]))).
% 2.60/3.46 cnf('1.2.1.2.1.2.1',plain,[in(set_difference(3 ^ [15 ^ []], 4 ^ [15 ^ []]), 15 ^ []), -(diff_closed(15 ^ []))],extension(19,bind([[_28404], [15 ^ []]]))).
% 2.60/3.46 cnf('1.2.1.2.1.2.1.1',plain,[diff_closed(15 ^ [])],reduction('1.2.1')).
% 2.60/3.46 cnf('1.2.1.2.1.3',plain,[-(in(4 ^ [15 ^ []], 15 ^ [])), -(diff_closed(15 ^ []))],extension(18,bind([[_28404], [15 ^ []]]))).
% 2.60/3.46 cnf('1.2.1.2.1.3.1',plain,[diff_closed(15 ^ [])],reduction('1.2.1')).
% 2.60/3.46 %-----------------------------------------------------
% 2.60/3.47
% 2.60/3.47 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------