%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : ALG227+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n023.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 : Thu Jul 14 17:22:05 EDT 2022
% Result : Theorem 0.45s 1.39s
% Output : Proof 0.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : ALG227+1 : TPTP v8.1.0. Released v3.4.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.33 % Computer : n023.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Wed Jun 8 09:32:23 EDT 2022
% 0.11/0.33 % CPUTime :
% 0.45/1.39 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.45/1.40 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.45/1.40
% 0.45/1.40 %-----------------------------------------------------
% 0.45/1.40 fof(t8_closure3, conjecture, ! [_41979] : (~ v1_xboole_0(_41979) => ! [_41996] : (m1_pboole(_41996, _41979) => ! [_42014] : (m1_subset_1(_42014, _41979) => ~ r2_hidden(_42014, k1_closure3(_41979, _41996)) => k1_funct_1(_41996, _42014) = k1_xboole_0))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t8_closure3)).
% 0.45/1.40 fof(d3_closure3, axiom, ! [_42391] : (~ v1_xboole_0(_42391) => ! [_42408] : (m1_pboole(_42408, _42391) => ! [_42426] : (_42426 = k1_closure3(_42391, _42408) <=> _42426 = a_2_0_closure3(_42391, _42408)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d3_closure3)).
% 0.45/1.40 fof(fraenkel_a_2_0_closure3, axiom, ! [_42674, _42677, _42680] : (~ v1_xboole_0(_42677) & m1_pboole(_42680, _42677) => (r2_hidden(_42674, a_2_0_closure3(_42677, _42680)) <=> ? [_42724] : (m1_subset_1(_42724, _42677) & _42674 = _42724 & (! k1_funct_1(_42680, _42724)) = k1_xboole_0))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fraenkel_a_2_0_closure3)).
% 0.45/1.40
% 0.45/1.40 cnf(1, plain, [v1_xboole_0(12 ^ [])], clausify(t8_closure3)).
% 0.45/1.40 cnf(2, plain, [-(m1_pboole(13 ^ [], 12 ^ []))], clausify(t8_closure3)).
% 0.45/1.40 cnf(3, plain, [-(m1_subset_1(14 ^ [], 12 ^ []))], clausify(t8_closure3)).
% 0.45/1.40 cnf(4, plain, [r2_hidden(14 ^ [], k1_closure3(12 ^ [], 13 ^ []))], clausify(t8_closure3)).
% 0.45/1.40 cnf(5, plain, [k1_funct_1(13 ^ [], 14 ^ []) = k1_xboole_0], clausify(t8_closure3)).
% 0.45/1.40 cnf(6, plain, [-(a_2_0_closure3(_17097, _17230) = a_2_0_closure3(_17164, _17295)), _17097 = _17164, _17230 = _17295], theory(equality)).
% 0.45/1.40 cnf(7, plain, [-(_12218 = _12218)], theory(equality)).
% 0.45/1.40 cnf(8, plain, [-(r2_hidden(_14441, _14572)), r2_hidden(_14374, _14507), _14374 = _14441, _14507 = _14572], theory(equality)).
% 0.45/1.40 cnf(9, plain, [-(v1_xboole_0(_20427)), m1_pboole(_20550, _20427), -(_20670 = k1_closure3(_20427, _20550)), _20670 = a_2_0_closure3(_20427, _20550)], clausify(d3_closure3)).
% 0.45/1.40 cnf(10, plain, [m1_pboole(_22675, _22588), -(v1_xboole_0(_22588)), -(r2_hidden(_22500, a_2_0_closure3(_22588, _22675))), m1_subset_1(_22986, _22588), _22500 = _22986, -(k1_funct_1(_22675, _22986) = k1_xboole_0)], clausify(fraenkel_a_2_0_closure3)).
% 0.45/1.40
% 0.45/1.40 cnf('1',plain,[v1_xboole_0(12 ^ [])],start(1)).
% 0.45/1.40 cnf('1.1',plain,[-(v1_xboole_0(12 ^ [])), m1_pboole(13 ^ [], 12 ^ []), -(a_2_0_closure3(12 ^ [], 13 ^ []) = k1_closure3(12 ^ [], 13 ^ [])), a_2_0_closure3(12 ^ [], 13 ^ []) = a_2_0_closure3(12 ^ [], 13 ^ [])],extension(9,bind([[_20670, _20427, _20550], [a_2_0_closure3(12 ^ [], 13 ^ []), 12 ^ [], 13 ^ []]]))).
% 0.45/1.40 cnf('1.1.1',plain,[-(m1_pboole(13 ^ [], 12 ^ []))],extension(2)).
% 0.45/1.40 cnf('1.1.2',plain,[a_2_0_closure3(12 ^ [], 13 ^ []) = k1_closure3(12 ^ [], 13 ^ []), -(r2_hidden(14 ^ [], k1_closure3(12 ^ [], 13 ^ []))), r2_hidden(14 ^ [], a_2_0_closure3(12 ^ [], 13 ^ [])), 14 ^ [] = 14 ^ []],extension(8,bind([[_14572, _14507, _14374, _14441], [k1_closure3(12 ^ [], 13 ^ []), a_2_0_closure3(12 ^ [], 13 ^ []), 14 ^ [], 14 ^ []]]))).
% 0.45/1.40 cnf('1.1.2.1',plain,[r2_hidden(14 ^ [], k1_closure3(12 ^ [], 13 ^ []))],extension(4)).
% 0.45/1.40 cnf('1.1.2.2',plain,[-(r2_hidden(14 ^ [], a_2_0_closure3(12 ^ [], 13 ^ []))), m1_pboole(13 ^ [], 12 ^ []), -(v1_xboole_0(12 ^ [])), m1_subset_1(14 ^ [], 12 ^ []), 14 ^ [] = 14 ^ [], -(k1_funct_1(13 ^ [], 14 ^ []) = k1_xboole_0)],extension(10,bind([[_22588, _22500, _22675, _22986], [12 ^ [], 14 ^ [], 13 ^ [], 14 ^ []]]))).
% 0.45/1.40 cnf('1.1.2.2.1',plain,[-(m1_pboole(13 ^ [], 12 ^ []))],extension(2)).
% 0.45/1.40 cnf('1.1.2.2.2',plain,[v1_xboole_0(12 ^ [])],extension(1)).
% 0.45/1.40 cnf('1.1.2.2.3',plain,[-(m1_subset_1(14 ^ [], 12 ^ []))],extension(3)).
% 0.45/1.40 cnf('1.1.2.2.4',plain,[-(14 ^ [] = 14 ^ [])],extension(7,bind([[_12218], [14 ^ []]]))).
% 0.45/1.40 cnf('1.1.2.2.5',plain,[k1_funct_1(13 ^ [], 14 ^ []) = k1_xboole_0],extension(5)).
% 0.45/1.40 cnf('1.1.2.3',plain,[-(14 ^ [] = 14 ^ [])],extension(7,bind([[_12218], [14 ^ []]]))).
% 0.45/1.40 cnf('1.1.3',plain,[-(a_2_0_closure3(12 ^ [], 13 ^ []) = a_2_0_closure3(12 ^ [], 13 ^ [])), 12 ^ [] = 12 ^ [], 13 ^ [] = 13 ^ []],extension(6,bind([[_17097, _17164, _17230, _17295], [12 ^ [], 12 ^ [], 13 ^ [], 13 ^ []]]))).
% 0.45/1.40 cnf('1.1.3.1',plain,[-(12 ^ [] = 12 ^ [])],extension(7,bind([[_12218], [12 ^ []]]))).
% 0.45/1.40 cnf('1.1.3.2',plain,[-(13 ^ [] = 13 ^ [])],extension(7,bind([[_12218], [13 ^ []]]))).
% 0.45/1.40 %-----------------------------------------------------
% 0.45/1.41
% 0.45/1.41 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------