%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : LAT370+1 : TPTP v8.1.0. Released v3.4.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 : Sun Jul 17 05:43:33 EDT 2022
% Result : Theorem 72.11s 69.85s
% Output : Proof 72.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : LAT370+1 : TPTP v8.1.0. Released v3.4.0.
% 0.06/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.33 % Computer : n029.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 29 02:41:37 EDT 2022
% 0.11/0.33 % CPUTime :
% 72.11/69.85 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 72.11/69.86 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 72.11/69.87
% 72.11/69.87 %-----------------------------------------------------
% 72.11/69.87 fof(t43_waybel34, conjecture, ! [_140518] : (v2_orders_2(_140518) & v3_orders_2(_140518) & v4_orders_2(_140518) & v1_lattice3(_140518) & v2_lattice3(_140518) & v3_lattice3(_140518) & v3_waybel_3(_140518) & l1_orders_2(_140518) => ! [_140582] : (v1_funct_1(_140582) & v1_funct_2(_140582, u1_struct_0(_140518), u1_struct_0(_140518)) & v7_waybel_1(_140582, _140518) & m2_relset_1(_140582, u1_struct_0(_140518), u1_struct_0(_140518)) => v1_waybel34(k2_waybel_1(_140518, _140518, _140582), _140518, k2_yellow_2(_140518, _140518, _140582)) => v4_waybel_0(k2_yellow_2(_140518, _140518, _140582), _140518))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t43_waybel34)).
% 72.11/69.87 fof(cc10_waybel_0, axiom, ! [_141360] : (l1_orders_2(_141360) => ~ v3_struct_0(_141360) & v2_orders_2(_141360) & v3_lattice3(_141360) => ~ v3_struct_0(_141360) & v2_orders_2(_141360) & v24_waybel_0(_141360) & v25_waybel_0(_141360)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc10_waybel_0)).
% 72.11/69.87 fof(cc11_yellow_0, axiom, ! [_141624] : (v3_orders_2(_141624) & v4_orders_2(_141624) & v2_lattice3(_141624) & l1_orders_2(_141624) => ! [_141660] : (m1_yellow_0(_141660, _141624) => ~ v3_struct_0(_141660) & v4_yellow_0(_141660, _141624) & v5_yellow_0(_141660, _141624) => ~ v3_struct_0(_141660) & v3_orders_2(_141660) & v4_orders_2(_141660) & v2_lattice3(_141660) & v4_yellow_0(_141660, _141624) & v5_yellow_0(_141660, _141624))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc11_yellow_0)).
% 72.11/69.87 fof(cc14_waybel_0, axiom, ! [_142117] : (l1_orders_2(_142117) => ~ v3_struct_0(_142117) & v2_orders_2(_142117) & v4_orders_2(_142117) & v2_yellow_0(_142117) & v25_waybel_0(_142117) => ~ v3_struct_0(_142117) & v2_orders_2(_142117) & v4_orders_2(_142117) & v1_lattice3(_142117) & v2_yellow_0(_142117)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc14_waybel_0)).
% 72.11/69.87 fof(cc1_lattice3, axiom, ! [_142458] : (l1_orders_2(_142458) => v1_lattice3(_142458) => ~ v3_struct_0(_142458)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc1_lattice3)).
% 72.11/69.87 fof(cc2_lattice3, axiom, ! [_142637] : (l1_orders_2(_142637) => v2_lattice3(_142637) => ~ v3_struct_0(_142637)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc2_lattice3)).
% 72.11/69.87 fof(cc3_waybel_1, axiom, ! [_142796] : (~ v3_struct_0(_142796) & l1_orders_2(_142796) => ! [_142820] : (m1_relset_1(_142820, u1_struct_0(_142796), u1_struct_0(_142796)) => v1_funct_1(_142820) & v1_funct_2(_142820, u1_struct_0(_142796), u1_struct_0(_142796)) & v7_waybel_1(_142820, _142796) => v1_funct_1(_142820) & ~ v1_xboole_0(_142820) & v1_funct_2(_142820, u1_struct_0(_142796), u1_struct_0(_142796)) & v1_partfun1(_142820, u1_struct_0(_142796), u1_struct_0(_142796)) & v6_waybel_1(_142820, _142796))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc3_waybel_1)).
% 72.11/69.87 fof(cc3_yellow_0, axiom, ! [_143292] : (l1_orders_2(_143292) => ~ v3_struct_0(_143292) & v3_lattice3(_143292) => ~ v3_struct_0(_143292) & v3_yellow_0(_143292)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc3_yellow_0)).
% 72.11/69.87 fof(cc4_yellow_0, axiom, ! [_143497] : (l1_orders_2(_143497) => v3_yellow_0(_143497) => v1_yellow_0(_143497) & v2_yellow_0(_143497)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc4_yellow_0)).
% 72.11/69.87 fof(cc6_yellow_0, axiom, ! [_143665] : (v2_orders_2(_143665) & l1_orders_2(_143665) => ! [_143687] : (m1_yellow_0(_143687, _143665) => v4_yellow_0(_143687, _143665) => v2_orders_2(_143687) & v4_yellow_0(_143687, _143665))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc6_yellow_0)).
% 72.11/69.87 fof(dt_k2_yellow_2, axiom, ! [_143944, _143947, _143950] : (~ v3_struct_0(_143944) & l1_orders_2(_143944) & ~ v3_struct_0(_143947) & l1_orders_2(_143947) & v1_funct_1(_143950) & v1_funct_2(_143950, u1_struct_0(_143944), u1_struct_0(_143947)) & m1_relset_1(_143950, u1_struct_0(_143944), u1_struct_0(_143947)) => v1_orders_2(k2_yellow_2(_143944, _143947, _143950)) & v4_yellow_0(k2_yellow_2(_143944, _143947, _143950), _143947) & m1_yellow_0(k2_yellow_2(_143944, _143947, _143950), _143947)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k2_yellow_2)).
% 72.11/69.87 fof(dt_k3_waybel_1, axiom, ! [_144428, _144431, _144434] : (~ v3_struct_0(_144428) & l1_orders_2(_144428) & ~ v3_struct_0(_144431) & l1_orders_2(_144431) & v1_funct_1(_144434) & v1_funct_2(_144434, u1_struct_0(_144428), u1_struct_0(_144431)) & m1_relset_1(_144434, u1_struct_0(_144428), u1_struct_0(_144431)) => v1_funct_1(k3_waybel_1(_144428, _144431, _144434)) & v1_funct_2(k3_waybel_1(_144428, _144431, _144434), u1_struct_0(k2_yellow_2(_144428, _144431, _144434)), u1_struct_0(_144431)) & m2_relset_1(k3_waybel_1(_144428, _144431, _144434), u1_struct_0(k2_yellow_2(_144428, _144431, _144434)), u1_struct_0(_144431))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k3_waybel_1)).
% 72.11/69.87 fof(dt_m1_yellow_0, axiom, ! [_145025] : (l1_orders_2(_145025) => ! [_145040] : (m1_yellow_0(_145040, _145025) => l1_orders_2(_145040))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_m1_yellow_0)).
% 72.11/69.87 fof(fc10_waybel10, axiom, ! [_145212, _145215] : (~ v3_struct_0(_145212) & v2_orders_2(_145212) & v3_orders_2(_145212) & v4_orders_2(_145212) & l1_orders_2(_145212) & v1_funct_1(_145215) & v1_funct_2(_145215, u1_struct_0(_145212), u1_struct_0(_145212)) & v7_waybel_1(_145215, _145212) & m1_relset_1(_145215, u1_struct_0(_145212), u1_struct_0(_145212)) => ~ v3_struct_0(k2_yellow_2(_145212, _145212, _145215)) & v1_orders_2(k2_yellow_2(_145212, _145212, _145215)) & v2_orders_2(k2_yellow_2(_145212, _145212, _145215)) & v3_orders_2(k2_yellow_2(_145212, _145212, _145215)) & v4_orders_2(k2_yellow_2(_145212, _145212, _145215)) & v4_yellow_0(k2_yellow_2(_145212, _145212, _145215), _145212) & v5_yellow_0(k2_yellow_2(_145212, _145212, _145215), _145212) & v7_yellow_0(k2_yellow_2(_145212, _145212, _145215), _145212) & v3_waybel_0(k2_yellow_2(_145212, _145212, _145215), _145212)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc10_waybel10)).
% 72.11/69.87 fof(fc10_waybel34, axiom, ! [_146054, _146057] : (v2_orders_2(_146054) & v3_orders_2(_146054) & v4_orders_2(_146054) & v1_lattice3(_146054) & v2_lattice3(_146054) & v3_lattice3(_146054) & l1_orders_2(_146054) & v1_funct_1(_146057) & v1_funct_2(_146057, u1_struct_0(_146054), u1_struct_0(_146054)) & v6_waybel_1(_146057, _146054) & m1_relset_1(_146057, u1_struct_0(_146054), u1_struct_0(_146054)) => ~ v3_struct_0(k2_yellow_2(_146054, _146054, _146057)) & v1_orders_2(k2_yellow_2(_146054, _146054, _146057)) & v2_orders_2(k2_yellow_2(_146054, _146054, _146057)) & v3_orders_2(k2_yellow_2(_146054, _146054, _146057)) & v4_orders_2(k2_yellow_2(_146054, _146054, _146057)) & v1_yellow_0(k2_yellow_2(_146054, _146054, _146057)) & v2_yellow_0(k2_yellow_2(_146054, _146054, _146057)) & v3_yellow_0(k2_yellow_2(_146054, _146054, _146057)) & v4_yellow_0(k2_yellow_2(_146054, _146054, _146057), _146054) & v24_waybel_0(k2_yellow_2(_146054, _146054, _146057)) & v25_waybel_0(k2_yellow_2(_146054, _146054, _146057)) & v1_lattice3(k2_yellow_2(_146054, _146054, _146057)) & v2_lattice3(k2_yellow_2(_146054, _146054, _146057)) & v3_lattice3(k2_yellow_2(_146054, _146054, _146057))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc10_waybel34)).
% 72.11/69.87 fof(redefinition_m2_relset_1, axiom, ! [_147410, _147413, _147416] : (m2_relset_1(_147416, _147410, _147413) <=> m1_relset_1(_147416, _147410, _147413)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', redefinition_m2_relset_1)).
% 72.11/69.87 fof(t25_waybel34, axiom, ! [_147584] : (v2_orders_2(_147584) & v3_orders_2(_147584) & v4_orders_2(_147584) & v1_lattice3(_147584) & v2_lattice3(_147584) & v3_lattice3(_147584) & l1_orders_2(_147584) => ! [_147641] : (v2_orders_2(_147641) & v3_orders_2(_147641) & v4_orders_2(_147641) & v1_lattice3(_147641) & v2_lattice3(_147641) & v3_lattice3(_147641) & v3_waybel_3(_147641) & l1_orders_2(_147641) => ! [_147705] : (v1_funct_1(_147705) & v1_funct_2(_147705, u1_struct_0(_147584), u1_struct_0(_147641)) & v17_waybel_0(_147705, _147584, _147641) & m2_relset_1(_147705, u1_struct_0(_147584), u1_struct_0(_147641)) => v1_waybel34(k1_waybel34(_147584, _147641, _147705), _147641, _147584) => v22_waybel_0(_147705, _147584, _147641)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t25_waybel34)).
% 72.11/69.87 fof(t39_waybel34, axiom, ! [_148295] : (v2_orders_2(_148295) & v3_orders_2(_148295) & v4_orders_2(_148295) & v1_lattice3(_148295) & v2_lattice3(_148295) & v3_lattice3(_148295) & l1_orders_2(_148295) => ! [_148352] : (v1_funct_1(_148352) & v1_funct_2(_148352, u1_struct_0(_148295), u1_struct_0(_148295)) & v7_waybel_1(_148352, _148295) & m2_relset_1(_148352, u1_struct_0(_148295), u1_struct_0(_148295)) => v18_waybel_0(k2_waybel_1(_148295, _148295, _148352), _148295, k2_yellow_2(_148295, _148295, _148352)) & v17_waybel_0(k3_waybel_1(_148295, _148295, _148352), k2_yellow_2(_148295, _148295, _148352), _148295) & k2_waybel34(k2_yellow_2(_148295, _148295, _148352), _148295, k2_waybel_1(_148295, _148295, _148352)) = k3_waybel_1(_148295, _148295, _148352) & k1_waybel34(k2_yellow_2(_148295, _148295, _148352), _148295, k3_waybel_1(_148295, _148295, _148352)) = k2_waybel_1(_148295, _148295, _148352))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t39_waybel34)).
% 72.11/69.87 fof(t40_waybel34, axiom, ! [_149116] : (v2_orders_2(_149116) & v3_orders_2(_149116) & v4_orders_2(_149116) & v1_lattice3(_149116) & v2_lattice3(_149116) & v3_lattice3(_149116) & l1_orders_2(_149116) => ! [_149173] : (v1_funct_1(_149173) & v1_funct_2(_149173, u1_struct_0(_149116), u1_struct_0(_149116)) & v7_waybel_1(_149173, _149116) & m2_relset_1(_149173, u1_struct_0(_149116), u1_struct_0(_149116)) => (v4_waybel_0(k2_yellow_2(_149116, _149116, _149173), _149116) <=> v22_waybel_0(k3_waybel_1(_149116, _149116, _149173), k2_yellow_2(_149116, _149116, _149173), _149116)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t40_waybel34)).
% 72.11/69.87
% 72.11/69.87 cnf(1, plain, [-(v2_orders_2(32 ^ []))], clausify(t43_waybel34)).
% 72.11/69.87 cnf(2, plain, [-(v3_orders_2(32 ^ []))], clausify(t43_waybel34)).
% 72.11/69.87 cnf(3, plain, [-(v4_orders_2(32 ^ []))], clausify(t43_waybel34)).
% 72.11/69.87 cnf(4, plain, [-(v1_lattice3(32 ^ []))], clausify(t43_waybel34)).
% 72.11/69.87 cnf(5, plain, [-(v2_lattice3(32 ^ []))], clausify(t43_waybel34)).
% 72.11/69.87 cnf(6, plain, [-(v3_lattice3(32 ^ []))], clausify(t43_waybel34)).
% 72.11/69.87 cnf(7, plain, [-(v3_waybel_3(32 ^ []))], clausify(t43_waybel34)).
% 72.11/69.87 cnf(8, plain, [-(l1_orders_2(32 ^ []))], clausify(t43_waybel34)).
% 72.11/69.87 cnf(9, plain, [-(v1_funct_1(33 ^ []))], clausify(t43_waybel34)).
% 72.11/69.87 cnf(10, plain, [-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))], clausify(t43_waybel34)).
% 72.11/69.87 cnf(11, plain, [-(v7_waybel_1(33 ^ [], 32 ^ []))], clausify(t43_waybel34)).
% 72.11/69.87 cnf(12, plain, [-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))], clausify(t43_waybel34)).
% 72.11/69.87 cnf(13, plain, [-(v1_waybel34(k2_waybel_1(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [], k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))], clausify(t43_waybel34)).
% 72.11/69.87 cnf(14, plain, [v4_waybel_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])], clausify(t43_waybel34)).
% 72.11/69.87 cnf(15, plain, [-(k2_yellow_2(_16083, _16085, _16087) = k2_yellow_2(_16084, _16086, _16088)), _16083 = _16084, _16085 = _16086, _16087 = _16088], theory(equality)).
% 72.11/69.87 cnf(16, plain, [-(_14955 = _14955)], theory(equality)).
% 72.11/69.87 cnf(17, plain, [_14961 = _14962, -(_14962 = _14961)], theory(equality)).
% 72.11/69.87 cnf(18, plain, [-(v1_waybel34(_15354, _15356, _15358)), v1_waybel34(_15353, _15355, _15357), _15353 = _15354, _15355 = _15356, _15357 = _15358], theory(equality)).
% 72.11/69.87 cnf(19, plain, [-(v3_struct_0(_15669)), _15668 = _15669, v3_struct_0(_15668)], theory(equality)).
% 72.11/69.87 cnf(20, plain, [l1_orders_2(_16265), -(v25_waybel_0(_16265)), -(v3_struct_0(_16265)), v2_orders_2(_16265), v3_lattice3(_16265)], clausify(cc10_waybel_0)).
% 72.11/69.87 cnf(21, plain, [l1_orders_2(_16309), v2_lattice3(_16309), v4_orders_2(_16309), v3_orders_2(_16309), m1_yellow_0(_16318, _16309), -(v3_orders_2(_16318)), -(v3_struct_0(_16318)), v4_yellow_0(_16318, _16309), v5_yellow_0(_16318, _16309)], clausify(cc11_yellow_0)).
% 72.11/69.87 cnf(22, plain, [l1_orders_2(_16309), v2_lattice3(_16309), v4_orders_2(_16309), v3_orders_2(_16309), m1_yellow_0(_16318, _16309), -(v4_orders_2(_16318)), -(v3_struct_0(_16318)), v4_yellow_0(_16318, _16309), v5_yellow_0(_16318, _16309)], clausify(cc11_yellow_0)).
% 72.11/69.87 cnf(23, plain, [l1_orders_2(_16309), v2_lattice3(_16309), v4_orders_2(_16309), v3_orders_2(_16309), m1_yellow_0(_16318, _16309), -(v2_lattice3(_16318)), -(v3_struct_0(_16318)), v4_yellow_0(_16318, _16309), v5_yellow_0(_16318, _16309)], clausify(cc11_yellow_0)).
% 72.11/69.87 cnf(24, plain, [l1_orders_2(_16437), -(v1_lattice3(_16437)), -(v3_struct_0(_16437)), v2_orders_2(_16437), v4_orders_2(_16437), v2_yellow_0(_16437), v25_waybel_0(_16437)], clausify(cc14_waybel_0)).
% 72.11/69.87 cnf(25, plain, [l1_orders_2(_16555), v1_lattice3(_16555), v3_struct_0(_16555)], clausify(cc1_lattice3)).
% 72.11/69.87 cnf(26, plain, [l1_orders_2(_16925), v2_lattice3(_16925), v3_struct_0(_16925)], clausify(cc2_lattice3)).
% 72.11/69.87 cnf(27, plain, [l1_orders_2(_17048), -(v3_struct_0(_17048)), m1_relset_1(_17053, u1_struct_0(_17048), u1_struct_0(_17048)), -(v6_waybel_1(_17053, _17048)), v1_funct_1(_17053), v1_funct_2(_17053, u1_struct_0(_17048), u1_struct_0(_17048)), v7_waybel_1(_17053, _17048)], clausify(cc3_waybel_1)).
% 72.11/69.87 cnf(28, plain, [l1_orders_2(_17091), -(v3_yellow_0(_17091)), -(v3_struct_0(_17091)), v3_lattice3(_17091)], clausify(cc3_yellow_0)).
% 72.11/69.87 cnf(29, plain, [l1_orders_2(_17170), v3_yellow_0(_17170), -(v2_yellow_0(_17170))], clausify(cc4_yellow_0)).
% 72.11/69.87 cnf(30, plain, [l1_orders_2(_17262), v2_orders_2(_17262), m1_yellow_0(_17267, _17262), v4_yellow_0(_17267, _17262), -(v2_orders_2(_17267))], clausify(cc6_yellow_0)).
% 72.11/69.87 cnf(31, plain, [-(v4_yellow_0(k2_yellow_2(_17771, _17772, _17773), _17772)), -(v3_struct_0(_17771)), l1_orders_2(_17771), -(v3_struct_0(_17772)), l1_orders_2(_17772), v1_funct_1(_17773), v1_funct_2(_17773, u1_struct_0(_17771), u1_struct_0(_17772)), m1_relset_1(_17773, u1_struct_0(_17771), u1_struct_0(_17772))], clausify(dt_k2_yellow_2)).
% 72.11/69.87 cnf(32, plain, [-(m1_yellow_0(k2_yellow_2(_17771, _17772, _17773), _17772)), -(v3_struct_0(_17771)), l1_orders_2(_17771), -(v3_struct_0(_17772)), l1_orders_2(_17772), v1_funct_1(_17773), v1_funct_2(_17773, u1_struct_0(_17771), u1_struct_0(_17772)), m1_relset_1(_17773, u1_struct_0(_17771), u1_struct_0(_17772))], clausify(dt_k2_yellow_2)).
% 72.11/69.87 cnf(33, plain, [-(v1_funct_1(k3_waybel_1(_17823, _17824, _17825))), -(v3_struct_0(_17823)), l1_orders_2(_17823), -(v3_struct_0(_17824)), l1_orders_2(_17824), v1_funct_1(_17825), v1_funct_2(_17825, u1_struct_0(_17823), u1_struct_0(_17824)), m1_relset_1(_17825, u1_struct_0(_17823), u1_struct_0(_17824))], clausify(dt_k3_waybel_1)).
% 72.11/69.87 cnf(34, plain, [-(v1_funct_2(k3_waybel_1(_17823, _17824, _17825), u1_struct_0(k2_yellow_2(_17823, _17824, _17825)), u1_struct_0(_17824))), -(v3_struct_0(_17823)), l1_orders_2(_17823), -(v3_struct_0(_17824)), l1_orders_2(_17824), v1_funct_1(_17825), v1_funct_2(_17825, u1_struct_0(_17823), u1_struct_0(_17824)), m1_relset_1(_17825, u1_struct_0(_17823), u1_struct_0(_17824))], clausify(dt_k3_waybel_1)).
% 72.11/69.87 cnf(35, plain, [-(m2_relset_1(k3_waybel_1(_17823, _17824, _17825), u1_struct_0(k2_yellow_2(_17823, _17824, _17825)), u1_struct_0(_17824))), -(v3_struct_0(_17823)), l1_orders_2(_17823), -(v3_struct_0(_17824)), l1_orders_2(_17824), v1_funct_1(_17825), v1_funct_2(_17825, u1_struct_0(_17823), u1_struct_0(_17824)), m1_relset_1(_17825, u1_struct_0(_17823), u1_struct_0(_17824))], clausify(dt_k3_waybel_1)).
% 72.11/69.87 cnf(36, plain, [l1_orders_2(_17943), m1_yellow_0(_17946, _17943), -(l1_orders_2(_17946))], clausify(dt_m1_yellow_0)).
% 72.11/69.87 cnf(37, plain, [v3_struct_0(k2_yellow_2(_18015, _18015, _18016)), -(v3_struct_0(_18015)), v2_orders_2(_18015), v3_orders_2(_18015), v4_orders_2(_18015), l1_orders_2(_18015), v1_funct_1(_18016), v1_funct_2(_18016, u1_struct_0(_18015), u1_struct_0(_18015)), v7_waybel_1(_18016, _18015), m1_relset_1(_18016, u1_struct_0(_18015), u1_struct_0(_18015))], clausify(fc10_waybel10)).
% 72.11/69.87 cnf(38, plain, [-(v2_orders_2(k2_yellow_2(_18015, _18015, _18016))), -(v3_struct_0(_18015)), v2_orders_2(_18015), v3_orders_2(_18015), v4_orders_2(_18015), l1_orders_2(_18015), v1_funct_1(_18016), v1_funct_2(_18016, u1_struct_0(_18015), u1_struct_0(_18015)), v7_waybel_1(_18016, _18015), m1_relset_1(_18016, u1_struct_0(_18015), u1_struct_0(_18015))], clausify(fc10_waybel10)).
% 72.11/69.87 cnf(39, plain, [-(v4_orders_2(k2_yellow_2(_18015, _18015, _18016))), -(v3_struct_0(_18015)), v2_orders_2(_18015), v3_orders_2(_18015), v4_orders_2(_18015), l1_orders_2(_18015), v1_funct_1(_18016), v1_funct_2(_18016, u1_struct_0(_18015), u1_struct_0(_18015)), v7_waybel_1(_18016, _18015), m1_relset_1(_18016, u1_struct_0(_18015), u1_struct_0(_18015))], clausify(fc10_waybel10)).
% 72.11/69.87 cnf(40, plain, [-(v5_yellow_0(k2_yellow_2(_18015, _18015, _18016), _18015)), -(v3_struct_0(_18015)), v2_orders_2(_18015), v3_orders_2(_18015), v4_orders_2(_18015), l1_orders_2(_18015), v1_funct_1(_18016), v1_funct_2(_18016, u1_struct_0(_18015), u1_struct_0(_18015)), v7_waybel_1(_18016, _18015), m1_relset_1(_18016, u1_struct_0(_18015), u1_struct_0(_18015))], clausify(fc10_waybel10)).
% 72.11/69.87 cnf(41, plain, [-(v3_lattice3(k2_yellow_2(_18109, _18109, _18110))), v2_orders_2(_18109), v3_orders_2(_18109), v4_orders_2(_18109), v1_lattice3(_18109), v2_lattice3(_18109), v3_lattice3(_18109), l1_orders_2(_18109), v1_funct_1(_18110), v1_funct_2(_18110, u1_struct_0(_18109), u1_struct_0(_18109)), v6_waybel_1(_18110, _18109), m1_relset_1(_18110, u1_struct_0(_18109), u1_struct_0(_18109))], clausify(fc10_waybel34)).
% 72.11/69.87 cnf(42, plain, [m2_relset_1(_20030, _20028, _20029), -(m1_relset_1(_20030, _20028, _20029))], clausify(redefinition_m2_relset_1)).
% 72.11/69.87 cnf(43, plain, [l1_orders_2(_20060), v3_lattice3(_20060), v2_lattice3(_20060), v1_lattice3(_20060), v4_orders_2(_20060), v3_orders_2(_20060), v2_orders_2(_20060), m2_relset_1(_20092, u1_struct_0(_20060), u1_struct_0(_20075)), v17_waybel_0(_20092, _20060, _20075), v1_funct_2(_20092, u1_struct_0(_20060), u1_struct_0(_20075)), v1_funct_1(_20092), v1_waybel34(k1_waybel34(_20060, _20075, _20092), _20075, _20060), -(v22_waybel_0(_20092, _20060, _20075)), v2_orders_2(_20075), v3_orders_2(_20075), v4_orders_2(_20075), v1_lattice3(_20075), v2_lattice3(_20075), v3_lattice3(_20075), v3_waybel_3(_20075), l1_orders_2(_20075)], clausify(t25_waybel34)).
% 72.11/69.87 cnf(44, plain, [m2_relset_1(_20158, u1_struct_0(_20143), u1_struct_0(_20143)), v7_waybel_1(_20158, _20143), v1_funct_2(_20158, u1_struct_0(_20143), u1_struct_0(_20143)), v1_funct_1(_20158), -(v17_waybel_0(k3_waybel_1(_20143, _20143, _20158), k2_yellow_2(_20143, _20143, _20158), _20143)), v2_orders_2(_20143), v3_orders_2(_20143), v4_orders_2(_20143), v1_lattice3(_20143), v2_lattice3(_20143), v3_lattice3(_20143), l1_orders_2(_20143)], clausify(t39_waybel34)).
% 72.11/69.87 cnf(45, plain, [m2_relset_1(_20158, u1_struct_0(_20143), u1_struct_0(_20143)), v7_waybel_1(_20158, _20143), v1_funct_2(_20158, u1_struct_0(_20143), u1_struct_0(_20143)), v1_funct_1(_20158), -(k1_waybel34(k2_yellow_2(_20143, _20143, _20158), _20143, k3_waybel_1(_20143, _20143, _20158)) = k2_waybel_1(_20143, _20143, _20158)), v2_orders_2(_20143), v3_orders_2(_20143), v4_orders_2(_20143), v1_lattice3(_20143), v2_lattice3(_20143), v3_lattice3(_20143), l1_orders_2(_20143)], clausify(t39_waybel34)).
% 72.11/69.87 cnf(46, plain, [l1_orders_2(_20258), v3_lattice3(_20258), v2_lattice3(_20258), v1_lattice3(_20258), v4_orders_2(_20258), v3_orders_2(_20258), v2_orders_2(_20258), m2_relset_1(_20273, u1_struct_0(_20258), u1_struct_0(_20258)), v7_waybel_1(_20273, _20258), v1_funct_2(_20273, u1_struct_0(_20258), u1_struct_0(_20258)), v1_funct_1(_20273), -(v4_waybel_0(k2_yellow_2(_20258, _20258, _20273), _20258)), v22_waybel_0(k3_waybel_1(_20258, _20258, _20273), k2_yellow_2(_20258, _20258, _20273), _20258)], clausify(t40_waybel34)).
% 72.11/69.87
% 72.11/69.87 cnf('1',plain,[v4_waybel_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])],start(14)).
% 72.11/69.87 cnf('1.1',plain,[-(v4_waybel_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), l1_orders_2(32 ^ []), v3_lattice3(32 ^ []), v2_lattice3(32 ^ []), v1_lattice3(32 ^ []), v4_orders_2(32 ^ []), v3_orders_2(32 ^ []), v2_orders_2(32 ^ []), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v7_waybel_1(33 ^ [], 32 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v1_funct_1(33 ^ []), v22_waybel_0(k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ []), k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])],extension(46,bind([[_20273, _20258], [33 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.2',plain,[-(v3_lattice3(32 ^ []))],extension(6)).
% 72.11/69.87 cnf('1.1.3',plain,[-(v2_lattice3(32 ^ []))],extension(5)).
% 72.11/69.87 cnf('1.1.4',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.5',plain,[-(v4_orders_2(32 ^ []))],extension(3)).
% 72.11/69.87 cnf('1.1.6',plain,[-(v3_orders_2(32 ^ []))],extension(2)).
% 72.11/69.87 cnf('1.1.7',plain,[-(v2_orders_2(32 ^ []))],extension(1)).
% 72.11/69.87 cnf('1.1.8',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.9',plain,[-(v7_waybel_1(33 ^ [], 32 ^ []))],extension(11)).
% 72.11/69.87 cnf('1.1.10',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.11',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12',plain,[-(v22_waybel_0(k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ []), k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v3_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v2_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v1_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v4_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v3_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v2_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), m2_relset_1(k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ []), u1_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), u1_struct_0(32 ^ [])), v17_waybel_0(k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ []), k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ []), v1_funct_2(k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ []), u1_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), u1_struct_0(32 ^ [])), v1_funct_1(k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ [])), v1_waybel34(k1_waybel34(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [], k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ [])), 32 ^ [], k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v2_orders_2(32 ^ []), v3_orders_2(32 ^ []), v4_orders_2(32 ^ []), v1_lattice3(32 ^ []), v2_lattice3(32 ^ []), v3_lattice3(32 ^ []), v3_waybel_3(32 ^ []), l1_orders_2(32 ^ [])],extension(43,bind([[_20092, _20060, _20075], [k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ []), k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.1',plain,[-(l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), l1_orders_2(32 ^ []), m1_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])],extension(36,bind([[_17946, _17943], [k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.1.2',plain,[-(m1_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(32,bind([[_17773, _17771, _17772], [33 ^ [], 32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.1.2.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.1.2.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.1.2.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.1.2.2',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.1.2.3',plain,[v3_struct_0(32 ^ [])],lemmata('1.1.12.1.2')).
% 72.11/69.87 cnf('1.1.12.1.2.4',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.1.2.5',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.1.2.6',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.1.2.7',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.1.2.7.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.2',plain,[-(v3_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), v2_orders_2(32 ^ []), v3_orders_2(32 ^ []), v4_orders_2(32 ^ []), v1_lattice3(32 ^ []), v2_lattice3(32 ^ []), v3_lattice3(32 ^ []), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v6_waybel_1(33 ^ [], 32 ^ []), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(41,bind([[_18110, _18109], [33 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.2.1',plain,[-(v2_orders_2(32 ^ []))],extension(1)).
% 72.11/69.87 cnf('1.1.12.2.2',plain,[-(v3_orders_2(32 ^ []))],extension(2)).
% 72.11/69.87 cnf('1.1.12.2.3',plain,[-(v4_orders_2(32 ^ []))],extension(3)).
% 72.11/69.87 cnf('1.1.12.2.4',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.2.5',plain,[-(v2_lattice3(32 ^ []))],extension(5)).
% 72.11/69.87 cnf('1.1.12.2.6',plain,[-(v3_lattice3(32 ^ []))],extension(6)).
% 72.11/69.87 cnf('1.1.12.2.7',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.2.8',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.2.9',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.2.10',plain,[-(v6_waybel_1(33 ^ [], 32 ^ [])), l1_orders_2(32 ^ []), -(v3_struct_0(32 ^ [])), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v7_waybel_1(33 ^ [], 32 ^ [])],extension(27,bind([[_17053, _17048], [33 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.2.10.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.2.10.2',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.2.10.2.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.2.10.2.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.2.10.3',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.2.10.3.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.2.10.4',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.2.10.5',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.2.10.6',plain,[-(v7_waybel_1(33 ^ [], 32 ^ []))],extension(11)).
% 72.11/69.87 cnf('1.1.12.2.11',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.2.11.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.3',plain,[-(v2_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), l1_orders_2(32 ^ []), v2_lattice3(32 ^ []), v4_orders_2(32 ^ []), v3_orders_2(32 ^ []), m1_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ []), -(v3_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), v4_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ []), v5_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])],extension(23,bind([[_16318, _16309], [k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.3.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.3.2',plain,[-(v2_lattice3(32 ^ []))],extension(5)).
% 72.11/69.87 cnf('1.1.12.3.3',plain,[-(v4_orders_2(32 ^ []))],extension(3)).
% 72.11/69.87 cnf('1.1.12.3.4',plain,[-(v3_orders_2(32 ^ []))],extension(2)).
% 72.11/69.87 cnf('1.1.12.3.5',plain,[-(m1_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(32,bind([[_17773, _17771, _17772], [33 ^ [], 32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.3.5.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.3.5.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.3.5.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.3.5.2',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.3.5.3',plain,[v3_struct_0(32 ^ [])],lemmata('1.1.12.3.5')).
% 72.11/69.87 cnf('1.1.12.3.5.4',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.3.5.5',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.3.5.6',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.3.5.7',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.3.5.7.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.3.6',plain,[v3_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), -(v3_struct_0(32 ^ [])), v2_orders_2(32 ^ []), v3_orders_2(32 ^ []), v4_orders_2(32 ^ []), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v7_waybel_1(33 ^ [], 32 ^ []), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(37,bind([[_18016, _18015], [33 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.3.6.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.3.6.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.3.6.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.3.6.2',plain,[-(v2_orders_2(32 ^ []))],extension(1)).
% 72.11/69.87 cnf('1.1.12.3.6.3',plain,[-(v3_orders_2(32 ^ []))],extension(2)).
% 72.11/69.87 cnf('1.1.12.3.6.4',plain,[-(v4_orders_2(32 ^ []))],extension(3)).
% 72.11/69.87 cnf('1.1.12.3.6.5',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.3.6.6',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.3.6.7',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.3.6.8',plain,[-(v7_waybel_1(33 ^ [], 32 ^ []))],extension(11)).
% 72.11/69.87 cnf('1.1.12.3.6.9',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.3.6.9.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.3.7',plain,[-(v4_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(31,bind([[_17773, _17771, _17772], [33 ^ [], 32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.3.7.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.3.7.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.3.7.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.3.7.2',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.3.7.3',plain,[v3_struct_0(32 ^ [])],lemmata('1.1.12.3.7')).
% 72.11/69.87 cnf('1.1.12.3.7.4',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.3.7.5',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.3.7.6',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.3.7.7',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.3.7.7.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.3.8',plain,[-(v5_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), -(v3_struct_0(32 ^ [])), v2_orders_2(32 ^ []), v3_orders_2(32 ^ []), v4_orders_2(32 ^ []), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v7_waybel_1(33 ^ [], 32 ^ []), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(40,bind([[_18016, _18015], [33 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.3.8.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.3.8.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.3.8.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.3.8.2',plain,[-(v2_orders_2(32 ^ []))],extension(1)).
% 72.11/69.87 cnf('1.1.12.3.8.3',plain,[-(v3_orders_2(32 ^ []))],extension(2)).
% 72.11/69.87 cnf('1.1.12.3.8.4',plain,[-(v4_orders_2(32 ^ []))],extension(3)).
% 72.11/69.87 cnf('1.1.12.3.8.5',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.3.8.6',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.3.8.7',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.3.8.8',plain,[-(v7_waybel_1(33 ^ [], 32 ^ []))],extension(11)).
% 72.11/69.87 cnf('1.1.12.3.8.9',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.3.8.9.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.4',plain,[-(v1_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), -(v3_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), v2_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v4_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v2_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v25_waybel_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))],extension(24,bind([[_16437], [k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.4.1',plain,[-(l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))],lemmata('1.1.12')).
% 72.11/69.87 cnf('1.1.12.4.2',plain,[v3_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v2_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))],extension(26,bind([[_16925], [k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.4.2.1',plain,[-(l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))],lemmata('1.1.12.4')).
% 72.11/69.87 cnf('1.1.12.4.2.2',plain,[-(v2_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))],lemmata('1.1.12')).
% 72.11/69.87 cnf('1.1.12.4.3',plain,[-(v2_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), -(v3_struct_0(32 ^ [])), v2_orders_2(32 ^ []), v3_orders_2(32 ^ []), v4_orders_2(32 ^ []), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v7_waybel_1(33 ^ [], 32 ^ []), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(38,bind([[_18016, _18015], [33 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.4.3.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.4.3.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.4.3.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.4.3.2',plain,[-(v2_orders_2(32 ^ []))],extension(1)).
% 72.11/69.87 cnf('1.1.12.4.3.3',plain,[-(v3_orders_2(32 ^ []))],extension(2)).
% 72.11/69.87 cnf('1.1.12.4.3.4',plain,[-(v4_orders_2(32 ^ []))],extension(3)).
% 72.11/69.87 cnf('1.1.12.4.3.5',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.4.3.6',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.4.3.7',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.4.3.8',plain,[-(v7_waybel_1(33 ^ [], 32 ^ []))],extension(11)).
% 72.11/69.87 cnf('1.1.12.4.3.9',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.4.3.9.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.4.4',plain,[-(v4_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), -(v3_struct_0(32 ^ [])), v2_orders_2(32 ^ []), v3_orders_2(32 ^ []), v4_orders_2(32 ^ []), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v7_waybel_1(33 ^ [], 32 ^ []), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(39,bind([[_18016, _18015], [33 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.4.4.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.4.4.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.4.4.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.4.4.2',plain,[-(v2_orders_2(32 ^ []))],extension(1)).
% 72.11/69.87 cnf('1.1.12.4.4.3',plain,[-(v3_orders_2(32 ^ []))],extension(2)).
% 72.11/69.87 cnf('1.1.12.4.4.4',plain,[-(v4_orders_2(32 ^ []))],extension(3)).
% 72.11/69.87 cnf('1.1.12.4.4.5',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.4.4.6',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.4.4.7',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.4.4.8',plain,[-(v7_waybel_1(33 ^ [], 32 ^ []))],extension(11)).
% 72.11/69.87 cnf('1.1.12.4.4.9',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.4.4.9.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.4.5',plain,[-(v2_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v3_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))],extension(29,bind([[_17170], [k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.4.5.1',plain,[-(l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))],lemmata('1.1.12.4')).
% 72.11/69.87 cnf('1.1.12.4.5.2',plain,[-(v3_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), -(v3_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), v3_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))],extension(28,bind([[_17091], [k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.4.5.2.1',plain,[-(l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))],lemmata('1.1.12.4.5')).
% 72.11/69.87 cnf('1.1.12.4.5.2.2',plain,[v3_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))],lemmata('1.1.12.4')).
% 72.11/69.87 cnf('1.1.12.4.5.2.3',plain,[-(v3_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))],lemmata('1.1.12')).
% 72.11/69.87 cnf('1.1.12.4.6',plain,[-(v25_waybel_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), -(v3_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), v2_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v3_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))],extension(20,bind([[_16265], [k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.4.6.1',plain,[-(l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))],lemmata('1.1.12.4')).
% 72.11/69.87 cnf('1.1.12.4.6.2',plain,[v3_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))],lemmata('1.1.12.4')).
% 72.11/69.87 cnf('1.1.12.4.6.3',plain,[-(v2_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))],lemmata('1.1.12.4')).
% 72.11/69.87 cnf('1.1.12.4.6.4',plain,[-(v3_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))],lemmata('1.1.12')).
% 72.11/69.87 cnf('1.1.12.5',plain,[-(v4_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), l1_orders_2(32 ^ []), v2_lattice3(32 ^ []), v4_orders_2(32 ^ []), v3_orders_2(32 ^ []), m1_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ []), -(v3_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), v4_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ []), v5_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])],extension(22,bind([[_16318, _16309], [k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.5.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.5.2',plain,[-(v2_lattice3(32 ^ []))],extension(5)).
% 72.11/69.87 cnf('1.1.12.5.3',plain,[-(v4_orders_2(32 ^ []))],extension(3)).
% 72.11/69.87 cnf('1.1.12.5.4',plain,[-(v3_orders_2(32 ^ []))],extension(2)).
% 72.11/69.87 cnf('1.1.12.5.5',plain,[-(m1_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(32,bind([[_17773, _17771, _17772], [33 ^ [], 32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.5.5.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.5.5.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.5.5.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.5.5.2',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.5.5.3',plain,[v3_struct_0(32 ^ [])],lemmata('1.1.12.5.5')).
% 72.11/69.87 cnf('1.1.12.5.5.4',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.5.5.5',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.5.5.6',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.5.5.7',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.5.5.7.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.5.6',plain,[v3_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v1_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))],extension(25,bind([[_16555], [k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.5.6.1',plain,[-(l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))],lemmata('1.1.12')).
% 72.11/69.87 cnf('1.1.12.5.6.2',plain,[-(v1_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))],lemmata('1.1.12')).
% 72.11/69.87 cnf('1.1.12.5.7',plain,[-(v4_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(31,bind([[_17773, _17771, _17772], [33 ^ [], 32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.5.7.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.5.7.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.5.7.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.5.7.2',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.5.7.3',plain,[v3_struct_0(32 ^ [])],lemmata('1.1.12.5.7')).
% 72.11/69.87 cnf('1.1.12.5.7.4',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.5.7.5',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.5.7.6',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.5.7.7',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.5.7.7.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.5.8',plain,[-(v5_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), -(v3_struct_0(32 ^ [])), v2_orders_2(32 ^ []), v3_orders_2(32 ^ []), v4_orders_2(32 ^ []), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v7_waybel_1(33 ^ [], 32 ^ []), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(40,bind([[_18016, _18015], [33 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.5.8.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.5.8.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.5.8.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.5.8.2',plain,[-(v2_orders_2(32 ^ []))],extension(1)).
% 72.11/69.87 cnf('1.1.12.5.8.3',plain,[-(v3_orders_2(32 ^ []))],extension(2)).
% 72.11/69.87 cnf('1.1.12.5.8.4',plain,[-(v4_orders_2(32 ^ []))],extension(3)).
% 72.11/69.87 cnf('1.1.12.5.8.5',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.5.8.6',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.5.8.7',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.5.8.8',plain,[-(v7_waybel_1(33 ^ [], 32 ^ []))],extension(11)).
% 72.11/69.87 cnf('1.1.12.5.8.9',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.5.8.9.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.6',plain,[-(v3_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), l1_orders_2(32 ^ []), v2_lattice3(32 ^ []), v4_orders_2(32 ^ []), v3_orders_2(32 ^ []), m1_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ []), -(v3_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), v4_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ []), v5_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])],extension(21,bind([[_16318, _16309], [k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.6.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.6.2',plain,[-(v2_lattice3(32 ^ []))],extension(5)).
% 72.11/69.87 cnf('1.1.12.6.3',plain,[-(v4_orders_2(32 ^ []))],extension(3)).
% 72.11/69.87 cnf('1.1.12.6.4',plain,[-(v3_orders_2(32 ^ []))],extension(2)).
% 72.11/69.87 cnf('1.1.12.6.5',plain,[-(m1_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(32,bind([[_17773, _17771, _17772], [33 ^ [], 32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.6.5.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.6.5.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.6.5.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.6.5.2',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.6.5.3',plain,[v3_struct_0(32 ^ [])],lemmata('1.1.12.6.5')).
% 72.11/69.87 cnf('1.1.12.6.5.4',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.6.5.5',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.6.5.6',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.6.5.7',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.6.5.7.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.6.6',plain,[v3_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), v1_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))],extension(25,bind([[_16555], [k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.6.6.1',plain,[-(l1_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))],lemmata('1.1.12')).
% 72.11/69.87 cnf('1.1.12.6.6.2',plain,[-(v1_lattice3(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))],lemmata('1.1.12')).
% 72.11/69.87 cnf('1.1.12.6.7',plain,[-(v4_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(31,bind([[_17773, _17771, _17772], [33 ^ [], 32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.6.7.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.6.7.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.6.7.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.6.7.2',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.6.7.3',plain,[v3_struct_0(32 ^ [])],lemmata('1.1.12.6.7')).
% 72.11/69.87 cnf('1.1.12.6.7.4',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.6.7.5',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.6.7.6',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.6.7.7',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.6.7.7.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.6.8',plain,[-(v5_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), -(v3_struct_0(32 ^ [])), v2_orders_2(32 ^ []), v3_orders_2(32 ^ []), v4_orders_2(32 ^ []), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v7_waybel_1(33 ^ [], 32 ^ []), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(40,bind([[_18016, _18015], [33 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.6.8.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.6.8.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.6.8.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.6.8.2',plain,[-(v2_orders_2(32 ^ []))],extension(1)).
% 72.11/69.87 cnf('1.1.12.6.8.3',plain,[-(v3_orders_2(32 ^ []))],extension(2)).
% 72.11/69.87 cnf('1.1.12.6.8.4',plain,[-(v4_orders_2(32 ^ []))],extension(3)).
% 72.11/69.87 cnf('1.1.12.6.8.5',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.6.8.6',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.6.8.7',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.6.8.8',plain,[-(v7_waybel_1(33 ^ [], 32 ^ []))],extension(11)).
% 72.11/69.87 cnf('1.1.12.6.8.9',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.6.8.9.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.7',plain,[-(v2_orders_2(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), l1_orders_2(32 ^ []), v2_orders_2(32 ^ []), m1_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ []), v4_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])],extension(30,bind([[_17267, _17262], [k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.7.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.7.2',plain,[-(v2_orders_2(32 ^ []))],extension(1)).
% 72.11/69.87 cnf('1.1.12.7.3',plain,[-(m1_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(32,bind([[_17773, _17771, _17772], [33 ^ [], 32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.7.3.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.7.3.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.7.3.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.7.3.2',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.7.3.3',plain,[v3_struct_0(32 ^ [])],lemmata('1.1.12.7.3')).
% 72.11/69.87 cnf('1.1.12.7.3.4',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.7.3.5',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.7.3.6',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.7.3.7',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.7.3.7.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.7.4',plain,[-(v4_yellow_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(31,bind([[_17773, _17771, _17772], [33 ^ [], 32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.7.4.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.7.4.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.7.4.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.7.4.2',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.7.4.3',plain,[v3_struct_0(32 ^ [])],lemmata('1.1.12.7.4')).
% 72.11/69.87 cnf('1.1.12.7.4.4',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.7.4.5',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.7.4.6',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.7.4.7',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.7.4.7.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.8',plain,[-(m2_relset_1(k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ []), u1_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), u1_struct_0(32 ^ []))), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(35,bind([[_17825, _17823, _17824], [33 ^ [], 32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.8.1',plain,[v3_struct_0(32 ^ []), -(v3_struct_0(32 ^ [])), 32 ^ [] = 32 ^ []],extension(19,bind([[_15668, _15669], [32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.8.1.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.8.1.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.8.1.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.8.1.2',plain,[-(32 ^ [] = 32 ^ [])],extension(16,bind([[_14955], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.8.2',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.8.3',plain,[v3_struct_0(32 ^ [])],lemmata('1.1.12.8')).
% 72.11/69.87 cnf('1.1.12.8.4',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.8.5',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.8.6',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.8.7',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.8.7.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.9',plain,[-(v17_waybel_0(k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ []), k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [])), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v7_waybel_1(33 ^ [], 32 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v1_funct_1(33 ^ []), v2_orders_2(32 ^ []), v3_orders_2(32 ^ []), v4_orders_2(32 ^ []), v1_lattice3(32 ^ []), v2_lattice3(32 ^ []), v3_lattice3(32 ^ []), l1_orders_2(32 ^ [])],extension(44,bind([[_20158, _20143], [33 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.9.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.9.2',plain,[-(v7_waybel_1(33 ^ [], 32 ^ []))],extension(11)).
% 72.11/69.87 cnf('1.1.12.9.3',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.9.4',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.9.5',plain,[-(v2_orders_2(32 ^ []))],extension(1)).
% 72.11/69.87 cnf('1.1.12.9.6',plain,[-(v3_orders_2(32 ^ []))],extension(2)).
% 72.11/69.87 cnf('1.1.12.9.7',plain,[-(v4_orders_2(32 ^ []))],extension(3)).
% 72.11/69.87 cnf('1.1.12.9.8',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.9.9',plain,[-(v2_lattice3(32 ^ []))],extension(5)).
% 72.11/69.87 cnf('1.1.12.9.10',plain,[-(v3_lattice3(32 ^ []))],extension(6)).
% 72.11/69.87 cnf('1.1.12.9.11',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.10',plain,[-(v1_funct_2(k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ []), u1_struct_0(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), u1_struct_0(32 ^ []))), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(34,bind([[_17825, _17823, _17824], [33 ^ [], 32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.10.1',plain,[v3_struct_0(32 ^ []), -(v3_struct_0(32 ^ [])), 32 ^ [] = 32 ^ []],extension(19,bind([[_15668, _15669], [32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.10.1.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.10.1.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.10.1.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.10.1.2',plain,[-(32 ^ [] = 32 ^ [])],extension(16,bind([[_14955], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.10.2',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.10.3',plain,[v3_struct_0(32 ^ [])],lemmata('1.1.12.10')).
% 72.11/69.87 cnf('1.1.12.10.4',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.10.5',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.10.6',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.10.7',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.10.7.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.11',plain,[-(v1_funct_1(k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ []))), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), -(v3_struct_0(32 ^ [])), l1_orders_2(32 ^ []), v1_funct_1(33 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(33,bind([[_17825, _17823, _17824], [33 ^ [], 32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.11.1',plain,[v3_struct_0(32 ^ []), -(v3_struct_0(32 ^ [])), 32 ^ [] = 32 ^ []],extension(19,bind([[_15668, _15669], [32 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.11.1.1',plain,[v3_struct_0(32 ^ []), l1_orders_2(32 ^ []), v1_lattice3(32 ^ [])],extension(25,bind([[_16555], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.11.1.1.1',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.11.1.1.2',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.11.1.2',plain,[-(32 ^ [] = 32 ^ [])],extension(16,bind([[_14955], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.11.2',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.11.3',plain,[v3_struct_0(32 ^ [])],lemmata('1.1.12.11')).
% 72.11/69.87 cnf('1.1.12.11.4',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.11.5',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.11.6',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.11.7',plain,[-(m1_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ []))],extension(42,bind([[_20030, _20028, _20029], [33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.11.7.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.12',plain,[-(v1_waybel34(k1_waybel34(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [], k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ [])), 32 ^ [], k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []))), v1_waybel34(k2_waybel_1(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [], k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), k2_waybel_1(32 ^ [], 32 ^ [], 33 ^ []) = k1_waybel34(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [], k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ [])), 32 ^ [] = 32 ^ [], k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []) = k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])],extension(18,bind([[_15353, _15354, _15355, _15356, _15357, _15358], [k2_waybel_1(32 ^ [], 32 ^ [], 33 ^ []), k1_waybel34(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [], k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ [])), 32 ^ [], 32 ^ [], k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.12.1',plain,[-(v1_waybel34(k2_waybel_1(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [], k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])))],extension(13)).
% 72.11/69.87 cnf('1.1.12.12.2',plain,[-(k2_waybel_1(32 ^ [], 32 ^ [], 33 ^ []) = k1_waybel34(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [], k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ []))), k1_waybel34(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [], k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ [])) = k2_waybel_1(32 ^ [], 32 ^ [], 33 ^ [])],extension(17,bind([[_14961, _14962], [k1_waybel34(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [], k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ [])), k2_waybel_1(32 ^ [], 32 ^ [], 33 ^ [])]]))).
% 72.11/69.87 cnf('1.1.12.12.2.1',plain,[-(k1_waybel34(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []), 32 ^ [], k3_waybel_1(32 ^ [], 32 ^ [], 33 ^ [])) = k2_waybel_1(32 ^ [], 32 ^ [], 33 ^ [])), m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v7_waybel_1(33 ^ [], 32 ^ []), v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])), v1_funct_1(33 ^ []), v2_orders_2(32 ^ []), v3_orders_2(32 ^ []), v4_orders_2(32 ^ []), v1_lattice3(32 ^ []), v2_lattice3(32 ^ []), v3_lattice3(32 ^ []), l1_orders_2(32 ^ [])],extension(45,bind([[_20158, _20143], [33 ^ [], 32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.12.2.1.1',plain,[-(m2_relset_1(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(12)).
% 72.11/69.87 cnf('1.1.12.12.2.1.2',plain,[-(v7_waybel_1(33 ^ [], 32 ^ []))],extension(11)).
% 72.11/69.87 cnf('1.1.12.12.2.1.3',plain,[-(v1_funct_2(33 ^ [], u1_struct_0(32 ^ []), u1_struct_0(32 ^ [])))],extension(10)).
% 72.11/69.87 cnf('1.1.12.12.2.1.4',plain,[-(v1_funct_1(33 ^ []))],extension(9)).
% 72.11/69.87 cnf('1.1.12.12.2.1.5',plain,[-(v2_orders_2(32 ^ []))],extension(1)).
% 72.11/69.87 cnf('1.1.12.12.2.1.6',plain,[-(v3_orders_2(32 ^ []))],extension(2)).
% 72.11/69.87 cnf('1.1.12.12.2.1.7',plain,[-(v4_orders_2(32 ^ []))],extension(3)).
% 72.11/69.87 cnf('1.1.12.12.2.1.8',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.12.2.1.9',plain,[-(v2_lattice3(32 ^ []))],extension(5)).
% 72.11/69.87 cnf('1.1.12.12.2.1.10',plain,[-(v3_lattice3(32 ^ []))],extension(6)).
% 72.11/69.87 cnf('1.1.12.12.2.1.11',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 cnf('1.1.12.12.3',plain,[-(32 ^ [] = 32 ^ [])],extension(16,bind([[_14955], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.12.4',plain,[-(k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ []) = k2_yellow_2(32 ^ [], 32 ^ [], 33 ^ [])), 32 ^ [] = 32 ^ [], 32 ^ [] = 32 ^ [], 33 ^ [] = 33 ^ []],extension(15,bind([[_16083, _16084, _16085, _16086, _16087, _16088], [32 ^ [], 32 ^ [], 32 ^ [], 32 ^ [], 33 ^ [], 33 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.12.4.1',plain,[-(32 ^ [] = 32 ^ [])],extension(16,bind([[_14955], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.12.4.2',plain,[-(32 ^ [] = 32 ^ [])],extension(16,bind([[_14955], [32 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.12.4.3',plain,[-(33 ^ [] = 33 ^ [])],extension(16,bind([[_14955], [33 ^ []]]))).
% 72.11/69.87 cnf('1.1.12.13',plain,[-(v2_orders_2(32 ^ []))],extension(1)).
% 72.11/69.87 cnf('1.1.12.14',plain,[-(v3_orders_2(32 ^ []))],extension(2)).
% 72.11/69.87 cnf('1.1.12.15',plain,[-(v4_orders_2(32 ^ []))],extension(3)).
% 72.11/69.87 cnf('1.1.12.16',plain,[-(v1_lattice3(32 ^ []))],extension(4)).
% 72.11/69.87 cnf('1.1.12.17',plain,[-(v2_lattice3(32 ^ []))],extension(5)).
% 72.11/69.87 cnf('1.1.12.18',plain,[-(v3_lattice3(32 ^ []))],extension(6)).
% 72.11/69.87 cnf('1.1.12.19',plain,[-(v3_waybel_3(32 ^ []))],extension(7)).
% 72.11/69.87 cnf('1.1.12.20',plain,[-(l1_orders_2(32 ^ []))],extension(8)).
% 72.11/69.87 %-----------------------------------------------------
% 72.11/69.87
% 72.11/69.87 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------