%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU348+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n010.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:02:10 EDT 2022
% Result : Theorem 238.64s 231.00s
% Output : Proof 238.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU348+1 : TPTP v8.1.0. Released v3.3.0.
% 0.06/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n010.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 : Mon Jun 20 13:34:07 EDT 2022
% 0.12/0.33 % CPUTime :
% 238.64/231.00 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 238.64/231.00 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 238.64/231.01
% 238.64/231.01 %-----------------------------------------------------
% 238.64/231.01 fof(t29_lattice3, conjecture, ! [_168426, _168429] : (~ empty_carrier(_168429) & lattice(_168429) & latt_str(_168429) => ! [_168460] : (element(_168460, the_carrier(poset_of_lattice(_168429))) => (relstr_element_smaller(poset_of_lattice(_168429), _168426, _168460) <=> latt_set_smaller(_168429, cast_to_el_of_lattice(_168429, _168460), _168426)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t29_lattice3)).
% 238.64/231.01 fof(dt_k5_lattice3, axiom, ! [_168784, _168787] : (~ empty_carrier(_168784) & lattice(_168784) & latt_str(_168784) & element(_168787, the_carrier(poset_of_lattice(_168784))) => element(cast_to_el_of_lattice(_168784, _168787), the_carrier(_168784))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', dt_k5_lattice3)).
% 238.64/231.01 fof(d4_lattice3, axiom, ! [_169047] : (~ empty_carrier(_169047) & lattice(_169047) & latt_str(_169047) => ! [_169078] : (element(_169078, the_carrier(poset_of_lattice(_169047))) => cast_to_el_of_lattice(_169047, _169078) = _169078)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d4_lattice3)).
% 238.64/231.01 fof(t28_lattice3, axiom, ! [_169388, _169391] : (~ empty_carrier(_169391) & lattice(_169391) & latt_str(_169391) => ! [_169422] : (element(_169422, the_carrier(_169391)) => (latt_set_smaller(_169391, _169422, _169388) <=> relstr_element_smaller(poset_of_lattice(_169391), _169388, cast_to_el_of_LattPOSet(_169391, _169422))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t28_lattice3)).
% 238.64/231.01 fof(d2_lattice3, axiom, ! [_169741] : (~ empty_carrier(_169741) & lattice(_169741) & latt_str(_169741) => poset_of_lattice(_169741) = rel_str_of(the_carrier(_169741), k2_lattice3(_169741))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d2_lattice3)).
% 238.64/231.01 fof(d3_lattice3, axiom, ! [_170103] : (~ empty_carrier(_170103) & lattice(_170103) & latt_str(_170103) => ! [_170134] : (element(_170134, the_carrier(_170103)) => cast_to_el_of_LattPOSet(_170103, _170134) = _170134)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d3_lattice3)).
% 238.64/231.01
% 238.64/231.01 cnf(1, plain, [20 ^ [], 21 ^ []], clausify(t29_lattice3)).
% 238.64/231.01 cnf(2, plain, [-(21 ^ []), relstr_element_smaller(poset_of_lattice(18 ^ []), 17 ^ [], 19 ^ [])], clausify(t29_lattice3)).
% 238.64/231.01 cnf(3, plain, [-(element(cast_to_el_of_lattice(_60131, _60202), the_carrier(_60131))), -(empty_carrier(_60131)), lattice(_60131), latt_str(_60131), element(_60202, the_carrier(poset_of_lattice(_60131)))], clausify(dt_k5_lattice3)).
% 238.64/231.01 cnf(4, plain, [-(cast_to_el_of_lattice(_56517, _56746) = _56746), element(_56746, the_carrier(poset_of_lattice(_56517))), -(empty_carrier(_56517)), lattice(_56517), latt_str(_56517)], clausify(d4_lattice3)).
% 238.64/231.01 cnf(5, plain, [-(21 ^ []), -(latt_set_smaller(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []), 17 ^ []))], clausify(t29_lattice3)).
% 238.64/231.01 cnf(6, plain, [-(20 ^ []), latt_set_smaller(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []), 17 ^ [])], clausify(t29_lattice3)).
% 238.64/231.01 cnf(7, plain, [_32896 = _32941, -(_32941 = _32896)], theory(equality)).
% 238.64/231.01 cnf(8, plain, [latt_str(_73802), lattice(_73802), -(empty_carrier(_73802)), element(_74043, the_carrier(_73802)), -(latt_set_smaller(_73802, _74043, _73720)), relstr_element_smaller(poset_of_lattice(_73802), _73720, cast_to_el_of_LattPOSet(_73802, _74043))], clausify(t28_lattice3)).
% 238.64/231.01 cnf(9, plain, [-(relstr_element_smaller(_44310, _44477, _44640)), relstr_element_smaller(_44225, _44394, _44559), _44225 = _44310, _44394 = _44477, _44559 = _44640], theory(equality)).
% 238.64/231.01 cnf(10, plain, [-(20 ^ []), -(relstr_element_smaller(poset_of_lattice(18 ^ []), 17 ^ [], 19 ^ []))], clausify(t29_lattice3)).
% 238.64/231.01 cnf(11, plain, [-(poset_of_lattice(_55492) = rel_str_of(the_carrier(_55492), k2_lattice3(_55492))), -(empty_carrier(_55492)), lattice(_55492), latt_str(_55492)], clausify(d2_lattice3)).
% 238.64/231.01 cnf(12, plain, [-(lattice(18 ^ []))], clausify(t29_lattice3)).
% 238.64/231.01 cnf(13, plain, [-(latt_str(18 ^ []))], clausify(t29_lattice3)).
% 238.64/231.01 cnf(14, plain, [-(_33175 = _33286), _33175 = _33231, _33231 = _33286], theory(equality)).
% 238.64/231.01 cnf(15, plain, [_50527 = _50576, -(poset_of_lattice(_50527) = poset_of_lattice(_50576))], theory(equality)).
% 238.64/231.01 cnf(16, plain, [empty_carrier(18 ^ [])], clausify(t29_lattice3)).
% 238.64/231.01 cnf(17, plain, [latt_str(_73802), lattice(_73802), -(empty_carrier(_73802)), element(_74043, the_carrier(_73802)), latt_set_smaller(_73802, _74043, _73720), -(relstr_element_smaller(poset_of_lattice(_73802), _73720, cast_to_el_of_LattPOSet(_73802, _74043)))], clausify(t28_lattice3)).
% 238.64/231.01 cnf(18, plain, [-(_32743 = _32743)], theory(equality)).
% 238.64/231.01 cnf(19, plain, [-(element(19 ^ [], the_carrier(poset_of_lattice(18 ^ []))))], clausify(t29_lattice3)).
% 238.64/231.01 cnf(20, plain, [-(cast_to_el_of_LattPOSet(_55952, _56179) = _56179), element(_56179, the_carrier(_55952)), -(empty_carrier(_55952)), lattice(_55952), latt_str(_55952)], clausify(d3_lattice3)).
% 238.64/231.01
% 238.64/231.01 cnf('1',plain,[20 ^ [], 21 ^ []],start(1)).
% 238.64/231.01 cnf('1.1',plain,[-(20 ^ []), latt_set_smaller(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []), 17 ^ [])],extension(6)).
% 238.64/231.01 cnf('1.1.1',plain,[-(latt_set_smaller(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []), 17 ^ [])), latt_str(18 ^ []), lattice(18 ^ []), -(empty_carrier(18 ^ [])), element(cast_to_el_of_lattice(18 ^ [], 19 ^ []), the_carrier(18 ^ [])), relstr_element_smaller(poset_of_lattice(18 ^ []), 17 ^ [], cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])))],extension(8,bind([[_73720, _73802, _74043], [17 ^ [], 18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])]]))).
% 238.64/231.01 cnf('1.1.1.1',plain,[-(latt_str(18 ^ []))],extension(13)).
% 238.64/231.01 cnf('1.1.1.2',plain,[-(lattice(18 ^ []))],extension(12)).
% 238.64/231.01 cnf('1.1.1.3',plain,[empty_carrier(18 ^ [])],extension(16)).
% 238.64/231.01 cnf('1.1.1.4',plain,[-(element(cast_to_el_of_lattice(18 ^ [], 19 ^ []), the_carrier(18 ^ []))), -(empty_carrier(18 ^ [])), lattice(18 ^ []), latt_str(18 ^ []), element(19 ^ [], the_carrier(poset_of_lattice(18 ^ [])))],extension(3,bind([[_60202, _60131], [19 ^ [], 18 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.4.1',plain,[empty_carrier(18 ^ [])],extension(16)).
% 238.64/231.01 cnf('1.1.1.4.2',plain,[-(lattice(18 ^ []))],extension(12)).
% 238.64/231.01 cnf('1.1.1.4.3',plain,[-(latt_str(18 ^ []))],extension(13)).
% 238.64/231.01 cnf('1.1.1.4.4',plain,[-(element(19 ^ [], the_carrier(poset_of_lattice(18 ^ []))))],extension(19)).
% 238.64/231.01 cnf('1.1.1.5',plain,[-(relstr_element_smaller(poset_of_lattice(18 ^ []), 17 ^ [], cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])))), relstr_element_smaller(poset_of_lattice(18 ^ []), 17 ^ [], 19 ^ []), poset_of_lattice(18 ^ []) = poset_of_lattice(18 ^ []), 17 ^ [] = 17 ^ [], 19 ^ [] = cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))],extension(9,bind([[_44225, _44310, _44394, _44477, _44559, _44640], [poset_of_lattice(18 ^ []), poset_of_lattice(18 ^ []), 17 ^ [], 17 ^ [], 19 ^ [], cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))]]))).
% 238.64/231.01 cnf('1.1.1.5.1',plain,[-(relstr_element_smaller(poset_of_lattice(18 ^ []), 17 ^ [], 19 ^ [])), relstr_element_smaller(poset_of_lattice(18 ^ []), 17 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])), poset_of_lattice(18 ^ []) = poset_of_lattice(18 ^ []), 17 ^ [] = 17 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []) = 19 ^ []],extension(9,bind([[_44225, _44310, _44394, _44477, _44559, _44640], [poset_of_lattice(18 ^ []), poset_of_lattice(18 ^ []), 17 ^ [], 17 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []), 19 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.1',plain,[-(relstr_element_smaller(poset_of_lattice(18 ^ []), 17 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))), relstr_element_smaller(rel_str_of(the_carrier(18 ^ []), k2_lattice3(18 ^ [])), 17 ^ [], 19 ^ []), rel_str_of(the_carrier(18 ^ []), k2_lattice3(18 ^ [])) = poset_of_lattice(18 ^ []), 17 ^ [] = 17 ^ [], 19 ^ [] = cast_to_el_of_lattice(18 ^ [], 19 ^ [])],extension(9,bind([[_44225, _44310, _44394, _44477, _44559, _44640], [rel_str_of(the_carrier(18 ^ []), k2_lattice3(18 ^ [])), poset_of_lattice(18 ^ []), 17 ^ [], 17 ^ [], 19 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])]]))).
% 238.64/231.01 cnf('1.1.1.5.1.1.1',plain,[-(relstr_element_smaller(rel_str_of(the_carrier(18 ^ []), k2_lattice3(18 ^ [])), 17 ^ [], 19 ^ [])), relstr_element_smaller(poset_of_lattice(18 ^ []), 17 ^ [], 19 ^ []), poset_of_lattice(18 ^ []) = rel_str_of(the_carrier(18 ^ []), k2_lattice3(18 ^ [])), 17 ^ [] = 17 ^ [], 19 ^ [] = 19 ^ []],extension(9,bind([[_44225, _44310, _44394, _44477, _44559, _44640], [poset_of_lattice(18 ^ []), rel_str_of(the_carrier(18 ^ []), k2_lattice3(18 ^ [])), 17 ^ [], 17 ^ [], 19 ^ [], 19 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.1.1.1',plain,[-(relstr_element_smaller(poset_of_lattice(18 ^ []), 17 ^ [], 19 ^ [])), -(20 ^ [])],extension(10)).
% 238.64/231.01 cnf('1.1.1.5.1.1.1.1.1',plain,[20 ^ []],reduction('1')).
% 238.64/231.01 cnf('1.1.1.5.1.1.1.2',plain,[-(poset_of_lattice(18 ^ []) = rel_str_of(the_carrier(18 ^ []), k2_lattice3(18 ^ []))), -(empty_carrier(18 ^ [])), lattice(18 ^ []), latt_str(18 ^ [])],extension(11,bind([[_55492], [18 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.1.1.2.1',plain,[empty_carrier(18 ^ [])],extension(16)).
% 238.64/231.01 cnf('1.1.1.5.1.1.1.2.2',plain,[-(lattice(18 ^ []))],extension(12)).
% 238.64/231.01 cnf('1.1.1.5.1.1.1.2.3',plain,[-(latt_str(18 ^ []))],extension(13)).
% 238.64/231.01 cnf('1.1.1.5.1.1.1.3',plain,[-(17 ^ [] = 17 ^ [])],extension(18,bind([[_32743], [17 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.1.1.4',plain,[-(19 ^ [] = 19 ^ [])],extension(18,bind([[_32743], [19 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.1.2',plain,[-(rel_str_of(the_carrier(18 ^ []), k2_lattice3(18 ^ [])) = poset_of_lattice(18 ^ [])), poset_of_lattice(18 ^ []) = rel_str_of(the_carrier(18 ^ []), k2_lattice3(18 ^ []))],extension(7,bind([[_32896, _32941], [poset_of_lattice(18 ^ []), rel_str_of(the_carrier(18 ^ []), k2_lattice3(18 ^ []))]]))).
% 238.64/231.01 cnf('1.1.1.5.1.1.2.1',plain,[-(poset_of_lattice(18 ^ []) = rel_str_of(the_carrier(18 ^ []), k2_lattice3(18 ^ []))), -(empty_carrier(18 ^ [])), lattice(18 ^ []), latt_str(18 ^ [])],extension(11,bind([[_55492], [18 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.1.2.1.1',plain,[empty_carrier(18 ^ [])],extension(16)).
% 238.64/231.01 cnf('1.1.1.5.1.1.2.1.2',plain,[-(lattice(18 ^ []))],extension(12)).
% 238.64/231.01 cnf('1.1.1.5.1.1.2.1.3',plain,[-(latt_str(18 ^ []))],extension(13)).
% 238.64/231.01 cnf('1.1.1.5.1.1.3',plain,[-(17 ^ [] = 17 ^ []), 17 ^ [] = 17 ^ []],extension(7,bind([[_32896, _32941], [17 ^ [], 17 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.1.3.1',plain,[-(17 ^ [] = 17 ^ [])],extension(18,bind([[_32743], [17 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.1.4',plain,[-(19 ^ [] = cast_to_el_of_lattice(18 ^ [], 19 ^ [])), cast_to_el_of_lattice(18 ^ [], 19 ^ []) = 19 ^ []],extension(7,bind([[_32896, _32941], [cast_to_el_of_lattice(18 ^ [], 19 ^ []), 19 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.1.4.1',plain,[-(cast_to_el_of_lattice(18 ^ [], 19 ^ []) = 19 ^ []), element(19 ^ [], the_carrier(poset_of_lattice(18 ^ []))), -(empty_carrier(18 ^ [])), lattice(18 ^ []), latt_str(18 ^ [])],extension(4,bind([[_56746, _56517], [19 ^ [], 18 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.1.4.1.1',plain,[-(element(19 ^ [], the_carrier(poset_of_lattice(18 ^ []))))],extension(19)).
% 238.64/231.01 cnf('1.1.1.5.1.1.4.1.2',plain,[empty_carrier(18 ^ [])],extension(16)).
% 238.64/231.01 cnf('1.1.1.5.1.1.4.1.3',plain,[-(lattice(18 ^ []))],extension(12)).
% 238.64/231.01 cnf('1.1.1.5.1.1.4.1.4',plain,[-(latt_str(18 ^ []))],extension(13)).
% 238.64/231.01 cnf('1.1.1.5.1.2',plain,[-(poset_of_lattice(18 ^ []) = poset_of_lattice(18 ^ [])), poset_of_lattice(18 ^ []) = poset_of_lattice(18 ^ [])],extension(7,bind([[_32896, _32941], [poset_of_lattice(18 ^ []), poset_of_lattice(18 ^ [])]]))).
% 238.64/231.01 cnf('1.1.1.5.1.2.1',plain,[-(poset_of_lattice(18 ^ []) = poset_of_lattice(18 ^ [])), 18 ^ [] = 18 ^ []],extension(15,bind([[_50527, _50576], [18 ^ [], 18 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.2.1.1',plain,[-(18 ^ [] = 18 ^ [])],extension(18,bind([[_32743], [18 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.3',plain,[-(17 ^ [] = 17 ^ []), 17 ^ [] = 17 ^ []],extension(7,bind([[_32896, _32941], [17 ^ [], 17 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.3.1',plain,[-(17 ^ [] = 17 ^ [])],extension(18,bind([[_32743], [17 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.4',plain,[-(cast_to_el_of_lattice(18 ^ [], 19 ^ []) = 19 ^ []), element(19 ^ [], the_carrier(poset_of_lattice(18 ^ []))), -(empty_carrier(18 ^ [])), lattice(18 ^ []), latt_str(18 ^ [])],extension(4,bind([[_56746, _56517], [19 ^ [], 18 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.1.4.1',plain,[-(element(19 ^ [], the_carrier(poset_of_lattice(18 ^ []))))],extension(19)).
% 238.64/231.01 cnf('1.1.1.5.1.4.2',plain,[empty_carrier(18 ^ [])],extension(16)).
% 238.64/231.01 cnf('1.1.1.5.1.4.3',plain,[-(lattice(18 ^ []))],extension(12)).
% 238.64/231.01 cnf('1.1.1.5.1.4.4',plain,[-(latt_str(18 ^ []))],extension(13)).
% 238.64/231.01 cnf('1.1.1.5.2',plain,[-(poset_of_lattice(18 ^ []) = poset_of_lattice(18 ^ [])), 18 ^ [] = 18 ^ []],extension(15,bind([[_50527, _50576], [18 ^ [], 18 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.2.1',plain,[-(18 ^ [] = 18 ^ [])],extension(18,bind([[_32743], [18 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.3',plain,[-(17 ^ [] = 17 ^ [])],extension(18,bind([[_32743], [17 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.4',plain,[-(19 ^ [] = cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))), 19 ^ [] = cast_to_el_of_lattice(18 ^ [], 19 ^ []), cast_to_el_of_lattice(18 ^ [], 19 ^ []) = cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))],extension(14,bind([[_33175, _33231, _33286], [19 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []), cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))]]))).
% 238.64/231.01 cnf('1.1.1.5.4.1',plain,[-(19 ^ [] = cast_to_el_of_lattice(18 ^ [], 19 ^ [])), cast_to_el_of_lattice(18 ^ [], 19 ^ []) = 19 ^ []],extension(7,bind([[_32896, _32941], [cast_to_el_of_lattice(18 ^ [], 19 ^ []), 19 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.4.1.1',plain,[-(cast_to_el_of_lattice(18 ^ [], 19 ^ []) = 19 ^ []), element(19 ^ [], the_carrier(poset_of_lattice(18 ^ []))), -(empty_carrier(18 ^ [])), lattice(18 ^ []), latt_str(18 ^ [])],extension(4,bind([[_56746, _56517], [19 ^ [], 18 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.4.1.1.1',plain,[-(element(19 ^ [], the_carrier(poset_of_lattice(18 ^ []))))],extension(19)).
% 238.64/231.01 cnf('1.1.1.5.4.1.1.2',plain,[empty_carrier(18 ^ [])],extension(16)).
% 238.64/231.01 cnf('1.1.1.5.4.1.1.3',plain,[-(lattice(18 ^ []))],extension(12)).
% 238.64/231.01 cnf('1.1.1.5.4.1.1.4',plain,[-(latt_str(18 ^ []))],extension(13)).
% 238.64/231.01 cnf('1.1.1.5.4.2',plain,[-(cast_to_el_of_lattice(18 ^ [], 19 ^ []) = cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))), cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])) = cast_to_el_of_lattice(18 ^ [], 19 ^ [])],extension(7,bind([[_32896, _32941], [cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])), cast_to_el_of_lattice(18 ^ [], 19 ^ [])]]))).
% 238.64/231.01 cnf('1.1.1.5.4.2.1',plain,[-(cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])) = cast_to_el_of_lattice(18 ^ [], 19 ^ [])), element(cast_to_el_of_lattice(18 ^ [], 19 ^ []), the_carrier(18 ^ [])), -(empty_carrier(18 ^ [])), lattice(18 ^ []), latt_str(18 ^ [])],extension(20,bind([[_56179, _55952], [cast_to_el_of_lattice(18 ^ [], 19 ^ []), 18 ^ []]]))).
% 238.64/231.01 cnf('1.1.1.5.4.2.1.1',plain,[-(element(cast_to_el_of_lattice(18 ^ [], 19 ^ []), the_carrier(18 ^ [])))],lemmata('1.1.1')).
% 238.64/231.01 cnf('1.1.1.5.4.2.1.2',plain,[empty_carrier(18 ^ [])],extension(16)).
% 238.64/231.01 cnf('1.1.1.5.4.2.1.3',plain,[-(lattice(18 ^ []))],extension(12)).
% 238.64/231.01 cnf('1.1.1.5.4.2.1.4',plain,[-(latt_str(18 ^ []))],extension(13)).
% 238.64/231.01 cnf('1.2',plain,[-(21 ^ []), -(latt_set_smaller(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []), 17 ^ []))],extension(5)).
% 238.64/231.01 cnf('1.2.1',plain,[latt_set_smaller(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []), 17 ^ []), latt_str(18 ^ []), lattice(18 ^ []), -(empty_carrier(18 ^ [])), element(cast_to_el_of_lattice(18 ^ [], 19 ^ []), the_carrier(18 ^ [])), -(relstr_element_smaller(poset_of_lattice(18 ^ []), 17 ^ [], cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))))],extension(17,bind([[_73720, _73802, _74043], [17 ^ [], 18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])]]))).
% 238.64/231.01 cnf('1.2.1.1',plain,[-(latt_str(18 ^ []))],extension(13)).
% 238.64/231.01 cnf('1.2.1.2',plain,[-(lattice(18 ^ []))],extension(12)).
% 238.64/231.01 cnf('1.2.1.3',plain,[empty_carrier(18 ^ [])],extension(16)).
% 238.64/231.01 cnf('1.2.1.4',plain,[-(element(cast_to_el_of_lattice(18 ^ [], 19 ^ []), the_carrier(18 ^ []))), -(empty_carrier(18 ^ [])), lattice(18 ^ []), latt_str(18 ^ []), element(19 ^ [], the_carrier(poset_of_lattice(18 ^ [])))],extension(3,bind([[_60202, _60131], [19 ^ [], 18 ^ []]]))).
% 238.64/231.01 cnf('1.2.1.4.1',plain,[empty_carrier(18 ^ [])],extension(16)).
% 238.64/231.01 cnf('1.2.1.4.2',plain,[-(lattice(18 ^ []))],extension(12)).
% 238.64/231.01 cnf('1.2.1.4.3',plain,[-(latt_str(18 ^ []))],extension(13)).
% 238.64/231.01 cnf('1.2.1.4.4',plain,[-(element(19 ^ [], the_carrier(poset_of_lattice(18 ^ []))))],extension(19)).
% 238.64/231.01 cnf('1.2.1.5',plain,[relstr_element_smaller(poset_of_lattice(18 ^ []), 17 ^ [], cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))), -(relstr_element_smaller(poset_of_lattice(18 ^ []), 17 ^ [], 19 ^ [])), poset_of_lattice(18 ^ []) = poset_of_lattice(18 ^ []), 17 ^ [] = 17 ^ [], cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])) = 19 ^ []],extension(9,bind([[_44225, _44310, _44394, _44477, _44559, _44640], [poset_of_lattice(18 ^ []), poset_of_lattice(18 ^ []), 17 ^ [], 17 ^ [], cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])), 19 ^ []]]))).
% 238.64/231.01 cnf('1.2.1.5.1',plain,[relstr_element_smaller(poset_of_lattice(18 ^ []), 17 ^ [], 19 ^ []), -(21 ^ [])],extension(2)).
% 238.64/231.01 cnf('1.2.1.5.1.1',plain,[21 ^ []],reduction('1')).
% 238.64/231.01 cnf('1.2.1.5.2',plain,[-(poset_of_lattice(18 ^ []) = poset_of_lattice(18 ^ [])), 18 ^ [] = 18 ^ []],extension(15,bind([[_50527, _50576], [18 ^ [], 18 ^ []]]))).
% 238.64/231.01 cnf('1.2.1.5.2.1',plain,[-(18 ^ [] = 18 ^ [])],extension(18,bind([[_32743], [18 ^ []]]))).
% 238.64/231.01 cnf('1.2.1.5.3',plain,[-(17 ^ [] = 17 ^ [])],extension(18,bind([[_32743], [17 ^ []]]))).
% 238.64/231.01 cnf('1.2.1.5.4',plain,[-(cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])) = 19 ^ []), 19 ^ [] = cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))],extension(7,bind([[_32896, _32941], [19 ^ [], cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))]]))).
% 238.64/231.01 cnf('1.2.1.5.4.1',plain,[-(19 ^ [] = cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))), 19 ^ [] = cast_to_el_of_lattice(18 ^ [], 19 ^ []), cast_to_el_of_lattice(18 ^ [], 19 ^ []) = cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))],extension(14,bind([[_33175, _33231, _33286], [19 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []), cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))]]))).
% 238.64/231.01 cnf('1.2.1.5.4.1.1',plain,[-(19 ^ [] = cast_to_el_of_lattice(18 ^ [], 19 ^ [])), cast_to_el_of_lattice(18 ^ [], 19 ^ []) = 19 ^ []],extension(7,bind([[_32896, _32941], [cast_to_el_of_lattice(18 ^ [], 19 ^ []), 19 ^ []]]))).
% 238.64/231.01 cnf('1.2.1.5.4.1.1.1',plain,[-(cast_to_el_of_lattice(18 ^ [], 19 ^ []) = 19 ^ []), element(19 ^ [], the_carrier(poset_of_lattice(18 ^ []))), -(empty_carrier(18 ^ [])), lattice(18 ^ []), latt_str(18 ^ [])],extension(4,bind([[_56746, _56517], [19 ^ [], 18 ^ []]]))).
% 238.64/231.01 cnf('1.2.1.5.4.1.1.1.1',plain,[-(element(19 ^ [], the_carrier(poset_of_lattice(18 ^ []))))],extension(19)).
% 238.64/231.01 cnf('1.2.1.5.4.1.1.1.2',plain,[empty_carrier(18 ^ [])],extension(16)).
% 238.64/231.01 cnf('1.2.1.5.4.1.1.1.3',plain,[-(lattice(18 ^ []))],extension(12)).
% 238.64/231.01 cnf('1.2.1.5.4.1.1.1.4',plain,[-(latt_str(18 ^ []))],extension(13)).
% 238.64/231.01 cnf('1.2.1.5.4.1.2',plain,[-(cast_to_el_of_lattice(18 ^ [], 19 ^ []) = cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ []))), cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])) = cast_to_el_of_lattice(18 ^ [], 19 ^ [])],extension(7,bind([[_32896, _32941], [cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])), cast_to_el_of_lattice(18 ^ [], 19 ^ [])]]))).
% 238.64/231.01 cnf('1.2.1.5.4.1.2.1',plain,[-(cast_to_el_of_LattPOSet(18 ^ [], cast_to_el_of_lattice(18 ^ [], 19 ^ [])) = cast_to_el_of_lattice(18 ^ [], 19 ^ [])), element(cast_to_el_of_lattice(18 ^ [], 19 ^ []), the_carrier(18 ^ [])), -(empty_carrier(18 ^ [])), lattice(18 ^ []), latt_str(18 ^ [])],extension(20,bind([[_56179, _55952], [cast_to_el_of_lattice(18 ^ [], 19 ^ []), 18 ^ []]]))).
% 238.64/231.01 cnf('1.2.1.5.4.1.2.1.1',plain,[-(element(cast_to_el_of_lattice(18 ^ [], 19 ^ []), the_carrier(18 ^ [])))],lemmata('1.2.1')).
% 238.64/231.01 cnf('1.2.1.5.4.1.2.1.2',plain,[empty_carrier(18 ^ [])],extension(16)).
% 238.64/231.01 cnf('1.2.1.5.4.1.2.1.3',plain,[-(lattice(18 ^ []))],extension(12)).
% 238.64/231.01 cnf('1.2.1.5.4.1.2.1.4',plain,[-(latt_str(18 ^ []))],extension(13)).
% 238.64/231.01 %-----------------------------------------------------
% 238.64/231.02
% 238.64/231.02 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------