WATCH: 0.00 CPU 0.01 WC

WATCH: 2.98 CPU 3.02 WC

WATCH: 6.05 CPU 6.03 WC

WATCH: 9.11 CPU 9.04 WC

WATCH: 12.18 CPU 12.05 WC

WATCH: 15.26 CPU 15.06 WC

WATCH: 18.32 CPU 18.07 WC

WATCH: 21.38 CPU 21.08 WC

WATCH: 24.46 CPU 24.10 WC

WATCH: 27.54 CPU 27.11 WC

/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE063.p is a Theorem
Start of proof for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE063.p
%-----------------------------------------------------
fof(prove_this,conjecture,! [_229672, _229675] : (? [_229683, _229686] : (q1(_229683) & (p1(f(_229686)) => p1(_229683) & (r1(_229686) => r1(_229672) & r1(_229675)))) <= ! [_229740] : q1(f(_229740))) & ! [_229759, _229672, _229675] : (? [_229683, _229686] : (q(_229683, _229686) & p1(_229683)) <= r(_229672, _229675) & ! [_229683] : (s1(_229683) => p1(_229683)) & ! [_229683, _229686] : (r(_229683, _229686) => q(_229683, _229686)) & s1(_229672) & s1(_229759)) & (? [_229740] : ! [_229686] : (r1(_229740) ; p1(_229686)) <= ! [_229683] : ? [_229686] : (p1(_229683) & q1(_229686))) & (? [_229740] : a(_229740, _229740) <= ! [_229683] : ? [_229686] : (a(_229686, _229686) & a(_229683, _229686))) & ! [_229759, _229672, _229675] : (? [_229683, _229686] : (q(_229683, _229686) & p1(_229683)) <= s1(_229759) & ! [_229683] : (s1(_229683) => p1(_229683)) & ! [_229683, _229686] : (r(_229683, _229686) => q(_229683, _229686)) & r(_229672, _229675) & s1(_229672)) & ! [_229759, _229672] : (! [_229686] : (q1(_229686) => p1(_229686)) => ? [_229683] : ((p1(_229683) => p1(_229759)) & (q1(_229683) => p1(_229672)))) & ! [_229759, _229672] : (? [_229683] : ((p1(_229672) <= q1(_229683)) & (p1(_229683) => p1(_229759))) <= ! [_229740] : (p1(_229740) <= q1(_229740))) & ((? [_229683] : b(_229683) <= ! [_229683] : a1(_229683)) <= ? [_229683] : (a1(_229683) => b(_229683))) & (? [_229683] : b(_229683) => ? [_229683] : (b(_229683) ; a1(_229683))) & (? [_229686, _229683] : a(_229683, _229686) <=> ? [_229683, _229686] : a(_229683, _229686)) & (? [_229686] : p1(_229686) <=> ? [_229683] : p1(_229683)) & ? [_229740] : ! [_229683] : ? [_229686] : ((p(_229740, _229686) & p(_229686, _229740) => p(_229686, _229683)) & (? [_230420] : p(_230420, _229686) <= p(_229686, _229683))) & ? [_229683] : ! [_229686] : (p1(_229683) => p1(_229686)) & ! [_229759, _229672] : ? [_229683, _229686] : ((r1(_229686) <= p1(_229683)) => p1(_229759) => r1(_229672)) & (? [_229683] : p1(_229683) => ? [_229686] : p1(_229686)) & (! [_229683] : p(_229683, _229683) <= ! [_229683, _229686] : p(_229683, _229686)) & (a0 ; b0 ; (b0 <=> a0)) & (? [_229740] : (r1(_229740) <= p1(_229740)) <= ! [_229683] : (p1(_229683) => q1(_229683)) & ? [_229686] : (q1(_229686) => r1(_229686))) & ! [_229672] : (! [_229686] : (p(f(_229686), _229686) <= r1(_229686) <= r1(_229672)) => ? [_229683, _229686] : (p(_229683, _229686) & (q(_229683, _229686) <= q(f(_229672), _229672)))) & ! [_229759, _229672] : ? [_229683, _229686] : ((p(_229683, _229759) <= q1(_229683)) & q1(_229759) & q1(_229672) & r1(_229759) & r1(_229672) & s1(_229759) & (p(_229683, _229686) <= s1(_229759)) & (r1(_229686) => p(_229672, _229686)) => p(_229759, _229672)) & ((b0 <=> a0) <= a0 & b0) & ! [_229759] : (q1(_229759) <= (g0 ; f0) & ! [_229683] : (p1(_229683) & q1(_229683))) & (p1(z) => p1(z)) & (? [_229683] : ! [_229686] : p(_229683, _229686) => ! [_229686] : ? [_229683] : p(_229683, _229686)) & ? [_229686] : (p1(_229686) <= ? [_229683] : p1(_229683)) & ! [_229672] : ((q1(_229672) <= ! [_229686] : (p1(_229686) <= r1(_229686))) <= r1(_229672) & ! [_229683] : (p1(_229683) => q1(_229683))) & ! [_229759, _229672] : (! [_229686] : (q1(_229686) => p1(_229686)) => ? [_229683] : ((q1(_229683) => p1(_229672)) & (p1(_229683) => p1(_229759)))) & (! [_229683, _229686] : (! [_229740] : (a_member_of(_229740, _229686) <=> a_member_of(_229740, _229683)) <=> eq(_229683, _229686)) => ! [_229759, _229672] : (eq(_229759, _229672) => eq(_229672, _229759))) & (? [_229740] : p1(_229740) <= ? [_229683] : p1(_229683)) & (! [_229683] : p1(_229683) => ! [_229686] : p1(_229686) & ! [_229683] : p1(_229683)) & ! [_229759, _229672] : (! [_229683] : p1(_229683) => p1(_229672) & p1(_229759)) & (? [_229683] : (b(_229683) & a1(_229683)) <= ? [_229683] : a1(_229683) & ! [_229683] : b(_229683)) & ~ ? [_229686] : ! [_229683] : (a(_229683, _229686) <=> ~ a(_229683, _229683)) & (! [_229683] : (a1(_229683) => b(_229683)) => ? [_229683] : a1(_229683) => ? [_229683] : b(_229683)) & ((! [_229683] : q1(_229683) <= ! [_229683] : p1(_229683)) <= ! [_229683] : (p1(_229683) => q1(_229683))) & (! [_229683] : p1(_229683) => ? [_229686] : p1(_229686)) & (((b0 ; ~ b0) & (q0 => q0) <= a0) & ? [_229683] : p1(_229683) <= ? [_229683] : p1(_229683)) & (? [_229686] : q1(_229686) & ! [_229683] : p1(_229683) => ? [_229740] : ! [_229686] : (r1(_229740) ; p1(_229686))) & (! [_229759, _229672] : (p1(_229759) & p1(_229672)) <= ! [_229683] : p1(_229683)) & ! [_229759] : ? [_229683, _231673, _231676, _231679, _229686] : (p1(_229759) & e(_229759) & (s(_229683, f(_229683)) ; g(_229683) <= e(_229683)) & (c(f(_231673)) ; g(_231673) <= e(_231673)) & (s(_229759, _229686) => p1(_229686)) => p1(_231676) & g(_231676) ; p1(_231679) & c(_231679)) & (~ ! [_229683] : (b(_229683) <= a1(_229683)) & ! [_229683] : (b(_229683) ; c(_229683) <= a1(_229683)) => ? [_229683] : (c(_229683) & a1(_229683))) & ! [_229672, _229675] : (? [_229683, _229686] : ((p1(f(_229686)) => (r1(_229686) => r1(_229672) & r1(_229675)) & p1(_229683)) & q1(_229683)) <= q1(f(_229672))) & ! [_229675, _229672] : (? [_229683, _229686] : ((p1(f(_229686)) => p1(_229683)) & (r1(_229686) => r1(_229672) & r1(_229675)) & q1(_229683)) <= ! [_229740] : q1(f(_229740))),file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE063.p',prove_this)).

cnf(1, plain, [-(132 ^ [_41400, _41395]), r1(130 ^ []), r1(129 ^ [])], clausify(prove_this)).
cnf(2, plain, [-(132 ^ [_41400, _41395]), -(r1(_41400))], clausify(prove_this)).
cnf(3, plain, [-(131 ^ [_41400, _41395]), p1(_41395)], clausify(prove_this)).
cnf(4, plain, [-(131 ^ [_41400, _41395]), -(p1(f(_41400)))], clausify(prove_this)).
cnf(5, plain, [-(133 ^ []), 131 ^ [_41400, _41395], q1(_41395), 132 ^ [_41400, _41395]], clausify(prove_this)).
cnf(6, plain, [-(133 ^ []), -(q1(f(_41386)))], clausify(prove_this)).
cnf(7, plain, [-(126 ^ [_41152, _41147]), r1(124 ^ []), r1(125 ^ [])], clausify(prove_this)).
cnf(8, plain, [-(126 ^ [_41152, _41147]), -(r1(_41152))], clausify(prove_this)).
cnf(9, plain, [-(127 ^ [_41152, _41147]), p1(_41147), 126 ^ [_41152, _41147]], clausify(prove_this)).
cnf(10, plain, [-(127 ^ [_41152, _41147]), -(p1(f(_41152)))], clausify(prove_this)).
cnf(11, plain, [-(128 ^ []), q1(_41147), 127 ^ [_41152, _41147]], clausify(prove_this)).
cnf(12, plain, [-(128 ^ []), -(q1(f(124 ^ [])))], clausify(prove_this)).
cnf(13, plain, [-(123 ^ []), a1(_32427), -(b(_32427)), -(c(_32427))], clausify(prove_this)).
cnf(14, plain, [-(123 ^ []), b(122 ^ [])], clausify(prove_this)).
cnf(15, plain, [-(123 ^ []), -(a1(122 ^ []))], clausify(prove_this)).
cnf(16, plain, [-(123 ^ []), c(_32627), a1(_32627)], clausify(prove_this)).
cnf(17, plain, [-(121 ^ []), e(_40685), -(c(f(_40685))), -(g(_40685))], clausify(prove_this)).
cnf(18, plain, [-(121 ^ []), s(120 ^ [], _40700), -(p1(_40700))], clausify(prove_this)).
cnf(19, plain, [-(121 ^ []), e(_40680), -(s(_40680, f(_40680))), -(g(_40680))], clausify(prove_this)).
cnf(20, plain, [-(121 ^ []), -(e(120 ^ []))], clausify(prove_this)).
cnf(21, plain, [-(121 ^ []), -(p1(120 ^ []))], clausify(prove_this)).
cnf(22, plain, [-(121 ^ []), p1(_40695), c(_40695)], clausify(prove_this)).
cnf(23, plain, [-(121 ^ []), p1(_40690), g(_40690)], clausify(prove_this)).
cnf(24, plain, [-(119 ^ []), p1(117 ^ []), p1(118 ^ [])], clausify(prove_this)).
cnf(25, plain, [-(119 ^ []), -(p1(_30385))], clausify(prove_this)).
cnf(26, plain, [-(116 ^ []), p1(115 ^ [_30170])], clausify(prove_this)).
cnf(27, plain, [-(116 ^ []), -(p1(_30086))], clausify(prove_this)).
cnf(28, plain, [-(111 ^ []), q0], clausify(prove_this)).
cnf(29, plain, [-(111 ^ []), -(q0)], clausify(prove_this)).
cnf(30, plain, [-(110 ^ []), -(b0)], clausify(prove_this)).
cnf(31, plain, [-(110 ^ []), b0], clausify(prove_this)).
cnf(32, plain, [-(112 ^ []), 110 ^ [], 111 ^ []], clausify(prove_this)).
cnf(33, plain, [-(113 ^ []), p1(_29889), 112 ^ []], clausify(prove_this)).
cnf(34, plain, [-(113 ^ []), -(p1(109 ^ []))], clausify(prove_this)).
cnf(35, plain, [-(108 ^ []), p1(_29530)], clausify(prove_this)).
cnf(36, plain, [-(108 ^ []), -(p1(_29461))], clausify(prove_this)).
cnf(37, plain, [-(107 ^ []), p1(_29139), -(q1(_29139))], clausify(prove_this)).
cnf(38, plain, [-(107 ^ []), q1(106 ^ [])], clausify(prove_this)).
cnf(39, plain, [-(107 ^ []), -(p1(_29275))], clausify(prove_this)).
cnf(40, plain, [-(105 ^ []), a1(_28815), -(b(_28815))], clausify(prove_this)).
cnf(41, plain, [-(105 ^ []), b(_29021)], clausify(prove_this)).
cnf(42, plain, [-(105 ^ []), -(a1(104 ^ []))], clausify(prove_this)).
cnf(43, plain, [-(103 ^ []), -(a(_39985, 102 ^ [])), -(a(_39985, _39985))], clausify(prove_this)).
cnf(44, plain, [-(103 ^ []), a(_39985, 102 ^ []), a(_39985, _39985)], clausify(prove_this)).
cnf(45, plain, [-(101 ^ []), b(_28381), a1(_28381)], clausify(prove_this)).
cnf(46, plain, [-(101 ^ []), -(b(_28297))], clausify(prove_this)).
cnf(47, plain, [-(101 ^ []), -(a1(100 ^ []))], clausify(prove_this)).
cnf(48, plain, [-(99 ^ []), p1(98 ^ []), p1(97 ^ [])], clausify(prove_this)).
cnf(49, plain, [-(99 ^ []), -(p1(_39808))], clausify(prove_this)).
cnf(50, plain, [-(96 ^ []), p1(94 ^ []), p1(95 ^ [])], clausify(prove_this)).
cnf(51, plain, [-(96 ^ []), -(p1(_27643))], clausify(prove_this)).
cnf(52, plain, [-(93 ^ []), p1(_27540)], clausify(prove_this)).
cnf(53, plain, [-(93 ^ []), -(p1(92 ^ []))], clausify(prove_this)).
cnf(54, plain, [-(88 ^ [_26888, _26832]), -(a_member_of(_26953, _26888)), a_member_of(_26953, _26832)], clausify(prove_this)).
cnf(55, plain, [-(88 ^ [_26888, _26832]), a_member_of(_26953, _26888), -(a_member_of(_26953, _26832))], clausify(prove_this)).
cnf(56, plain, [-(87 ^ [_26888, _26832]), a_member_of(85 ^ [_26888, _26832], _26888)], clausify(prove_this)).
cnf(57, plain, [-(87 ^ [_26888, _26832]), -(a_member_of(85 ^ [_26888, _26832], _26832))], clausify(prove_this)).
cnf(58, plain, [-(86 ^ [_26888, _26832]), a_member_of(85 ^ [_26888, _26832], _26832)], clausify(prove_this)).
cnf(59, plain, [-(86 ^ [_26888, _26832]), -(a_member_of(85 ^ [_26888, _26832], _26888))], clausify(prove_this)).
cnf(60, plain, [-(91 ^ []), eq(_26832, _26888), 88 ^ [_26888, _26832]], clausify(prove_this)).
cnf(61, plain, [-(91 ^ []), -(eq(_26832, _26888)), 86 ^ [_26888, _26832], 87 ^ [_26888, _26832]], clausify(prove_this)).
cnf(62, plain, [-(91 ^ []), eq(90 ^ [], 89 ^ [])], clausify(prove_this)).
cnf(63, plain, [-(91 ^ []), -(eq(89 ^ [], 90 ^ []))], clausify(prove_this)).
cnf(64, plain, [-(83 ^ [_39138]), p1(80 ^ [])], clausify(prove_this)).
cnf(65, plain, [-(83 ^ [_39138]), -(p1(_39138))], clausify(prove_this)).
cnf(66, plain, [-(82 ^ [_39138]), p1(81 ^ [])], clausify(prove_this)).
cnf(67, plain, [-(82 ^ [_39138]), -(q1(_39138))], clausify(prove_this)).
cnf(68, plain, [-(84 ^ []), 82 ^ [_39138], 83 ^ [_39138]], clausify(prove_this)).
cnf(69, plain, [-(84 ^ []), q1(_39126), -(p1(_39126))], clausify(prove_this)).
cnf(70, plain, [-(79 ^ []), r1(_38931), -(p1(_38931))], clausify(prove_this)).
cnf(71, plain, [-(79 ^ []), q1(78 ^ [])], clausify(prove_this)).
cnf(72, plain, [-(79 ^ []), p1(_38916), -(q1(_38916))], clausify(prove_this)).
cnf(73, plain, [-(79 ^ []), -(r1(78 ^ []))], clausify(prove_this)).
cnf(74, plain, [-(77 ^ []), p1(_25581)], clausify(prove_this)).
cnf(75, plain, [-(77 ^ []), -(p1(76 ^ [_25581]))], clausify(prove_this)).
cnf(76, plain, [-(75 ^ []), p(_38790, 74 ^ [])], clausify(prove_this)).
cnf(77, plain, [-(75 ^ []), -(p(73 ^ [], _38748))], clausify(prove_this)).
cnf(78, plain, [-(72 ^ []), p1(z)], clausify(prove_this)).
cnf(79, plain, [-(72 ^ []), -(p1(z))], clausify(prove_this)).
cnf(80, plain, [-(71 ^ []), -(q1(_38594))], clausify(prove_this)).
cnf(81, plain, [-(71 ^ []), q1(70 ^ [])], clausify(prove_this)).
cnf(82, plain, [-(68 ^ []), b0], clausify(prove_this)).
cnf(83, plain, [-(67 ^ []), a0], clausify(prove_this)).
cnf(84, plain, [-(69 ^ []), 67 ^ [], 68 ^ []], clausify(prove_this)).
cnf(85, plain, [-(69 ^ []), -(b0)], clausify(prove_this)).
cnf(86, plain, [-(69 ^ []), -(a0)], clausify(prove_this)).
cnf(87, plain, [-(66 ^ []), s1(64 ^ []), -(p(_38251, _38256))], clausify(prove_this)).
cnf(88, plain, [-(66 ^ []), -(s1(64 ^ []))], clausify(prove_this)).
cnf(89, plain, [-(66 ^ []), p(64 ^ [], 65 ^ [])], clausify(prove_this)).
cnf(90, plain, [-(62 ^ [_37996, _37991]), q(_37991, _37996)], clausify(prove_this)).
cnf(91, plain, [-(62 ^ [_37996, _37991]), -(q(f(60 ^ []), 60 ^ []))], clausify(prove_this)).
cnf(92, plain, [-(61 ^ [_37971]), r1(_37971)], clausify(prove_this)).
cnf(93, plain, [-(61 ^ [_37971]), -(r1(60 ^ []))], clausify(prove_this)).
cnf(94, plain, [-(63 ^ []), p(_37991, _37996), 62 ^ [_37996, _37991]], clausify(prove_this)).
cnf(95, plain, [-(63 ^ []), 61 ^ [_37971], -(p(f(_37971), _37971))], clausify(prove_this)).
cnf(96, plain, [-(59 ^ []), q1(58 ^ []), -(r1(58 ^ []))], clausify(prove_this)).
cnf(97, plain, [-(59 ^ []), p1(_22444), -(q1(_22444))], clausify(prove_this)).
cnf(98, plain, [-(59 ^ []), r1(_22713)], clausify(prove_this)).
cnf(99, plain, [-(59 ^ []), -(p1(_22713))], clausify(prove_this)).
cnf(100, plain, [-(56 ^ []), -(a0)], clausify(prove_this)).
cnf(101, plain, [-(55 ^ []), -(b0)], clausify(prove_this)).
cnf(102, plain, [-(57 ^ []), 55 ^ [], 56 ^ []], clausify(prove_this)).
cnf(103, plain, [-(57 ^ []), b0], clausify(prove_this)).
cnf(104, plain, [-(57 ^ []), a0], clausify(prove_this)).
cnf(105, plain, [-(54 ^ []), p(53 ^ [], 53 ^ [])], clausify(prove_this)).
cnf(106, plain, [-(54 ^ []), -(p(_22036, _22075))], clausify(prove_this)).
cnf(107, plain, [-(52 ^ []), p1(_21933)], clausify(prove_this)).
cnf(108, plain, [-(52 ^ []), -(p1(51 ^ []))], clausify(prove_this)).
cnf(109, plain, [-(50 ^ []), p1(_37517), -(r1(_37522))], clausify(prove_this)).
cnf(110, plain, [-(50 ^ []), r1(49 ^ [])], clausify(prove_this)).
cnf(111, plain, [-(50 ^ []), -(p1(48 ^ []))], clausify(prove_this)).
cnf(112, plain, [-(47 ^ []), p1(46 ^ [_21190])], clausify(prove_this)).
cnf(113, plain, [-(47 ^ []), -(p1(_21190))], clausify(prove_this)).
cnf(114, plain, [-(45 ^ [_37267, _20542]), p(_37296, _37267)], clausify(prove_this)).
cnf(115, plain, [-(45 ^ [_37267, _20542]), -(p(_37267, 43 ^ [_20542]))], clausify(prove_this)).
cnf(116, plain, [-(44 ^ [_37267, _20542]), p(_37267, 43 ^ [_20542])], clausify(prove_this)).
cnf(117, plain, [-(44 ^ [_37267, _20542]), -(p(_37267, _20542))], clausify(prove_this)).
cnf(118, plain, [-(44 ^ [_37267, _20542]), -(p(_20542, _37267))], clausify(prove_this)).
cnf(119, plain, [-(42 ^ []), p1(_20379)], clausify(prove_this)).
cnf(120, plain, [-(42 ^ []), -(p1(41 ^ []))], clausify(prove_this)).
cnf(121, plain, [-(40 ^ []), p1(_20448)], clausify(prove_this)).
cnf(122, plain, [-(40 ^ []), -(p1(39 ^ []))], clausify(prove_this)).
cnf(123, plain, [-(38 ^ []), a(_20100, _20060)], clausify(prove_this)).
cnf(124, plain, [-(38 ^ []), -(a(36 ^ [], 37 ^ []))], clausify(prove_this)).
cnf(125, plain, [-(35 ^ []), a(_20202, _20242)], clausify(prove_this)).
cnf(126, plain, [-(35 ^ []), -(a(34 ^ [], 33 ^ []))], clausify(prove_this)).
cnf(127, plain, [-(32 ^ []), b(_19898)], clausify(prove_this)).
cnf(128, plain, [-(32 ^ []), -(b(31 ^ []))], clausify(prove_this)).
cnf(129, plain, [-(30 ^ []), a1(29 ^ []), -(b(29 ^ []))], clausify(prove_this)).
cnf(130, plain, [-(30 ^ []), b(_19710)], clausify(prove_this)).
cnf(131, plain, [-(30 ^ []), -(a1(_19641))], clausify(prove_this)).
cnf(132, plain, [-(27 ^ [_36568]), p1(24 ^ [])], clausify(prove_this)).
cnf(133, plain, [-(27 ^ [_36568]), -(p1(_36568))], clausify(prove_this)).
cnf(134, plain, [-(26 ^ [_36568]), p1(25 ^ [])], clausify(prove_this)).
cnf(135, plain, [-(26 ^ [_36568]), -(q1(_36568))], clausify(prove_this)).
cnf(136, plain, [-(28 ^ []), 26 ^ [_36568], 27 ^ [_36568]], clausify(prove_this)).
cnf(137, plain, [-(28 ^ []), q1(_36556), -(p1(_36556))], clausify(prove_this)).
cnf(138, plain, [-(22 ^ [_36339]), p1(20 ^ [])], clausify(prove_this)).
cnf(139, plain, [-(22 ^ [_36339]), -(q1(_36339))], clausify(prove_this)).
cnf(140, plain, [-(21 ^ [_36339]), p1(19 ^ [])], clausify(prove_this)).
cnf(141, plain, [-(21 ^ [_36339]), -(p1(_36339))], clausify(prove_this)).
cnf(142, plain, [-(23 ^ []), 21 ^ [_36339], 22 ^ [_36339]], clausify(prove_this)).
cnf(143, plain, [-(23 ^ []), q1(_36327), -(p1(_36327))], clausify(prove_this)).
cnf(144, plain, [-(18 ^ []), r(_36056, _36061), -(q(_36056, _36061))], clausify(prove_this)).
cnf(145, plain, [-(18 ^ []), -(s1(16 ^ []))], clausify(prove_this)).
cnf(146, plain, [-(18 ^ []), -(r(16 ^ [], 17 ^ []))], clausify(prove_this)).
cnf(147, plain, [-(18 ^ []), s1(_36041), -(p1(_36041))], clausify(prove_this)).
cnf(148, plain, [-(18 ^ []), q(_36081, _36086), p1(_36081)], clausify(prove_this)).
cnf(149, plain, [-(14 ^ []), a(_17010, _17010)], clausify(prove_this)).
cnf(150, plain, [-(14 ^ []), -(a(13 ^ [_16782], 13 ^ [_16782]))], clausify(prove_this)).
cnf(151, plain, [-(12 ^ []), p1(11 ^ [_16567])], clausify(prove_this)).
cnf(152, plain, [-(12 ^ []), -(p1(_16385))], clausify(prove_this)).
cnf(153, plain, [-(9 ^ []), r(_35409, _35414), -(q(_35409, _35414))], clausify(prove_this)).
cnf(154, plain, [-(9 ^ []), -(s1(7 ^ []))], clausify(prove_this)).
cnf(155, plain, [-(9 ^ []), s1(_35394), -(p1(_35394))], clausify(prove_this)).
cnf(156, plain, [-(9 ^ []), -(r(7 ^ [], 8 ^ []))], clausify(prove_this)).
cnf(157, plain, [-(9 ^ []), q(_35428, _35433), p1(_35428)], clausify(prove_this)).
cnf(158, plain, [-(3 ^ [_35024, _35019]), r1(1 ^ []), r1(2 ^ [])], clausify(prove_this)).
cnf(159, plain, [-(3 ^ [_35024, _35019]), -(r1(_35024))], clausify(prove_this)).
cnf(160, plain, [-(4 ^ [_35024, _35019]), p1(_35019), 3 ^ [_35024, _35019]], clausify(prove_this)).
cnf(161, plain, [-(4 ^ [_35024, _35019]), -(p1(f(_35024)))], clausify(prove_this)).
cnf(162, plain, [-(5 ^ []), q1(_35019), 4 ^ [_35024, _35019]], clausify(prove_this)).
cnf(163, plain, [-(5 ^ []), -(q1(f(_35010)))], clausify(prove_this)).
cnf(164, plain, [5 ^ [], 9 ^ [], 12 ^ [], 14 ^ [], 18 ^ [], 23 ^ [], 28 ^ [], 30 ^ [], 32 ^ [], 38 ^ [], 35 ^ [], 42 ^ [], 40 ^ [], 45 ^ [_37267, _20542], 44 ^ [_37267, _20542], 47 ^ [], 50 ^ [], 52 ^ [], 54 ^ [], 57 ^ [], 59 ^ [], 63 ^ [], 66 ^ [], 69 ^ [], 71 ^ [], 72 ^ [], 75 ^ [], 77 ^ [], 79 ^ [], 84 ^ [], 91 ^ [], 93 ^ [], 96 ^ [], 99 ^ [], 101 ^ [], 103 ^ [], 105 ^ [], 107 ^ [], 108 ^ [], 113 ^ [], 116 ^ [], 119 ^ [], 133 ^ [], 128 ^ [], 123 ^ [], 121 ^ []], clausify(prove_this)).

cnf('1',plain,[5 ^ [], 9 ^ [], 12 ^ [], 14 ^ [], 18 ^ [], 23 ^ [], 28 ^ [], 30 ^ [], 32 ^ [], 38 ^ [], 35 ^ [], 42 ^ [], 40 ^ [], 45 ^ [43 ^ [_61675], _61675], 44 ^ [43 ^ [_61675], _61675], 47 ^ [], 50 ^ [], 52 ^ [], 54 ^ [], 57 ^ [], 59 ^ [], 63 ^ [], 66 ^ [], 69 ^ [], 71 ^ [], 72 ^ [], 75 ^ [], 77 ^ [], 79 ^ [], 84 ^ [], 91 ^ [], 93 ^ [], 96 ^ [], 99 ^ [], 101 ^ [], 103 ^ [], 105 ^ [], 107 ^ [], 108 ^ [], 113 ^ [], 116 ^ [], 119 ^ [], 133 ^ [], 128 ^ [], 123 ^ [], 121 ^ []],start(164,bind([[_37267, _20542], [43 ^ [_61675], _61675]]))).
cnf('1.1',plain,[-(5 ^ []), q1(f(1 ^ [])), 4 ^ [1 ^ [], f(1 ^ [])]],extension(162,bind([[_35024, _35019], [1 ^ [], f(1 ^ [])]]))).
cnf('1.1.1',plain,[-(q1(f(1 ^ []))), -(5 ^ [])],extension(163,bind([[_35010], [1 ^ []]]))).
cnf('1.1.1.1',plain,[5 ^ []],reduction('1')).
cnf('1.1.2',plain,[-(4 ^ [1 ^ [], f(1 ^ [])]), p1(f(1 ^ [])), 3 ^ [1 ^ [], f(1 ^ [])]],extension(160,bind([[_35024, _35019], [1 ^ [], f(1 ^ [])]]))).
cnf('1.1.2.1',plain,[-(p1(f(1 ^ []))), -(4 ^ [1 ^ [], f(1 ^ [])])],extension(161,bind([[_35024, _35019], [1 ^ [], f(1 ^ [])]]))).
cnf('1.1.2.1.1',plain,[4 ^ [1 ^ [], f(1 ^ [])]],reduction('1.1')).
cnf('1.1.2.2',plain,[-(3 ^ [1 ^ [], f(1 ^ [])]), r1(1 ^ []), r1(2 ^ [])],extension(158,bind([[_35024, _35019], [1 ^ [], f(1 ^ [])]]))).
cnf('1.1.2.2.1',plain,[-(r1(1 ^ [])), -(3 ^ [1 ^ [], f(1 ^ [])])],extension(159,bind([[_35024, _35019], [1 ^ [], f(1 ^ [])]]))).
cnf('1.1.2.2.1.1',plain,[3 ^ [1 ^ [], f(1 ^ [])]],reduction('1.1.2')).
cnf('1.1.2.2.2',plain,[-(r1(2 ^ [])), -(3 ^ [2 ^ [], f(1 ^ [])])],extension(159,bind([[_35024, _35019], [2 ^ [], f(1 ^ [])]]))).
cnf('1.1.2.2.2.1',plain,[3 ^ [2 ^ [], f(1 ^ [])], -(4 ^ [2 ^ [], f(1 ^ [])]), p1(f(1 ^ []))],extension(160,bind([[_35024, _35019], [2 ^ [], f(1 ^ [])]]))).
cnf('1.1.2.2.2.1.1',plain,[4 ^ [2 ^ [], f(1 ^ [])], -(5 ^ []), q1(f(1 ^ []))],extension(162,bind([[_35024, _35019], [2 ^ [], f(1 ^ [])]]))).
cnf('1.1.2.2.2.1.1.1',plain,[5 ^ []],reduction('1')).
cnf('1.1.2.2.2.1.1.2',plain,[-(q1(f(1 ^ []))), -(5 ^ [])],extension(163,bind([[_35010], [1 ^ []]]))).
cnf('1.1.2.2.2.1.1.2.1',plain,[5 ^ []],lemmata('1.1.2.2.2.1.1')).
cnf('1.1.2.2.2.1.2',plain,[-(p1(f(1 ^ []))), -(4 ^ [1 ^ [], f(1 ^ [])])],extension(161,bind([[_35024, _35019], [1 ^ [], f(1 ^ [])]]))).
cnf('1.1.2.2.2.1.2.1',plain,[4 ^ [1 ^ [], f(1 ^ [])]],reduction('1.1')).
cnf('1.2',plain,[-(9 ^ []), r(7 ^ [], 8 ^ []), -(q(7 ^ [], 8 ^ []))],extension(153,bind([[_35409, _35414], [7 ^ [], 8 ^ []]]))).
cnf('1.2.1',plain,[-(r(7 ^ [], 8 ^ [])), -(9 ^ [])],extension(156)).
cnf('1.2.1.1',plain,[9 ^ []],reduction('1')).
cnf('1.2.2',plain,[q(7 ^ [], 8 ^ []), -(9 ^ []), p1(7 ^ [])],extension(157,bind([[_35433, _35428], [8 ^ [], 7 ^ []]]))).
cnf('1.2.2.1',plain,[9 ^ []],reduction('1')).
cnf('1.2.2.2',plain,[-(p1(7 ^ [])), -(9 ^ []), s1(7 ^ [])],extension(155,bind([[_35394], [7 ^ []]]))).
cnf('1.2.2.2.1',plain,[9 ^ []],lemmata('1.2.2')).
cnf('1.2.2.2.2',plain,[-(s1(7 ^ [])), -(9 ^ [])],extension(154)).
cnf('1.2.2.2.2.1',plain,[9 ^ []],lemmata('1.2.2.2')).
cnf('1.3',plain,[-(12 ^ []), p1(11 ^ [_62397])],extension(151,bind([[_16567], [_62397]]))).
cnf('1.3.1',plain,[-(p1(11 ^ [_62397])), -(12 ^ [])],extension(152,bind([[_16385], [11 ^ [_62397]]]))).
cnf('1.3.1.1',plain,[12 ^ []],reduction('1')).
cnf('1.4',plain,[-(14 ^ []), a(13 ^ [_62475], 13 ^ [_62475])],extension(149,bind([[_17010], [13 ^ [_62475]]]))).
cnf('1.4.1',plain,[-(a(13 ^ [_62475], 13 ^ [_62475])), -(14 ^ [])],extension(150,bind([[_16782], [_62475]]))).
cnf('1.4.1.1',plain,[14 ^ []],reduction('1')).
cnf('1.5',plain,[-(18 ^ []), r(16 ^ [], 17 ^ []), -(q(16 ^ [], 17 ^ []))],extension(144,bind([[_36056, _36061], [16 ^ [], 17 ^ []]]))).
cnf('1.5.1',plain,[-(r(16 ^ [], 17 ^ [])), -(18 ^ [])],extension(146)).
cnf('1.5.1.1',plain,[18 ^ []],reduction('1')).
cnf('1.5.2',plain,[q(16 ^ [], 17 ^ []), -(18 ^ []), p1(16 ^ [])],extension(148,bind([[_36086, _36081], [17 ^ [], 16 ^ []]]))).
cnf('1.5.2.1',plain,[18 ^ []],reduction('1')).
cnf('1.5.2.2',plain,[-(p1(16 ^ [])), -(18 ^ []), s1(16 ^ [])],extension(147,bind([[_36041], [16 ^ []]]))).
cnf('1.5.2.2.1',plain,[18 ^ []],lemmata('1.5.2')).
cnf('1.5.2.2.2',plain,[-(s1(16 ^ [])), -(18 ^ [])],extension(145)).
cnf('1.5.2.2.2.1',plain,[18 ^ []],lemmata('1.5.2.2')).
cnf('1.6',plain,[-(23 ^ []), 21 ^ [19 ^ []], 22 ^ [19 ^ []]],extension(142,bind([[_36339], [19 ^ []]]))).
cnf('1.6.1',plain,[-(21 ^ [19 ^ []]), p1(19 ^ [])],extension(140,bind([[_36339], [19 ^ []]]))).
cnf('1.6.1.1',plain,[-(p1(19 ^ [])), -(21 ^ [19 ^ []])],extension(141,bind([[_36339], [19 ^ []]]))).
cnf('1.6.1.1.1',plain,[21 ^ [19 ^ []]],reduction('1.6')).
cnf('1.6.2',plain,[-(22 ^ [19 ^ []]), p1(20 ^ [])],extension(138,bind([[_36339], [19 ^ []]]))).
cnf('1.6.2.1',plain,[-(p1(20 ^ [])), -(21 ^ [20 ^ []])],extension(141,bind([[_36339], [20 ^ []]]))).
cnf('1.6.2.1.1',plain,[21 ^ [20 ^ []], -(23 ^ []), 22 ^ [20 ^ []]],extension(142,bind([[_36339], [20 ^ []]]))).
cnf('1.6.2.1.1.1',plain,[23 ^ []],reduction('1')).
cnf('1.6.2.1.1.2',plain,[-(22 ^ [20 ^ []]), -(q1(20 ^ []))],extension(139,bind([[_36339], [20 ^ []]]))).
cnf('1.6.2.1.1.2.1',plain,[q1(20 ^ []), -(23 ^ []), -(p1(20 ^ []))],extension(143,bind([[_36327], [20 ^ []]]))).
cnf('1.6.2.1.1.2.1.1',plain,[23 ^ []],lemmata('1.6.2.1.1')).
cnf('1.6.2.1.1.2.1.2',plain,[p1(20 ^ [])],reduction('1.6.2')).
cnf('1.7',plain,[-(28 ^ []), 26 ^ [24 ^ []], 27 ^ [24 ^ []]],extension(136,bind([[_36568], [24 ^ []]]))).
cnf('1.7.1',plain,[-(26 ^ [24 ^ []]), p1(25 ^ [])],extension(134,bind([[_36568], [24 ^ []]]))).
cnf('1.7.1.1',plain,[-(p1(25 ^ [])), -(27 ^ [25 ^ []])],extension(133,bind([[_36568], [25 ^ []]]))).
cnf('1.7.1.1.1',plain,[27 ^ [25 ^ []], -(28 ^ []), 26 ^ [25 ^ []]],extension(136,bind([[_36568], [25 ^ []]]))).
cnf('1.7.1.1.1.1',plain,[28 ^ []],reduction('1')).
cnf('1.7.1.1.1.2',plain,[-(26 ^ [25 ^ []]), -(q1(25 ^ []))],extension(135,bind([[_36568], [25 ^ []]]))).
cnf('1.7.1.1.1.2.1',plain,[q1(25 ^ []), -(28 ^ []), -(p1(25 ^ []))],extension(137,bind([[_36556], [25 ^ []]]))).
cnf('1.7.1.1.1.2.1.1',plain,[28 ^ []],lemmata('1.7.1.1.1')).
cnf('1.7.1.1.1.2.1.2',plain,[p1(25 ^ [])],reduction('1.7.1')).
cnf('1.7.2',plain,[-(27 ^ [24 ^ []]), p1(24 ^ [])],extension(132,bind([[_36568], [24 ^ []]]))).
cnf('1.7.2.1',plain,[-(p1(24 ^ [])), -(27 ^ [24 ^ []])],extension(133,bind([[_36568], [24 ^ []]]))).
cnf('1.7.2.1.1',plain,[27 ^ [24 ^ []]],reduction('1.7')).
cnf('1.8',plain,[-(30 ^ []), a1(29 ^ []), -(b(29 ^ []))],extension(129)).
cnf('1.8.1',plain,[-(a1(29 ^ [])), -(30 ^ [])],extension(131,bind([[_19641], [29 ^ []]]))).
cnf('1.8.1.1',plain,[30 ^ []],reduction('1')).
cnf('1.8.2',plain,[b(29 ^ []), -(30 ^ [])],extension(130,bind([[_19710], [29 ^ []]]))).
cnf('1.8.2.1',plain,[30 ^ []],reduction('1')).
cnf('1.9',plain,[-(32 ^ []), b(31 ^ [])],extension(127,bind([[_19898], [31 ^ []]]))).
cnf('1.9.1',plain,[-(b(31 ^ [])), -(32 ^ [])],extension(128)).
cnf('1.9.1.1',plain,[32 ^ []],reduction('1')).
cnf('1.10',plain,[-(38 ^ []), a(36 ^ [], 37 ^ [])],extension(123,bind([[_20100, _20060], [36 ^ [], 37 ^ []]]))).
cnf('1.10.1',plain,[-(a(36 ^ [], 37 ^ [])), -(38 ^ [])],extension(124)).
cnf('1.10.1.1',plain,[38 ^ []],reduction('1')).
cnf('1.11',plain,[-(35 ^ []), a(34 ^ [], 33 ^ [])],extension(125,bind([[_20202, _20242], [34 ^ [], 33 ^ []]]))).
cnf('1.11.1',plain,[-(a(34 ^ [], 33 ^ [])), -(35 ^ [])],extension(126)).
cnf('1.11.1.1',plain,[35 ^ []],reduction('1')).
cnf('1.12',plain,[-(42 ^ []), p1(41 ^ [])],extension(119,bind([[_20379], [41 ^ []]]))).
cnf('1.12.1',plain,[-(p1(41 ^ [])), -(42 ^ [])],extension(120)).
cnf('1.12.1.1',plain,[42 ^ []],reduction('1')).
cnf('1.13',plain,[-(40 ^ []), p1(39 ^ [])],extension(121,bind([[_20448], [39 ^ []]]))).
cnf('1.13.1',plain,[-(p1(39 ^ [])), -(40 ^ [])],extension(122)).
cnf('1.13.1.1',plain,[40 ^ []],reduction('1')).
cnf('1.14',plain,[-(45 ^ [43 ^ [_61675], _61675]), p(73 ^ [], 43 ^ [_61675])],extension(114,bind([[_20542, _37296, _37267], [_61675, 73 ^ [], 43 ^ [_61675]]]))).
cnf('1.14.1',plain,[-(p(73 ^ [], 43 ^ [_61675])), -(75 ^ [])],extension(77,bind([[_38748], [43 ^ [_61675]]]))).
cnf('1.14.1.1',plain,[75 ^ [], 5 ^ [], 9 ^ [], 12 ^ [], 14 ^ [], 18 ^ [], 23 ^ [], 28 ^ [], 30 ^ [], 32 ^ [], 38 ^ [], 35 ^ [], 42 ^ [], 40 ^ [], 45 ^ [43 ^ [_61675], _61675], 44 ^ [43 ^ [_61675], _61675], 47 ^ [], 50 ^ [], 52 ^ [], 54 ^ [], 57 ^ [], 59 ^ [], 63 ^ [], 66 ^ [], 69 ^ [], 71 ^ [], 72 ^ [], 77 ^ [], 79 ^ [], 84 ^ [], 91 ^ [], 93 ^ [], 96 ^ [], 99 ^ [], 101 ^ [], 103 ^ [], 105 ^ [], 107 ^ [], 108 ^ [], 113 ^ [], 116 ^ [], 119 ^ [], 133 ^ [], 128 ^ [], 123 ^ [], 121 ^ []],extension(164,bind([[_37267, _20542], [43 ^ [_61675], _61675]]))).
cnf('1.14.1.1.1',plain,[-(5 ^ [])],lemmata('1')).
cnf('1.14.1.1.2',plain,[-(9 ^ [])],lemmata('1')).
cnf('1.14.1.1.3',plain,[-(12 ^ [])],lemmata('1')).
cnf('1.14.1.1.4',plain,[-(14 ^ [])],lemmata('1')).
cnf('1.14.1.1.5',plain,[-(18 ^ [])],lemmata('1')).
cnf('1.14.1.1.6',plain,[-(23 ^ [])],lemmata('1')).
cnf('1.14.1.1.7',plain,[-(28 ^ [])],lemmata('1')).
cnf('1.14.1.1.8',plain,[-(30 ^ [])],lemmata('1')).
cnf('1.14.1.1.9',plain,[-(32 ^ [])],lemmata('1')).
cnf('1.14.1.1.10',plain,[-(38 ^ [])],lemmata('1')).
cnf('1.14.1.1.11',plain,[-(35 ^ [])],lemmata('1')).
cnf('1.14.1.1.12',plain,[-(42 ^ [])],lemmata('1')).
cnf('1.14.1.1.13',plain,[-(40 ^ [])],lemmata('1')).
cnf('1.14.1.1.14',plain,[-(45 ^ [43 ^ [_61675], _61675]), p(43 ^ [_61675], 43 ^ [_61675])],extension(114,bind([[_20542, _37296, _37267], [_61675, 43 ^ [_61675], 43 ^ [_61675]]]))).
cnf('1.14.1.1.14.1',plain,[-(p(43 ^ [_61675], 43 ^ [_61675])), -(45 ^ [43 ^ [_61675], _61675])],extension(115,bind([[_37267, _20542], [43 ^ [_61675], _61675]]))).
cnf('1.14.1.1.14.1.1',plain,[45 ^ [43 ^ [_61675], _61675]],reduction('1.14.1.1')).
cnf('1.14.1.1.15',plain,[-(44 ^ [43 ^ [_61675], _61675]), p(43 ^ [_61675], 43 ^ [_61675])],extension(116,bind([[_37267, _20542], [43 ^ [_61675], _61675]]))).
cnf('1.14.1.1.15.1',plain,[-(p(43 ^ [_61675], 43 ^ [_61675])), -(45 ^ [43 ^ [_61675], _61675])],extension(115,bind([[_37267, _20542], [43 ^ [_61675], _61675]]))).
cnf('1.14.1.1.15.1.1',plain,[45 ^ [43 ^ [_61675], _61675]],reduction('1')).
cnf('1.14.1.1.16',plain,[-(47 ^ []), p1(46 ^ [_64149])],extension(112,bind([[_21190], [_64149]]))).
cnf('1.14.1.1.16.1',plain,[-(p1(46 ^ [_64149])), -(47 ^ [])],extension(113,bind([[_21190], [46 ^ [_64149]]]))).
cnf('1.14.1.1.16.1.1',plain,[47 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.17',plain,[-(50 ^ []), p1(48 ^ []), -(r1(49 ^ []))],extension(109,bind([[_37517, _37522], [48 ^ [], 49 ^ []]]))).
cnf('1.14.1.1.17.1',plain,[-(p1(48 ^ [])), -(50 ^ [])],extension(111)).
cnf('1.14.1.1.17.1.1',plain,[50 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.17.2',plain,[r1(49 ^ []), -(50 ^ [])],extension(110)).
cnf('1.14.1.1.17.2.1',plain,[50 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.18',plain,[-(52 ^ []), p1(51 ^ [])],extension(107,bind([[_21933], [51 ^ []]]))).
cnf('1.14.1.1.18.1',plain,[-(p1(51 ^ [])), -(52 ^ [])],extension(108)).
cnf('1.14.1.1.18.1.1',plain,[52 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.19',plain,[-(54 ^ []), p(53 ^ [], 53 ^ [])],extension(105)).
cnf('1.14.1.1.19.1',plain,[-(p(53 ^ [], 53 ^ [])), -(54 ^ [])],extension(106,bind([[_22036, _22075], [53 ^ [], 53 ^ []]]))).
cnf('1.14.1.1.19.1.1',plain,[54 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.20',plain,[-(57 ^ []), 55 ^ [], 56 ^ []],extension(102)).
cnf('1.14.1.1.20.1',plain,[-(55 ^ []), -(b0)],extension(101)).
cnf('1.14.1.1.20.1.1',plain,[b0, -(57 ^ [])],extension(103)).
cnf('1.14.1.1.20.1.1.1',plain,[57 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.20.2',plain,[-(56 ^ []), -(a0)],extension(100)).
cnf('1.14.1.1.20.2.1',plain,[a0, -(57 ^ [])],extension(104)).
cnf('1.14.1.1.20.2.1.1',plain,[57 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.21',plain,[-(59 ^ []), q1(58 ^ []), -(r1(58 ^ []))],extension(96)).
cnf('1.14.1.1.21.1',plain,[-(q1(58 ^ [])), -(59 ^ []), p1(58 ^ [])],extension(97,bind([[_22444], [58 ^ []]]))).
cnf('1.14.1.1.21.1.1',plain,[59 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.21.1.2',plain,[-(p1(58 ^ [])), -(59 ^ [])],extension(99,bind([[_22713], [58 ^ []]]))).
cnf('1.14.1.1.21.1.2.1',plain,[59 ^ []],lemmata('1.14.1.1.21.1')).
cnf('1.14.1.1.21.2',plain,[r1(58 ^ []), -(59 ^ [])],extension(98,bind([[_22713], [58 ^ []]]))).
cnf('1.14.1.1.21.2.1',plain,[59 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.22',plain,[-(63 ^ []), p(f(60 ^ []), 60 ^ []), 62 ^ [60 ^ [], f(60 ^ [])]],extension(94,bind([[_37996, _37991], [60 ^ [], f(60 ^ [])]]))).
cnf('1.14.1.1.22.1',plain,[-(p(f(60 ^ []), 60 ^ [])), -(63 ^ []), 61 ^ [60 ^ []]],extension(95,bind([[_37971], [60 ^ []]]))).
cnf('1.14.1.1.22.1.1',plain,[63 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.22.1.2',plain,[-(61 ^ [60 ^ []]), r1(60 ^ [])],extension(92,bind([[_37971], [60 ^ []]]))).
cnf('1.14.1.1.22.1.2.1',plain,[-(r1(60 ^ [])), -(61 ^ [60 ^ []])],extension(93,bind([[_37971], [60 ^ []]]))).
cnf('1.14.1.1.22.1.2.1.1',plain,[61 ^ [60 ^ []]],reduction('1.14.1.1.22.1')).
cnf('1.14.1.1.22.2',plain,[-(62 ^ [60 ^ [], f(60 ^ [])]), q(f(60 ^ []), 60 ^ [])],extension(90,bind([[_37991, _37996], [f(60 ^ []), 60 ^ []]]))).
cnf('1.14.1.1.22.2.1',plain,[-(q(f(60 ^ []), 60 ^ [])), -(62 ^ [60 ^ [], f(60 ^ [])])],extension(91,bind([[_37996, _37991], [60 ^ [], f(60 ^ [])]]))).
cnf('1.14.1.1.22.2.1.1',plain,[62 ^ [60 ^ [], f(60 ^ [])]],reduction('1.14.1.1.22')).
cnf('1.14.1.1.23',plain,[-(66 ^ []), s1(64 ^ []), -(p(73 ^ [], 43 ^ [_61675]))],extension(87,bind([[_38251, _38256], [73 ^ [], 43 ^ [_61675]]]))).
cnf('1.14.1.1.23.1',plain,[-(s1(64 ^ [])), -(66 ^ [])],extension(88)).
cnf('1.14.1.1.23.1.1',plain,[66 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.23.2',plain,[p(73 ^ [], 43 ^ [_61675])],reduction('1.14')).
cnf('1.14.1.1.24',plain,[-(69 ^ []), 67 ^ [], 68 ^ []],extension(84)).
cnf('1.14.1.1.24.1',plain,[-(67 ^ []), a0],extension(83)).
cnf('1.14.1.1.24.1.1',plain,[-(a0), -(69 ^ [])],extension(86)).
cnf('1.14.1.1.24.1.1.1',plain,[69 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.24.2',plain,[-(68 ^ []), b0],extension(82)).
cnf('1.14.1.1.24.2.1',plain,[-(b0), -(69 ^ [])],extension(85)).
cnf('1.14.1.1.24.2.1.1',plain,[69 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.25',plain,[-(71 ^ []), -(q1(70 ^ []))],extension(80,bind([[_38594], [70 ^ []]]))).
cnf('1.14.1.1.25.1',plain,[q1(70 ^ []), -(71 ^ [])],extension(81)).
cnf('1.14.1.1.25.1.1',plain,[71 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.26',plain,[-(72 ^ []), p1(z)],extension(78)).
cnf('1.14.1.1.26.1',plain,[-(p1(z)), -(72 ^ [])],extension(79)).
cnf('1.14.1.1.26.1.1',plain,[72 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.27',plain,[-(77 ^ []), p1(76 ^ [_65186])],extension(74,bind([[_25581], [76 ^ [_65186]]]))).
cnf('1.14.1.1.27.1',plain,[-(p1(76 ^ [_65186])), -(77 ^ [])],extension(75,bind([[_25581], [_65186]]))).
cnf('1.14.1.1.27.1.1',plain,[77 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.28',plain,[-(79 ^ []), r1(78 ^ []), -(p1(78 ^ []))],extension(70,bind([[_38931], [78 ^ []]]))).
cnf('1.14.1.1.28.1',plain,[-(r1(78 ^ [])), -(79 ^ [])],extension(73)).
cnf('1.14.1.1.28.1.1',plain,[79 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.28.2',plain,[p1(78 ^ []), -(79 ^ []), -(q1(78 ^ []))],extension(72,bind([[_38916], [78 ^ []]]))).
cnf('1.14.1.1.28.2.1',plain,[79 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.28.2.2',plain,[q1(78 ^ []), -(79 ^ [])],extension(71)).
cnf('1.14.1.1.28.2.2.1',plain,[79 ^ []],lemmata('1.14.1.1.28.2')).
cnf('1.14.1.1.29',plain,[-(84 ^ []), 82 ^ [80 ^ []], 83 ^ [80 ^ []]],extension(68,bind([[_39138], [80 ^ []]]))).
cnf('1.14.1.1.29.1',plain,[-(82 ^ [80 ^ []]), p1(81 ^ [])],extension(66,bind([[_39138], [80 ^ []]]))).
cnf('1.14.1.1.29.1.1',plain,[-(p1(81 ^ [])), -(83 ^ [81 ^ []])],extension(65,bind([[_39138], [81 ^ []]]))).
cnf('1.14.1.1.29.1.1.1',plain,[83 ^ [81 ^ []], -(84 ^ []), 82 ^ [81 ^ []]],extension(68,bind([[_39138], [81 ^ []]]))).
cnf('1.14.1.1.29.1.1.1.1',plain,[84 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.29.1.1.1.2',plain,[-(82 ^ [81 ^ []]), -(q1(81 ^ []))],extension(67,bind([[_39138], [81 ^ []]]))).
cnf('1.14.1.1.29.1.1.1.2.1',plain,[q1(81 ^ []), -(84 ^ []), -(p1(81 ^ []))],extension(69,bind([[_39126], [81 ^ []]]))).
cnf('1.14.1.1.29.1.1.1.2.1.1',plain,[84 ^ []],lemmata('1.14.1.1.29.1.1.1')).
cnf('1.14.1.1.29.1.1.1.2.1.2',plain,[p1(81 ^ [])],reduction('1.14.1.1.29.1')).
cnf('1.14.1.1.29.2',plain,[-(83 ^ [80 ^ []]), p1(80 ^ [])],extension(64,bind([[_39138], [80 ^ []]]))).
cnf('1.14.1.1.29.2.1',plain,[-(p1(80 ^ [])), -(83 ^ [80 ^ []])],extension(65,bind([[_39138], [80 ^ []]]))).
cnf('1.14.1.1.29.2.1.1',plain,[83 ^ [80 ^ []]],reduction('1.14.1.1.29')).
cnf('1.14.1.1.30',plain,[-(91 ^ []), eq(90 ^ [], 89 ^ []), 88 ^ [89 ^ [], 90 ^ []]],extension(60,bind([[_26888, _26832], [89 ^ [], 90 ^ []]]))).
cnf('1.14.1.1.30.1',plain,[-(eq(90 ^ [], 89 ^ [])), -(91 ^ []), 86 ^ [89 ^ [], 90 ^ []], 87 ^ [89 ^ [], 90 ^ []]],extension(61,bind([[_26888, _26832], [89 ^ [], 90 ^ []]]))).
cnf('1.14.1.1.30.1.1',plain,[91 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.30.1.2',plain,[-(86 ^ [89 ^ [], 90 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])],extension(58,bind([[_26888, _26832], [89 ^ [], 90 ^ []]]))).
cnf('1.14.1.1.30.1.2.1',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])), -(88 ^ [90 ^ [], 89 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])],extension(54,bind([[_26888, _26953, _26832], [90 ^ [], 85 ^ [89 ^ [], 90 ^ []], 89 ^ []]]))).
cnf('1.14.1.1.30.1.2.1.1',plain,[88 ^ [90 ^ [], 89 ^ []], -(91 ^ []), eq(89 ^ [], 90 ^ [])],extension(60,bind([[_26832, _26888], [89 ^ [], 90 ^ []]]))).
cnf('1.14.1.1.30.1.2.1.1.1',plain,[91 ^ []],lemmata('1.14.1.1.30.1')).
cnf('1.14.1.1.30.1.2.1.1.2',plain,[-(eq(89 ^ [], 90 ^ [])), -(91 ^ [])],extension(63)).
cnf('1.14.1.1.30.1.2.1.1.2.1',plain,[91 ^ []],lemmata('1.14.1.1.30.1.2.1.1')).
cnf('1.14.1.1.30.1.2.1.2',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])), -(86 ^ [89 ^ [], 90 ^ []])],extension(59,bind([[_26888, _26832], [89 ^ [], 90 ^ []]]))).
cnf('1.14.1.1.30.1.2.1.2.1',plain,[86 ^ [89 ^ [], 90 ^ []]],reduction('1.14.1.1.30.1')).
cnf('1.14.1.1.30.1.3',plain,[-(87 ^ [89 ^ [], 90 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])],extension(56,bind([[_26832, _26888], [90 ^ [], 89 ^ []]]))).
cnf('1.14.1.1.30.1.3.1',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])), -(88 ^ [90 ^ [], 89 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])],extension(55,bind([[_26832, _26953, _26888], [89 ^ [], 85 ^ [89 ^ [], 90 ^ []], 90 ^ []]]))).
cnf('1.14.1.1.30.1.3.1.1',plain,[88 ^ [90 ^ [], 89 ^ []], -(91 ^ []), eq(89 ^ [], 90 ^ [])],extension(60,bind([[_26832, _26888], [89 ^ [], 90 ^ []]]))).
cnf('1.14.1.1.30.1.3.1.1.1',plain,[91 ^ []],lemmata('1.14.1.1.30.1')).
cnf('1.14.1.1.30.1.3.1.1.2',plain,[-(eq(89 ^ [], 90 ^ [])), -(91 ^ [])],extension(63)).
cnf('1.14.1.1.30.1.3.1.1.2.1',plain,[91 ^ []],lemmata('1.14.1.1.30.1.3.1.1')).
cnf('1.14.1.1.30.1.3.1.2',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])), -(87 ^ [89 ^ [], 90 ^ []])],extension(57,bind([[_26888, _26832], [89 ^ [], 90 ^ []]]))).
cnf('1.14.1.1.30.1.3.1.2.1',plain,[87 ^ [89 ^ [], 90 ^ []]],reduction('1.14.1.1.30.1')).
cnf('1.14.1.1.30.2',plain,[-(88 ^ [89 ^ [], 90 ^ []]), -(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])), a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])],extension(54,bind([[_26888, _26953, _26832], [89 ^ [], 85 ^ [89 ^ [], 90 ^ []], 90 ^ []]]))).
cnf('1.14.1.1.30.2.1',plain,[a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ []), -(88 ^ [89 ^ [], 90 ^ []]), -(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ []))],extension(55,bind([[_26888, _26953, _26832], [89 ^ [], 85 ^ [89 ^ [], 90 ^ []], 90 ^ []]]))).
cnf('1.14.1.1.30.2.1.1',plain,[88 ^ [89 ^ [], 90 ^ []]],reduction('1.14.1.1.30')).
cnf('1.14.1.1.30.2.1.2',plain,[a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ []), -(86 ^ [89 ^ [], 90 ^ []])],extension(58,bind([[_26888, _26832], [89 ^ [], 90 ^ []]]))).
cnf('1.14.1.1.30.2.1.2.1',plain,[86 ^ [89 ^ [], 90 ^ []], -(91 ^ []), -(eq(90 ^ [], 89 ^ [])), 87 ^ [89 ^ [], 90 ^ []]],extension(61,bind([[_26888, _26832], [89 ^ [], 90 ^ []]]))).
cnf('1.14.1.1.30.2.1.2.1.1',plain,[91 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.30.2.1.2.1.2',plain,[eq(90 ^ [], 89 ^ []), -(91 ^ [])],extension(62)).
cnf('1.14.1.1.30.2.1.2.1.2.1',plain,[91 ^ []],lemmata('1.14.1.1.30.2.1.2.1')).
cnf('1.14.1.1.30.2.1.2.1.3',plain,[-(87 ^ [89 ^ [], 90 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])],extension(56,bind([[_26832, _26888], [90 ^ [], 89 ^ []]]))).
cnf('1.14.1.1.30.2.1.2.1.3.1',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ []))],reduction('1.14.1.1.30.2')).
cnf('1.14.1.1.30.2.2',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])), -(88 ^ [90 ^ [], 89 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])],extension(54,bind([[_26888, _26953, _26832], [90 ^ [], 85 ^ [89 ^ [], 90 ^ []], 89 ^ []]]))).
cnf('1.14.1.1.30.2.2.1',plain,[88 ^ [90 ^ [], 89 ^ []], -(91 ^ []), eq(89 ^ [], 90 ^ [])],extension(60,bind([[_26832, _26888], [89 ^ [], 90 ^ []]]))).
cnf('1.14.1.1.30.2.2.1.1',plain,[91 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.30.2.2.1.2',plain,[-(eq(89 ^ [], 90 ^ [])), -(91 ^ [])],extension(63)).
cnf('1.14.1.1.30.2.2.1.2.1',plain,[91 ^ []],lemmata('1.14.1.1.30.2.2.1')).
cnf('1.14.1.1.30.2.2.2',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])), -(86 ^ [89 ^ [], 90 ^ []])],extension(59,bind([[_26888, _26832], [89 ^ [], 90 ^ []]]))).
cnf('1.14.1.1.30.2.2.2.1',plain,[86 ^ [89 ^ [], 90 ^ []], -(91 ^ []), -(eq(90 ^ [], 89 ^ [])), 87 ^ [89 ^ [], 90 ^ []]],extension(61,bind([[_26888, _26832], [89 ^ [], 90 ^ []]]))).
cnf('1.14.1.1.30.2.2.2.1.1',plain,[91 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.30.2.2.2.1.2',plain,[eq(90 ^ [], 89 ^ []), -(91 ^ [])],extension(62)).
cnf('1.14.1.1.30.2.2.2.1.2.1',plain,[91 ^ []],lemmata('1.14.1.1.30.2.2.2.1')).
cnf('1.14.1.1.30.2.2.2.1.3',plain,[-(87 ^ [89 ^ [], 90 ^ []]), -(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ []))],extension(57,bind([[_26888, _26832], [89 ^ [], 90 ^ []]]))).
cnf('1.14.1.1.30.2.2.2.1.3.1',plain,[a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])],reduction('1.14.1.1.30.2')).
cnf('1.14.1.1.31',plain,[-(93 ^ []), p1(92 ^ [])],extension(52,bind([[_27540], [92 ^ []]]))).
cnf('1.14.1.1.31.1',plain,[-(p1(92 ^ [])), -(93 ^ [])],extension(53)).
cnf('1.14.1.1.31.1.1',plain,[93 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.32',plain,[-(96 ^ []), p1(94 ^ []), p1(95 ^ [])],extension(50)).
cnf('1.14.1.1.32.1',plain,[-(p1(94 ^ [])), -(96 ^ [])],extension(51,bind([[_27643], [94 ^ []]]))).
cnf('1.14.1.1.32.1.1',plain,[96 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.32.2',plain,[-(p1(95 ^ [])), -(96 ^ [])],extension(51,bind([[_27643], [95 ^ []]]))).
cnf('1.14.1.1.32.2.1',plain,[96 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.33',plain,[-(99 ^ []), p1(98 ^ []), p1(97 ^ [])],extension(48)).
cnf('1.14.1.1.33.1',plain,[-(p1(98 ^ [])), -(99 ^ [])],extension(49,bind([[_39808], [98 ^ []]]))).
cnf('1.14.1.1.33.1.1',plain,[99 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.33.2',plain,[-(p1(97 ^ [])), -(99 ^ [])],extension(49,bind([[_39808], [97 ^ []]]))).
cnf('1.14.1.1.33.2.1',plain,[99 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.34',plain,[-(101 ^ []), b(100 ^ []), a1(100 ^ [])],extension(45,bind([[_28381], [100 ^ []]]))).
cnf('1.14.1.1.34.1',plain,[-(b(100 ^ [])), -(101 ^ [])],extension(46,bind([[_28297], [100 ^ []]]))).
cnf('1.14.1.1.34.1.1',plain,[101 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.34.2',plain,[-(a1(100 ^ [])), -(101 ^ [])],extension(47)).
cnf('1.14.1.1.34.2.1',plain,[101 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.35',plain,[-(103 ^ []), -(a(102 ^ [], 102 ^ [])), -(a(102 ^ [], 102 ^ []))],extension(43,bind([[_39985], [102 ^ []]]))).
cnf('1.14.1.1.35.1',plain,[a(102 ^ [], 102 ^ []), -(103 ^ []), a(102 ^ [], 102 ^ [])],extension(44,bind([[_39985], [102 ^ []]]))).
cnf('1.14.1.1.35.1.1',plain,[103 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.35.1.2',plain,[-(a(102 ^ [], 102 ^ []))],reduction('1.14.1.1.35')).
cnf('1.14.1.1.35.2',plain,[a(102 ^ [], 102 ^ [])],lemmata('1.14.1.1.35')).
cnf('1.14.1.1.36',plain,[-(105 ^ []), a1(104 ^ []), -(b(104 ^ []))],extension(40,bind([[_28815], [104 ^ []]]))).
cnf('1.14.1.1.36.1',plain,[-(a1(104 ^ [])), -(105 ^ [])],extension(42)).
cnf('1.14.1.1.36.1.1',plain,[105 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.36.2',plain,[b(104 ^ []), -(105 ^ [])],extension(41,bind([[_29021], [104 ^ []]]))).
cnf('1.14.1.1.36.2.1',plain,[105 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.37',plain,[-(107 ^ []), p1(106 ^ []), -(q1(106 ^ []))],extension(37,bind([[_29139], [106 ^ []]]))).
cnf('1.14.1.1.37.1',plain,[-(p1(106 ^ [])), -(107 ^ [])],extension(39,bind([[_29275], [106 ^ []]]))).
cnf('1.14.1.1.37.1.1',plain,[107 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.37.2',plain,[q1(106 ^ []), -(107 ^ [])],extension(38)).
cnf('1.14.1.1.37.2.1',plain,[107 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.38',plain,[-(108 ^ []), p1(_67125)],extension(35,bind([[_29530], [_67125]]))).
cnf('1.14.1.1.38.1',plain,[-(p1(_67125)), -(108 ^ [])],extension(36,bind([[_29461], [_67125]]))).
cnf('1.14.1.1.38.1.1',plain,[108 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.39',plain,[-(113 ^ []), p1(109 ^ []), 112 ^ []],extension(33,bind([[_29889], [109 ^ []]]))).
cnf('1.14.1.1.39.1',plain,[-(p1(109 ^ [])), -(113 ^ [])],extension(34)).
cnf('1.14.1.1.39.1.1',plain,[113 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.39.2',plain,[-(112 ^ []), 110 ^ [], 111 ^ []],extension(32)).
cnf('1.14.1.1.39.2.1',plain,[-(110 ^ []), -(b0)],extension(30)).
cnf('1.14.1.1.39.2.1.1',plain,[b0, -(110 ^ [])],extension(31)).
cnf('1.14.1.1.39.2.1.1.1',plain,[110 ^ []],reduction('1.14.1.1.39.2')).
cnf('1.14.1.1.39.2.2',plain,[-(111 ^ []), q0],extension(28)).
cnf('1.14.1.1.39.2.2.1',plain,[-(q0), -(111 ^ [])],extension(29)).
cnf('1.14.1.1.39.2.2.1.1',plain,[111 ^ []],reduction('1.14.1.1.39.2')).
cnf('1.14.1.1.40',plain,[-(116 ^ []), p1(115 ^ [_67365])],extension(26,bind([[_30170], [_67365]]))).
cnf('1.14.1.1.40.1',plain,[-(p1(115 ^ [_67365])), -(116 ^ [])],extension(27,bind([[_30086], [115 ^ [_67365]]]))).
cnf('1.14.1.1.40.1.1',plain,[116 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.41',plain,[-(119 ^ []), p1(117 ^ []), p1(118 ^ [])],extension(24)).
cnf('1.14.1.1.41.1',plain,[-(p1(117 ^ [])), -(119 ^ [])],extension(25,bind([[_30385], [117 ^ []]]))).
cnf('1.14.1.1.41.1.1',plain,[119 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.41.2',plain,[-(p1(118 ^ [])), -(119 ^ [])],extension(25,bind([[_30385], [118 ^ []]]))).
cnf('1.14.1.1.41.2.1',plain,[119 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.42',plain,[-(133 ^ []), 131 ^ [130 ^ [], f(130 ^ [])], q1(f(130 ^ [])), 132 ^ [130 ^ [], f(130 ^ [])]],extension(5,bind([[_41400, _41395], [130 ^ [], f(130 ^ [])]]))).
cnf('1.14.1.1.42.1',plain,[-(131 ^ [130 ^ [], f(130 ^ [])]), p1(f(130 ^ []))],extension(3,bind([[_41400, _41395], [130 ^ [], f(130 ^ [])]]))).
cnf('1.14.1.1.42.1.1',plain,[-(p1(f(130 ^ []))), -(131 ^ [130 ^ [], f(130 ^ [])])],extension(4,bind([[_41400, _41395], [130 ^ [], f(130 ^ [])]]))).
cnf('1.14.1.1.42.1.1.1',plain,[131 ^ [130 ^ [], f(130 ^ [])]],reduction('1.14.1.1.42')).
cnf('1.14.1.1.42.2',plain,[-(q1(f(130 ^ []))), -(133 ^ [])],extension(6,bind([[_41386], [130 ^ []]]))).
cnf('1.14.1.1.42.2.1',plain,[133 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.42.3',plain,[-(132 ^ [130 ^ [], f(130 ^ [])]), r1(130 ^ []), r1(129 ^ [])],extension(1,bind([[_41400, _41395], [130 ^ [], f(130 ^ [])]]))).
cnf('1.14.1.1.42.3.1',plain,[-(r1(130 ^ [])), -(132 ^ [130 ^ [], f(130 ^ [])])],extension(2,bind([[_41400, _41395], [130 ^ [], f(130 ^ [])]]))).
cnf('1.14.1.1.42.3.1.1',plain,[132 ^ [130 ^ [], f(130 ^ [])]],reduction('1.14.1.1.42')).
cnf('1.14.1.1.42.3.2',plain,[-(r1(129 ^ [])), -(132 ^ [129 ^ [], f(129 ^ [])])],extension(2,bind([[_41400, _41395], [129 ^ [], f(129 ^ [])]]))).
cnf('1.14.1.1.42.3.2.1',plain,[132 ^ [129 ^ [], f(129 ^ [])], -(133 ^ []), 131 ^ [129 ^ [], f(129 ^ [])], q1(f(129 ^ []))],extension(5,bind([[_41400, _41395], [129 ^ [], f(129 ^ [])]]))).
cnf('1.14.1.1.42.3.2.1.1',plain,[133 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.42.3.2.1.2',plain,[-(131 ^ [129 ^ [], f(129 ^ [])]), p1(f(129 ^ []))],extension(3,bind([[_41400, _41395], [129 ^ [], f(129 ^ [])]]))).
cnf('1.14.1.1.42.3.2.1.2.1',plain,[-(p1(f(129 ^ []))), -(131 ^ [129 ^ [], f(129 ^ [])])],extension(4,bind([[_41400, _41395], [129 ^ [], f(129 ^ [])]]))).
cnf('1.14.1.1.42.3.2.1.2.1.1',plain,[131 ^ [129 ^ [], f(129 ^ [])]],reduction('1.14.1.1.42.3.2.1')).
cnf('1.14.1.1.42.3.2.1.3',plain,[-(q1(f(129 ^ []))), -(133 ^ [])],extension(6,bind([[_41386], [129 ^ []]]))).
cnf('1.14.1.1.42.3.2.1.3.1',plain,[133 ^ []],lemmata('1.14.1.1.42.3.2.1')).
cnf('1.14.1.1.43',plain,[-(128 ^ []), q1(f(124 ^ [])), 127 ^ [124 ^ [], f(124 ^ [])]],extension(11,bind([[_41152, _41147], [124 ^ [], f(124 ^ [])]]))).
cnf('1.14.1.1.43.1',plain,[-(q1(f(124 ^ []))), -(128 ^ [])],extension(12)).
cnf('1.14.1.1.43.1.1',plain,[128 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.43.2',plain,[-(127 ^ [124 ^ [], f(124 ^ [])]), p1(f(124 ^ [])), 126 ^ [124 ^ [], f(124 ^ [])]],extension(9,bind([[_41152, _41147], [124 ^ [], f(124 ^ [])]]))).
cnf('1.14.1.1.43.2.1',plain,[-(p1(f(124 ^ []))), -(127 ^ [124 ^ [], f(124 ^ [])])],extension(10,bind([[_41152, _41147], [124 ^ [], f(124 ^ [])]]))).
cnf('1.14.1.1.43.2.1.1',plain,[127 ^ [124 ^ [], f(124 ^ [])]],reduction('1.14.1.1.43')).
cnf('1.14.1.1.43.2.2',plain,[-(126 ^ [124 ^ [], f(124 ^ [])]), r1(124 ^ []), r1(125 ^ [])],extension(7,bind([[_41152, _41147], [124 ^ [], f(124 ^ [])]]))).
cnf('1.14.1.1.43.2.2.1',plain,[-(r1(124 ^ [])), -(126 ^ [124 ^ [], f(124 ^ [])])],extension(8,bind([[_41152, _41147], [124 ^ [], f(124 ^ [])]]))).
cnf('1.14.1.1.43.2.2.1.1',plain,[126 ^ [124 ^ [], f(124 ^ [])]],reduction('1.14.1.1.43.2')).
cnf('1.14.1.1.43.2.2.2',plain,[-(r1(125 ^ [])), -(126 ^ [125 ^ [], f(124 ^ [])])],extension(8,bind([[_41152, _41147], [125 ^ [], f(124 ^ [])]]))).
cnf('1.14.1.1.43.2.2.2.1',plain,[126 ^ [125 ^ [], f(124 ^ [])], -(127 ^ [125 ^ [], f(124 ^ [])]), p1(f(124 ^ []))],extension(9,bind([[_41152, _41147], [125 ^ [], f(124 ^ [])]]))).
cnf('1.14.1.1.43.2.2.2.1.1',plain,[127 ^ [125 ^ [], f(124 ^ [])], -(128 ^ []), q1(f(124 ^ []))],extension(11,bind([[_41152, _41147], [125 ^ [], f(124 ^ [])]]))).
cnf('1.14.1.1.43.2.2.2.1.1.1',plain,[128 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.43.2.2.2.1.1.2',plain,[-(q1(f(124 ^ []))), -(128 ^ [])],extension(12)).
cnf('1.14.1.1.43.2.2.2.1.1.2.1',plain,[128 ^ []],lemmata('1.14.1.1.43.2.2.2.1.1')).
cnf('1.14.1.1.43.2.2.2.1.2',plain,[-(p1(f(124 ^ [])))],lemmata('1.14.1.1.43.2')).
cnf('1.14.1.1.44',plain,[-(123 ^ []), a1(122 ^ []), -(b(122 ^ [])), -(c(122 ^ []))],extension(13,bind([[_32427], [122 ^ []]]))).
cnf('1.14.1.1.44.1',plain,[-(a1(122 ^ [])), -(123 ^ [])],extension(15)).
cnf('1.14.1.1.44.1.1',plain,[123 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.44.2',plain,[b(122 ^ []), -(123 ^ [])],extension(14)).
cnf('1.14.1.1.44.2.1',plain,[123 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.44.3',plain,[c(122 ^ []), -(123 ^ []), a1(122 ^ [])],extension(16,bind([[_1991], [122 ^ []]]))).
cnf('1.14.1.1.44.3.1',plain,[123 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.44.3.2',plain,[-(a1(122 ^ []))],lemmata('1.14.1.1.44')).
cnf('1.14.1.1.45',plain,[-(121 ^ []), e(120 ^ []), -(c(f(120 ^ []))), -(g(120 ^ []))],extension(17,bind([[_2955], [120 ^ []]]))).
cnf('1.14.1.1.45.1',plain,[-(e(120 ^ [])), -(121 ^ [])],extension(20)).
cnf('1.14.1.1.45.1.1',plain,[121 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.45.2',plain,[c(f(120 ^ [])), -(121 ^ []), p1(f(120 ^ []))],extension(22,bind([[_2957], [f(120 ^ [])]]))).
cnf('1.14.1.1.45.2.1',plain,[121 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.45.2.2',plain,[-(p1(f(120 ^ []))), -(121 ^ []), s(120 ^ [], f(120 ^ []))],extension(18,bind([[_2958], [f(120 ^ [])]]))).
cnf('1.14.1.1.45.2.2.1',plain,[121 ^ []],lemmata('1.14.1.1.45.2')).
cnf('1.14.1.1.45.2.2.2',plain,[-(s(120 ^ [], f(120 ^ []))), -(121 ^ []), e(120 ^ []), -(g(120 ^ []))],extension(19,bind([[_2954], [120 ^ []]]))).
cnf('1.14.1.1.45.2.2.2.1',plain,[121 ^ []],lemmata('1.14.1.1.45.2.2')).
cnf('1.14.1.1.45.2.2.2.2',plain,[-(e(120 ^ []))],lemmata('1.14.1.1.45')).
cnf('1.14.1.1.45.2.2.2.3',plain,[g(120 ^ []), -(121 ^ []), p1(120 ^ [])],extension(23,bind([[_2956], [120 ^ []]]))).
cnf('1.14.1.1.45.2.2.2.3.1',plain,[121 ^ []],lemmata('1.14.1.1.45.2.2.2')).
cnf('1.14.1.1.45.2.2.2.3.2',plain,[-(p1(120 ^ [])), -(121 ^ [])],extension(21)).
cnf('1.14.1.1.45.2.2.2.3.2.1',plain,[121 ^ []],lemmata('1.14.1.1.45.2.2.2.3')).
cnf('1.14.1.1.45.3',plain,[g(120 ^ []), -(121 ^ []), p1(120 ^ [])],extension(23,bind([[_2956], [120 ^ []]]))).
cnf('1.14.1.1.45.3.1',plain,[121 ^ []],reduction('1.14.1.1')).
cnf('1.14.1.1.45.3.2',plain,[-(p1(120 ^ [])), -(121 ^ [])],extension(21)).
cnf('1.14.1.1.45.3.2.1',plain,[121 ^ []],lemmata('1.14.1.1.45.3')).
cnf('1.15',plain,[-(44 ^ [43 ^ [_5470], _5470]), p(43 ^ [_5470], 43 ^ [_5470])],extension(116,bind([[_2353, _1899], [43 ^ [_5470], _5470]]))).
cnf('1.15.1',plain,[-(p(43 ^ [_5470], 43 ^ [_5470])), -(44 ^ [43 ^ [_5470], 43 ^ [_5470]])],extension(117,bind([[_2353, _1899], [43 ^ [_5470], 43 ^ [_5470]]]))).
cnf('1.15.1.1',plain,[44 ^ [43 ^ [_5470], 43 ^ [_5470]], 5 ^ [], 9 ^ [], 12 ^ [], 14 ^ [], 18 ^ [], 23 ^ [], 28 ^ [], 30 ^ [], 32 ^ [], 38 ^ [], 35 ^ [], 42 ^ [], 40 ^ [], 45 ^ [43 ^ [_5470], 43 ^ [_5470]], 47 ^ [], 50 ^ [], 52 ^ [], 54 ^ [], 57 ^ [], 59 ^ [], 63 ^ [], 66 ^ [], 69 ^ [], 71 ^ [], 72 ^ [], 75 ^ [], 77 ^ [], 79 ^ [], 84 ^ [], 91 ^ [], 93 ^ [], 96 ^ [], 99 ^ [], 101 ^ [], 103 ^ [], 105 ^ [], 107 ^ [], 108 ^ [], 113 ^ [], 116 ^ [], 119 ^ [], 133 ^ [], 128 ^ [], 123 ^ [], 121 ^ []],extension(164,bind([[_2353, _1899], [43 ^ [_5470], 43 ^ [_5470]]]))).
cnf('1.15.1.1.1',plain,[-(5 ^ [])],lemmata('1')).
cnf('1.15.1.1.2',plain,[-(9 ^ [])],lemmata('1')).
cnf('1.15.1.1.3',plain,[-(12 ^ [])],lemmata('1')).
cnf('1.15.1.1.4',plain,[-(14 ^ [])],lemmata('1')).
cnf('1.15.1.1.5',plain,[-(18 ^ [])],lemmata('1')).
cnf('1.15.1.1.6',plain,[-(23 ^ [])],lemmata('1')).
cnf('1.15.1.1.7',plain,[-(28 ^ [])],lemmata('1')).
cnf('1.15.1.1.8',plain,[-(30 ^ [])],lemmata('1')).
cnf('1.15.1.1.9',plain,[-(32 ^ [])],lemmata('1')).
cnf('1.15.1.1.10',plain,[-(38 ^ [])],lemmata('1')).
cnf('1.15.1.1.11',plain,[-(35 ^ [])],lemmata('1')).
cnf('1.15.1.1.12',plain,[-(42 ^ [])],lemmata('1')).
cnf('1.15.1.1.13',plain,[-(40 ^ [])],lemmata('1')).
cnf('1.15.1.1.14',plain,[-(45 ^ [43 ^ [_5470], 43 ^ [_5470]]), p(_5470, 43 ^ [_5470])],extension(114,bind([[_1899, _2366, _2353], [43 ^ [_5470], _5470, 43 ^ [_5470]]]))).
cnf('1.15.1.1.14.1',plain,[-(p(_5470, 43 ^ [_5470])), -(44 ^ [43 ^ [_5470], _5470])],extension(118,bind([[_2353, _1899], [43 ^ [_5470], _5470]]))).
cnf('1.15.1.1.14.1.1',plain,[44 ^ [43 ^ [_5470], _5470]],reduction('1')).
cnf('1.15.1.1.15',plain,[-(47 ^ []), p1(46 ^ [_10748])],extension(112,bind([[_1900], [_10748]]))).
cnf('1.15.1.1.15.1',plain,[-(p1(46 ^ [_10748])), -(47 ^ [])],extension(113,bind([[_1900], [46 ^ [_10748]]]))).
cnf('1.15.1.1.15.1.1',plain,[47 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.16',plain,[-(50 ^ []), p1(48 ^ []), -(r1(49 ^ []))],extension(109,bind([[_2410, _2411], [48 ^ [], 49 ^ []]]))).
cnf('1.15.1.1.16.1',plain,[-(p1(48 ^ [])), -(50 ^ [])],extension(111)).
cnf('1.15.1.1.16.1.1',plain,[50 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.16.2',plain,[r1(49 ^ []), -(50 ^ [])],extension(110)).
cnf('1.15.1.1.16.2.1',plain,[50 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.17',plain,[-(52 ^ []), p1(51 ^ [])],extension(107,bind([[_1901], [51 ^ []]]))).
cnf('1.15.1.1.17.1',plain,[-(p1(51 ^ [])), -(52 ^ [])],extension(108)).
cnf('1.15.1.1.17.1.1',plain,[52 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.18',plain,[-(54 ^ []), p(53 ^ [], 53 ^ [])],extension(105)).
cnf('1.15.1.1.18.1',plain,[-(p(53 ^ [], 53 ^ [])), -(54 ^ [])],extension(106,bind([[_1904, _1905], [53 ^ [], 53 ^ []]]))).
cnf('1.15.1.1.18.1.1',plain,[54 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.19',plain,[-(57 ^ []), 55 ^ [], 56 ^ []],extension(102)).
cnf('1.15.1.1.19.1',plain,[-(55 ^ []), -(b0)],extension(101)).
cnf('1.15.1.1.19.1.1',plain,[b0, -(57 ^ [])],extension(103)).
cnf('1.15.1.1.19.1.1.1',plain,[57 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.19.2',plain,[-(56 ^ []), -(a0)],extension(100)).
cnf('1.15.1.1.19.2.1',plain,[a0, -(57 ^ [])],extension(104)).
cnf('1.15.1.1.19.2.1.1',plain,[57 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.20',plain,[-(59 ^ []), q1(58 ^ []), -(r1(58 ^ []))],extension(96)).
cnf('1.15.1.1.20.1',plain,[-(q1(58 ^ [])), -(59 ^ []), p1(58 ^ [])],extension(97,bind([[_1909], [58 ^ []]]))).
cnf('1.15.1.1.20.1.1',plain,[59 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.20.1.2',plain,[-(p1(58 ^ [])), -(59 ^ [])],extension(99,bind([[_1914], [58 ^ []]]))).
cnf('1.15.1.1.20.1.2.1',plain,[59 ^ []],lemmata('1.15.1.1.20.1')).
cnf('1.15.1.1.20.2',plain,[r1(58 ^ []), -(59 ^ [])],extension(98,bind([[_1914], [58 ^ []]]))).
cnf('1.15.1.1.20.2.1',plain,[59 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.21',plain,[-(63 ^ []), p(f(60 ^ []), 60 ^ []), 62 ^ [60 ^ [], f(60 ^ [])]],extension(94,bind([[_2496, _2495], [60 ^ [], f(60 ^ [])]]))).
cnf('1.15.1.1.21.1',plain,[-(p(f(60 ^ []), 60 ^ [])), -(63 ^ []), 61 ^ [60 ^ []]],extension(95,bind([[_2485], [60 ^ []]]))).
cnf('1.15.1.1.21.1.1',plain,[63 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.21.1.2',plain,[-(61 ^ [60 ^ []]), r1(60 ^ [])],extension(92,bind([[_2485], [60 ^ []]]))).
cnf('1.15.1.1.21.1.2.1',plain,[-(r1(60 ^ [])), -(61 ^ [60 ^ []])],extension(93,bind([[_2485], [60 ^ []]]))).
cnf('1.15.1.1.21.1.2.1.1',plain,[61 ^ [60 ^ []]],reduction('1.15.1.1.21.1')).
cnf('1.15.1.1.21.2',plain,[-(62 ^ [60 ^ [], f(60 ^ [])]), q(f(60 ^ []), 60 ^ [])],extension(90,bind([[_2495, _2496], [f(60 ^ []), 60 ^ []]]))).
cnf('1.15.1.1.21.2.1',plain,[-(q(f(60 ^ []), 60 ^ [])), -(62 ^ [60 ^ [], f(60 ^ [])])],extension(91,bind([[_2496, _2495], [60 ^ [], f(60 ^ [])]]))).
cnf('1.15.1.1.21.2.1.1',plain,[62 ^ [60 ^ [], f(60 ^ [])]],reduction('1.15.1.1.21')).
cnf('1.15.1.1.22',plain,[-(66 ^ []), s1(64 ^ []), -(p(43 ^ [_5470], 43 ^ [_5470]))],extension(87,bind([[_2548, _2549], [43 ^ [_5470], 43 ^ [_5470]]]))).
cnf('1.15.1.1.22.1',plain,[-(s1(64 ^ [])), -(66 ^ [])],extension(88)).
cnf('1.15.1.1.22.1.1',plain,[66 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.22.2',plain,[p(43 ^ [_5470], 43 ^ [_5470])],reduction('1.15')).
cnf('1.15.1.1.23',plain,[-(69 ^ []), 67 ^ [], 68 ^ []],extension(84)).
cnf('1.15.1.1.23.1',plain,[-(67 ^ []), a0],extension(83)).
cnf('1.15.1.1.23.1.1',plain,[-(a0), -(69 ^ [])],extension(86)).
cnf('1.15.1.1.23.1.1.1',plain,[69 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.23.2',plain,[-(68 ^ []), b0],extension(82)).
cnf('1.15.1.1.23.2.1',plain,[-(b0), -(69 ^ [])],extension(85)).
cnf('1.15.1.1.23.2.1.1',plain,[69 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.24',plain,[-(71 ^ []), -(q1(70 ^ []))],extension(80,bind([[_2598], [70 ^ []]]))).
cnf('1.15.1.1.24.1',plain,[q1(70 ^ []), -(71 ^ [])],extension(81)).
cnf('1.15.1.1.24.1.1',plain,[71 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.25',plain,[-(72 ^ []), p1(z)],extension(78)).
cnf('1.15.1.1.25.1',plain,[-(p1(z)), -(72 ^ [])],extension(79)).
cnf('1.15.1.1.25.1.1',plain,[72 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.26',plain,[-(75 ^ []), p(73 ^ [], 74 ^ [])],extension(76,bind([[_2629], [73 ^ []]]))).
cnf('1.15.1.1.26.1',plain,[-(p(73 ^ [], 74 ^ [])), -(75 ^ [])],extension(77,bind([[_2621], [74 ^ []]]))).
cnf('1.15.1.1.26.1.1',plain,[75 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.27',plain,[-(77 ^ []), p1(76 ^ [_11476])],extension(74,bind([[_1923], [76 ^ [_11476]]]))).
cnf('1.15.1.1.27.1',plain,[-(p1(76 ^ [_11476])), -(77 ^ [])],extension(75,bind([[_1923], [_11476]]))).
cnf('1.15.1.1.27.1.1',plain,[77 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.28',plain,[-(79 ^ []), r1(78 ^ []), -(p1(78 ^ []))],extension(70,bind([[_2664], [78 ^ []]]))).
cnf('1.15.1.1.28.1',plain,[-(r1(78 ^ [])), -(79 ^ [])],extension(73)).
cnf('1.15.1.1.28.1.1',plain,[79 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.28.2',plain,[p1(78 ^ []), -(79 ^ []), -(q1(78 ^ []))],extension(72,bind([[_2659], [78 ^ []]]))).
cnf('1.15.1.1.28.2.1',plain,[79 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.28.2.2',plain,[q1(78 ^ []), -(79 ^ [])],extension(71)).
cnf('1.15.1.1.28.2.2.1',plain,[79 ^ []],lemmata('1.15.1.1.28.2')).
cnf('1.15.1.1.29',plain,[-(84 ^ []), 82 ^ [80 ^ []], 83 ^ [80 ^ []]],extension(68,bind([[_2692], [80 ^ []]]))).
cnf('1.15.1.1.29.1',plain,[-(82 ^ [80 ^ []]), p1(81 ^ [])],extension(66,bind([[_2692], [80 ^ []]]))).
cnf('1.15.1.1.29.1.1',plain,[-(p1(81 ^ [])), -(83 ^ [81 ^ []])],extension(65,bind([[_2692], [81 ^ []]]))).
cnf('1.15.1.1.29.1.1.1',plain,[83 ^ [81 ^ []], -(84 ^ []), 82 ^ [81 ^ []]],extension(68,bind([[_2692], [81 ^ []]]))).
cnf('1.15.1.1.29.1.1.1.1',plain,[84 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.29.1.1.1.2',plain,[-(82 ^ [81 ^ []]), -(q1(81 ^ []))],extension(67,bind([[_2692], [81 ^ []]]))).
cnf('1.15.1.1.29.1.1.1.2.1',plain,[q1(81 ^ []), -(84 ^ []), -(p1(81 ^ []))],extension(69,bind([[_2687], [81 ^ []]]))).
cnf('1.15.1.1.29.1.1.1.2.1.1',plain,[84 ^ []],lemmata('1.15.1.1.29.1.1.1')).
cnf('1.15.1.1.29.1.1.1.2.1.2',plain,[p1(81 ^ [])],reduction('1.15.1.1.29.1')).
cnf('1.15.1.1.29.2',plain,[-(83 ^ [80 ^ []]), p1(80 ^ [])],extension(64,bind([[_2692], [80 ^ []]]))).
cnf('1.15.1.1.29.2.1',plain,[-(p1(80 ^ [])), -(83 ^ [80 ^ []])],extension(65,bind([[_2692], [80 ^ []]]))).
cnf('1.15.1.1.29.2.1.1',plain,[83 ^ [80 ^ []]],reduction('1.15.1.1.29')).
cnf('1.15.1.1.30',plain,[-(91 ^ []), eq(90 ^ [], 89 ^ []), 88 ^ [89 ^ [], 90 ^ []]],extension(60,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.15.1.1.30.1',plain,[-(eq(90 ^ [], 89 ^ [])), -(91 ^ []), 86 ^ [89 ^ [], 90 ^ []], 87 ^ [89 ^ [], 90 ^ []]],extension(61,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.15.1.1.30.1.1',plain,[91 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.30.1.2',plain,[-(86 ^ [89 ^ [], 90 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])],extension(58,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.15.1.1.30.1.2.1',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])), -(88 ^ [90 ^ [], 89 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])],extension(54,bind([[_1927, _1928, _1926], [90 ^ [], 85 ^ [89 ^ [], 90 ^ []], 89 ^ []]]))).
cnf('1.15.1.1.30.1.2.1.1',plain,[88 ^ [90 ^ [], 89 ^ []], -(91 ^ []), eq(89 ^ [], 90 ^ [])],extension(60,bind([[_1926, _1927], [89 ^ [], 90 ^ []]]))).
cnf('1.15.1.1.30.1.2.1.1.1',plain,[91 ^ []],lemmata('1.15.1.1.30.1')).
cnf('1.15.1.1.30.1.2.1.1.2',plain,[-(eq(89 ^ [], 90 ^ [])), -(91 ^ [])],extension(63)).
cnf('1.15.1.1.30.1.2.1.1.2.1',plain,[91 ^ []],lemmata('1.15.1.1.30.1.2.1.1')).
cnf('1.15.1.1.30.1.2.1.2',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])), -(86 ^ [89 ^ [], 90 ^ []])],extension(59,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.15.1.1.30.1.2.1.2.1',plain,[86 ^ [89 ^ [], 90 ^ []]],reduction('1.15.1.1.30.1')).
cnf('1.15.1.1.30.1.3',plain,[-(87 ^ [89 ^ [], 90 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])],extension(56,bind([[_1926, _1927], [90 ^ [], 89 ^ []]]))).
cnf('1.15.1.1.30.1.3.1',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])), -(88 ^ [90 ^ [], 89 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])],extension(55,bind([[_1926, _1928, _1927], [89 ^ [], 85 ^ [89 ^ [], 90 ^ []], 90 ^ []]]))).
cnf('1.15.1.1.30.1.3.1.1',plain,[88 ^ [90 ^ [], 89 ^ []], -(91 ^ []), eq(89 ^ [], 90 ^ [])],extension(60,bind([[_1926, _1927], [89 ^ [], 90 ^ []]]))).
cnf('1.15.1.1.30.1.3.1.1.1',plain,[91 ^ []],lemmata('1.15.1.1.30.1')).
cnf('1.15.1.1.30.1.3.1.1.2',plain,[-(eq(89 ^ [], 90 ^ [])), -(91 ^ [])],extension(63)).
cnf('1.15.1.1.30.1.3.1.1.2.1',plain,[91 ^ []],lemmata('1.15.1.1.30.1.3.1.1')).
cnf('1.15.1.1.30.1.3.1.2',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])), -(87 ^ [89 ^ [], 90 ^ []])],extension(57,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.15.1.1.30.1.3.1.2.1',plain,[87 ^ [89 ^ [], 90 ^ []]],reduction('1.15.1.1.30.1')).
cnf('1.15.1.1.30.2',plain,[-(88 ^ [89 ^ [], 90 ^ []]), -(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])), a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])],extension(54,bind([[_1927, _1928, _1926], [89 ^ [], 85 ^ [89 ^ [], 90 ^ []], 90 ^ []]]))).
cnf('1.15.1.1.30.2.1',plain,[a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ []), -(88 ^ [89 ^ [], 90 ^ []]), -(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ []))],extension(55,bind([[_1927, _1928, _1926], [89 ^ [], 85 ^ [89 ^ [], 90 ^ []], 90 ^ []]]))).
cnf('1.15.1.1.30.2.1.1',plain,[88 ^ [89 ^ [], 90 ^ []]],reduction('1.15.1.1.30')).
cnf('1.15.1.1.30.2.1.2',plain,[a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ []), -(86 ^ [89 ^ [], 90 ^ []])],extension(58,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.15.1.1.30.2.1.2.1',plain,[86 ^ [89 ^ [], 90 ^ []], -(91 ^ []), -(eq(90 ^ [], 89 ^ [])), 87 ^ [89 ^ [], 90 ^ []]],extension(61,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.15.1.1.30.2.1.2.1.1',plain,[91 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.30.2.1.2.1.2',plain,[eq(90 ^ [], 89 ^ []), -(91 ^ [])],extension(62)).
cnf('1.15.1.1.30.2.1.2.1.2.1',plain,[91 ^ []],lemmata('1.15.1.1.30.2.1.2.1')).
cnf('1.15.1.1.30.2.1.2.1.3',plain,[-(87 ^ [89 ^ [], 90 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])],extension(56,bind([[_1926, _1927], [90 ^ [], 89 ^ []]]))).
cnf('1.15.1.1.30.2.1.2.1.3.1',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ []))],reduction('1.15.1.1.30.2')).
cnf('1.15.1.1.30.2.2',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])), -(88 ^ [90 ^ [], 89 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])],extension(54,bind([[_1927, _1928, _1926], [90 ^ [], 85 ^ [89 ^ [], 90 ^ []], 89 ^ []]]))).
cnf('1.15.1.1.30.2.2.1',plain,[88 ^ [90 ^ [], 89 ^ []], -(91 ^ []), eq(89 ^ [], 90 ^ [])],extension(60,bind([[_1926, _1927], [89 ^ [], 90 ^ []]]))).
cnf('1.15.1.1.30.2.2.1.1',plain,[91 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.30.2.2.1.2',plain,[-(eq(89 ^ [], 90 ^ [])), -(91 ^ [])],extension(63)).
cnf('1.15.1.1.30.2.2.1.2.1',plain,[91 ^ []],lemmata('1.15.1.1.30.2.2.1')).
cnf('1.15.1.1.30.2.2.2',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])), -(86 ^ [89 ^ [], 90 ^ []])],extension(59,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.15.1.1.30.2.2.2.1',plain,[86 ^ [89 ^ [], 90 ^ []], -(91 ^ []), -(eq(90 ^ [], 89 ^ [])), 87 ^ [89 ^ [], 90 ^ []]],extension(61,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.15.1.1.30.2.2.2.1.1',plain,[91 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.30.2.2.2.1.2',plain,[eq(90 ^ [], 89 ^ []), -(91 ^ [])],extension(62)).
cnf('1.15.1.1.30.2.2.2.1.2.1',plain,[91 ^ []],lemmata('1.15.1.1.30.2.2.2.1')).
cnf('1.15.1.1.30.2.2.2.1.3',plain,[-(87 ^ [89 ^ [], 90 ^ []]), -(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ []))],extension(57,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.15.1.1.30.2.2.2.1.3.1',plain,[a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])],reduction('1.15.1.1.30.2')).
cnf('1.15.1.1.31',plain,[-(93 ^ []), p1(92 ^ [])],extension(52,bind([[_1938], [92 ^ []]]))).
cnf('1.15.1.1.31.1',plain,[-(p1(92 ^ [])), -(93 ^ [])],extension(53)).
cnf('1.15.1.1.31.1.1',plain,[93 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.32',plain,[-(96 ^ []), p1(94 ^ []), p1(95 ^ [])],extension(50)).
cnf('1.15.1.1.32.1',plain,[-(p1(94 ^ [])), -(96 ^ [])],extension(51,bind([[_1941], [94 ^ []]]))).
cnf('1.15.1.1.32.1.1',plain,[96 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.32.2',plain,[-(p1(95 ^ [])), -(96 ^ [])],extension(51,bind([[_1941], [95 ^ []]]))).
cnf('1.15.1.1.32.2.1',plain,[96 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.33',plain,[-(99 ^ []), p1(98 ^ []), p1(97 ^ [])],extension(48)).
cnf('1.15.1.1.33.1',plain,[-(p1(98 ^ [])), -(99 ^ [])],extension(49,bind([[_2810], [98 ^ []]]))).
cnf('1.15.1.1.33.1.1',plain,[99 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.33.2',plain,[-(p1(97 ^ [])), -(99 ^ [])],extension(49,bind([[_2810], [97 ^ []]]))).
cnf('1.15.1.1.33.2.1',plain,[99 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.34',plain,[-(101 ^ []), b(100 ^ []), a1(100 ^ [])],extension(45,bind([[_1947], [100 ^ []]]))).
cnf('1.15.1.1.34.1',plain,[-(b(100 ^ [])), -(101 ^ [])],extension(46,bind([[_1944], [100 ^ []]]))).
cnf('1.15.1.1.34.1.1',plain,[101 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.34.2',plain,[-(a1(100 ^ [])), -(101 ^ [])],extension(47)).
cnf('1.15.1.1.34.2.1',plain,[101 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.35',plain,[-(103 ^ []), -(a(102 ^ [], 102 ^ [])), -(a(102 ^ [], 102 ^ []))],extension(43,bind([[_2837], [102 ^ []]]))).
cnf('1.15.1.1.35.1',plain,[a(102 ^ [], 102 ^ []), -(103 ^ []), a(102 ^ [], 102 ^ [])],extension(44,bind([[_2837], [102 ^ []]]))).
cnf('1.15.1.1.35.1.1',plain,[103 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.35.1.2',plain,[-(a(102 ^ [], 102 ^ []))],reduction('1.15.1.1.35')).
cnf('1.15.1.1.35.2',plain,[a(102 ^ [], 102 ^ [])],lemmata('1.15.1.1.35')).
cnf('1.15.1.1.36',plain,[-(105 ^ []), a1(104 ^ []), -(b(104 ^ []))],extension(40,bind([[_1952], [104 ^ []]]))).
cnf('1.15.1.1.36.1',plain,[-(a1(104 ^ [])), -(105 ^ [])],extension(42)).
cnf('1.15.1.1.36.1.1',plain,[105 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.36.2',plain,[b(104 ^ []), -(105 ^ [])],extension(41,bind([[_1957], [104 ^ []]]))).
cnf('1.15.1.1.36.2.1',plain,[105 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.37',plain,[-(107 ^ []), p1(106 ^ []), -(q1(106 ^ []))],extension(37,bind([[_1960], [106 ^ []]]))).
cnf('1.15.1.1.37.1',plain,[-(p1(106 ^ [])), -(107 ^ [])],extension(39,bind([[_1965], [106 ^ []]]))).
cnf('1.15.1.1.37.1.1',plain,[107 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.37.2',plain,[q1(106 ^ []), -(107 ^ [])],extension(38)).
cnf('1.15.1.1.37.2.1',plain,[107 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.38',plain,[-(108 ^ []), p1(_12784)],extension(35,bind([[_1971], [_12784]]))).
cnf('1.15.1.1.38.1',plain,[-(p1(_12784)), -(108 ^ [])],extension(36,bind([[_1968], [_12784]]))).
cnf('1.15.1.1.38.1.1',plain,[108 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.39',plain,[-(113 ^ []), p1(109 ^ []), 112 ^ []],extension(33,bind([[_1974], [109 ^ []]]))).
cnf('1.15.1.1.39.1',plain,[-(p1(109 ^ [])), -(113 ^ [])],extension(34)).
cnf('1.15.1.1.39.1.1',plain,[113 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.39.2',plain,[-(112 ^ []), 110 ^ [], 111 ^ []],extension(32)).
cnf('1.15.1.1.39.2.1',plain,[-(110 ^ []), -(b0)],extension(30)).
cnf('1.15.1.1.39.2.1.1',plain,[b0, -(110 ^ [])],extension(31)).
cnf('1.15.1.1.39.2.1.1.1',plain,[110 ^ []],reduction('1.15.1.1.39.2')).
cnf('1.15.1.1.39.2.2',plain,[-(111 ^ []), q0],extension(28)).
cnf('1.15.1.1.39.2.2.1',plain,[-(q0), -(111 ^ [])],extension(29)).
cnf('1.15.1.1.39.2.2.1.1',plain,[111 ^ []],reduction('1.15.1.1.39.2')).
cnf('1.15.1.1.40',plain,[-(116 ^ []), p1(115 ^ [_12942])],extension(26,bind([[_1980], [_12942]]))).
cnf('1.15.1.1.40.1',plain,[-(p1(115 ^ [_12942])), -(116 ^ [])],extension(27,bind([[_1977], [115 ^ [_12942]]]))).
cnf('1.15.1.1.40.1.1',plain,[116 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.41',plain,[-(119 ^ []), p1(117 ^ []), p1(118 ^ [])],extension(24)).
cnf('1.15.1.1.41.1',plain,[-(p1(117 ^ [])), -(119 ^ [])],extension(25,bind([[_1981], [117 ^ []]]))).
cnf('1.15.1.1.41.1.1',plain,[119 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.41.2',plain,[-(p1(118 ^ [])), -(119 ^ [])],extension(25,bind([[_1981], [118 ^ []]]))).
cnf('1.15.1.1.41.2.1',plain,[119 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.42',plain,[-(133 ^ []), 131 ^ [130 ^ [], f(130 ^ [])], q1(f(130 ^ [])), 132 ^ [130 ^ [], f(130 ^ [])]],extension(5,bind([[_3079, _3078], [130 ^ [], f(130 ^ [])]]))).
cnf('1.15.1.1.42.1',plain,[-(131 ^ [130 ^ [], f(130 ^ [])]), p1(f(130 ^ []))],extension(3,bind([[_3079, _3078], [130 ^ [], f(130 ^ [])]]))).
cnf('1.15.1.1.42.1.1',plain,[-(p1(f(130 ^ []))), -(131 ^ [130 ^ [], f(130 ^ [])])],extension(4,bind([[_3079, _3078], [130 ^ [], f(130 ^ [])]]))).
cnf('1.15.1.1.42.1.1.1',plain,[131 ^ [130 ^ [], f(130 ^ [])]],reduction('1.15.1.1.42')).
cnf('1.15.1.1.42.2',plain,[-(q1(f(130 ^ []))), -(133 ^ [])],extension(6,bind([[_3073], [130 ^ []]]))).
cnf('1.15.1.1.42.2.1',plain,[133 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.42.3',plain,[-(132 ^ [130 ^ [], f(130 ^ [])]), r1(130 ^ []), r1(129 ^ [])],extension(1,bind([[_3079, _3078], [130 ^ [], f(130 ^ [])]]))).
cnf('1.15.1.1.42.3.1',plain,[-(r1(130 ^ [])), -(132 ^ [130 ^ [], f(130 ^ [])])],extension(2,bind([[_3079, _3078], [130 ^ [], f(130 ^ [])]]))).
cnf('1.15.1.1.42.3.1.1',plain,[132 ^ [130 ^ [], f(130 ^ [])]],reduction('1.15.1.1.42')).
cnf('1.15.1.1.42.3.2',plain,[-(r1(129 ^ [])), -(132 ^ [129 ^ [], f(129 ^ [])])],extension(2,bind([[_3079, _3078], [129 ^ [], f(129 ^ [])]]))).
cnf('1.15.1.1.42.3.2.1',plain,[132 ^ [129 ^ [], f(129 ^ [])], -(133 ^ []), 131 ^ [129 ^ [], f(129 ^ [])], q1(f(129 ^ []))],extension(5,bind([[_3079, _3078], [129 ^ [], f(129 ^ [])]]))).
cnf('1.15.1.1.42.3.2.1.1',plain,[133 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.42.3.2.1.2',plain,[-(131 ^ [129 ^ [], f(129 ^ [])]), p1(f(129 ^ []))],extension(3,bind([[_3079, _3078], [129 ^ [], f(129 ^ [])]]))).
cnf('1.15.1.1.42.3.2.1.2.1',plain,[-(p1(f(129 ^ []))), -(131 ^ [129 ^ [], f(129 ^ [])])],extension(4,bind([[_3079, _3078], [129 ^ [], f(129 ^ [])]]))).
cnf('1.15.1.1.42.3.2.1.2.1.1',plain,[131 ^ [129 ^ [], f(129 ^ [])]],reduction('1.15.1.1.42.3.2.1')).
cnf('1.15.1.1.42.3.2.1.3',plain,[-(q1(f(129 ^ []))), -(133 ^ [])],extension(6,bind([[_3073], [129 ^ []]]))).
cnf('1.15.1.1.42.3.2.1.3.1',plain,[133 ^ []],lemmata('1.15.1.1.42.3.2.1')).
cnf('1.15.1.1.43',plain,[-(128 ^ []), q1(f(124 ^ [])), 127 ^ [124 ^ [], f(124 ^ [])]],extension(11,bind([[_3028, _3027], [124 ^ [], f(124 ^ [])]]))).
cnf('1.15.1.1.43.1',plain,[-(q1(f(124 ^ []))), -(128 ^ [])],extension(12)).
cnf('1.15.1.1.43.1.1',plain,[128 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.43.2',plain,[-(127 ^ [124 ^ [], f(124 ^ [])]), p1(f(124 ^ [])), 126 ^ [124 ^ [], f(124 ^ [])]],extension(9,bind([[_3028, _3027], [124 ^ [], f(124 ^ [])]]))).
cnf('1.15.1.1.43.2.1',plain,[-(p1(f(124 ^ []))), -(127 ^ [124 ^ [], f(124 ^ [])])],extension(10,bind([[_3028, _3027], [124 ^ [], f(124 ^ [])]]))).
cnf('1.15.1.1.43.2.1.1',plain,[127 ^ [124 ^ [], f(124 ^ [])]],reduction('1.15.1.1.43')).
cnf('1.15.1.1.43.2.2',plain,[-(126 ^ [124 ^ [], f(124 ^ [])]), r1(124 ^ []), r1(125 ^ [])],extension(7,bind([[_3028, _3027], [124 ^ [], f(124 ^ [])]]))).
cnf('1.15.1.1.43.2.2.1',plain,[-(r1(124 ^ [])), -(126 ^ [124 ^ [], f(124 ^ [])])],extension(8,bind([[_3028, _3027], [124 ^ [], f(124 ^ [])]]))).
cnf('1.15.1.1.43.2.2.1.1',plain,[126 ^ [124 ^ [], f(124 ^ [])]],reduction('1.15.1.1.43.2')).
cnf('1.15.1.1.43.2.2.2',plain,[-(r1(125 ^ [])), -(126 ^ [125 ^ [], f(124 ^ [])])],extension(8,bind([[_3028, _3027], [125 ^ [], f(124 ^ [])]]))).
cnf('1.15.1.1.43.2.2.2.1',plain,[126 ^ [125 ^ [], f(124 ^ [])], -(127 ^ [125 ^ [], f(124 ^ [])]), p1(f(124 ^ []))],extension(9,bind([[_3028, _3027], [125 ^ [], f(124 ^ [])]]))).
cnf('1.15.1.1.43.2.2.2.1.1',plain,[127 ^ [125 ^ [], f(124 ^ [])], -(128 ^ []), q1(f(124 ^ []))],extension(11,bind([[_3028, _3027], [125 ^ [], f(124 ^ [])]]))).
cnf('1.15.1.1.43.2.2.2.1.1.1',plain,[128 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.43.2.2.2.1.1.2',plain,[-(q1(f(124 ^ []))), -(128 ^ [])],extension(12)).
cnf('1.15.1.1.43.2.2.2.1.1.2.1',plain,[128 ^ []],lemmata('1.15.1.1.43.2.2.2.1.1')).
cnf('1.15.1.1.43.2.2.2.1.2',plain,[-(p1(f(124 ^ [])))],lemmata('1.15.1.1.43.2')).
cnf('1.15.1.1.44',plain,[-(123 ^ []), a1(122 ^ []), -(b(122 ^ [])), -(c(122 ^ []))],extension(13,bind([[_1984], [122 ^ []]]))).
cnf('1.15.1.1.44.1',plain,[-(a1(122 ^ [])), -(123 ^ [])],extension(15)).
cnf('1.15.1.1.44.1.1',plain,[123 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.44.2',plain,[b(122 ^ []), -(123 ^ [])],extension(14)).
cnf('1.15.1.1.44.2.1',plain,[123 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.44.3',plain,[c(122 ^ []), -(123 ^ []), a1(122 ^ [])],extension(16,bind([[_1991], [122 ^ []]]))).
cnf('1.15.1.1.44.3.1',plain,[123 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.44.3.2',plain,[-(a1(122 ^ []))],lemmata('1.15.1.1.44')).
cnf('1.15.1.1.45',plain,[-(121 ^ []), e(120 ^ []), -(c(f(120 ^ []))), -(g(120 ^ []))],extension(17,bind([[_2955], [120 ^ []]]))).
cnf('1.15.1.1.45.1',plain,[-(e(120 ^ [])), -(121 ^ [])],extension(20)).
cnf('1.15.1.1.45.1.1',plain,[121 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.45.2',plain,[c(f(120 ^ [])), -(121 ^ []), p1(f(120 ^ []))],extension(22,bind([[_2957], [f(120 ^ [])]]))).
cnf('1.15.1.1.45.2.1',plain,[121 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.45.2.2',plain,[-(p1(f(120 ^ []))), -(121 ^ []), s(120 ^ [], f(120 ^ []))],extension(18,bind([[_2958], [f(120 ^ [])]]))).
cnf('1.15.1.1.45.2.2.1',plain,[121 ^ []],lemmata('1.15.1.1.45.2')).
cnf('1.15.1.1.45.2.2.2',plain,[-(s(120 ^ [], f(120 ^ []))), -(121 ^ []), e(120 ^ []), -(g(120 ^ []))],extension(19,bind([[_2954], [120 ^ []]]))).
cnf('1.15.1.1.45.2.2.2.1',plain,[121 ^ []],lemmata('1.15.1.1.45.2.2')).
cnf('1.15.1.1.45.2.2.2.2',plain,[-(e(120 ^ []))],lemmata('1.15.1.1.45')).
cnf('1.15.1.1.45.2.2.2.3',plain,[g(120 ^ []), -(121 ^ []), p1(120 ^ [])],extension(23,bind([[_2956], [120 ^ []]]))).
cnf('1.15.1.1.45.2.2.2.3.1',plain,[121 ^ []],lemmata('1.15.1.1.45.2.2.2')).
cnf('1.15.1.1.45.2.2.2.3.2',plain,[-(p1(120 ^ [])), -(121 ^ [])],extension(21)).
cnf('1.15.1.1.45.2.2.2.3.2.1',plain,[121 ^ []],lemmata('1.15.1.1.45.2.2.2.3')).
cnf('1.15.1.1.45.3',plain,[g(120 ^ []), -(121 ^ []), p1(120 ^ [])],extension(23,bind([[_2956], [120 ^ []]]))).
cnf('1.15.1.1.45.3.1',plain,[121 ^ []],reduction('1.15.1.1')).
cnf('1.15.1.1.45.3.2',plain,[-(p1(120 ^ [])), -(121 ^ [])],extension(21)).
cnf('1.15.1.1.45.3.2.1',plain,[121 ^ []],lemmata('1.15.1.1.45.3')).
cnf('1.16',plain,[-(47 ^ []), p1(46 ^ [_13856])],extension(112,bind([[_1900], [_13856]]))).
cnf('1.16.1',plain,[-(p1(46 ^ [_13856])), -(47 ^ [])],extension(113,bind([[_1900], [46 ^ [_13856]]]))).
cnf('1.16.1.1',plain,[47 ^ []],reduction('1')).
cnf('1.17',plain,[-(50 ^ []), p1(48 ^ []), -(r1(49 ^ []))],extension(109,bind([[_2410, _2411], [48 ^ [], 49 ^ []]]))).
cnf('1.17.1',plain,[-(p1(48 ^ [])), -(50 ^ [])],extension(111)).
cnf('1.17.1.1',plain,[50 ^ []],reduction('1')).
cnf('1.17.2',plain,[r1(49 ^ []), -(50 ^ [])],extension(110)).
cnf('1.17.2.1',plain,[50 ^ []],reduction('1')).
cnf('1.18',plain,[-(52 ^ []), p1(51 ^ [])],extension(107,bind([[_1901], [51 ^ []]]))).
cnf('1.18.1',plain,[-(p1(51 ^ [])), -(52 ^ [])],extension(108)).
cnf('1.18.1.1',plain,[52 ^ []],reduction('1')).
cnf('1.19',plain,[-(54 ^ []), p(53 ^ [], 53 ^ [])],extension(105)).
cnf('1.19.1',plain,[-(p(53 ^ [], 53 ^ [])), -(54 ^ [])],extension(106,bind([[_1904, _1905], [53 ^ [], 53 ^ []]]))).
cnf('1.19.1.1',plain,[54 ^ []],reduction('1')).
cnf('1.20',plain,[-(57 ^ []), 55 ^ [], 56 ^ []],extension(102)).
cnf('1.20.1',plain,[-(55 ^ []), -(b0)],extension(101)).
cnf('1.20.1.1',plain,[b0, -(57 ^ [])],extension(103)).
cnf('1.20.1.1.1',plain,[57 ^ []],reduction('1')).
cnf('1.20.2',plain,[-(56 ^ []), -(a0)],extension(100)).
cnf('1.20.2.1',plain,[a0, -(57 ^ [])],extension(104)).
cnf('1.20.2.1.1',plain,[57 ^ []],reduction('1')).
cnf('1.21',plain,[-(59 ^ []), q1(58 ^ []), -(r1(58 ^ []))],extension(96)).
cnf('1.21.1',plain,[-(q1(58 ^ [])), -(59 ^ []), p1(58 ^ [])],extension(97,bind([[_1909], [58 ^ []]]))).
cnf('1.21.1.1',plain,[59 ^ []],reduction('1')).
cnf('1.21.1.2',plain,[-(p1(58 ^ [])), -(59 ^ [])],extension(99,bind([[_1914], [58 ^ []]]))).
cnf('1.21.1.2.1',plain,[59 ^ []],lemmata('1.21.1')).
cnf('1.21.2',plain,[r1(58 ^ []), -(59 ^ [])],extension(98,bind([[_1914], [58 ^ []]]))).
cnf('1.21.2.1',plain,[59 ^ []],reduction('1')).
cnf('1.22',plain,[-(63 ^ []), p(f(60 ^ []), 60 ^ []), 62 ^ [60 ^ [], f(60 ^ [])]],extension(94,bind([[_2496, _2495], [60 ^ [], f(60 ^ [])]]))).
cnf('1.22.1',plain,[-(p(f(60 ^ []), 60 ^ [])), -(63 ^ []), 61 ^ [60 ^ []]],extension(95,bind([[_2485], [60 ^ []]]))).
cnf('1.22.1.1',plain,[63 ^ []],reduction('1')).
cnf('1.22.1.2',plain,[-(61 ^ [60 ^ []]), r1(60 ^ [])],extension(92,bind([[_2485], [60 ^ []]]))).
cnf('1.22.1.2.1',plain,[-(r1(60 ^ [])), -(61 ^ [60 ^ []])],extension(93,bind([[_2485], [60 ^ []]]))).
cnf('1.22.1.2.1.1',plain,[61 ^ [60 ^ []]],reduction('1.22.1')).
cnf('1.22.2',plain,[-(62 ^ [60 ^ [], f(60 ^ [])]), q(f(60 ^ []), 60 ^ [])],extension(90,bind([[_2495, _2496], [f(60 ^ []), 60 ^ []]]))).
cnf('1.22.2.1',plain,[-(q(f(60 ^ []), 60 ^ [])), -(62 ^ [60 ^ [], f(60 ^ [])])],extension(91,bind([[_2496, _2495], [60 ^ [], f(60 ^ [])]]))).
cnf('1.22.2.1.1',plain,[62 ^ [60 ^ [], f(60 ^ [])]],reduction('1.22')).
cnf('1.23',plain,[-(66 ^ []), s1(64 ^ []), -(p(64 ^ [], 65 ^ []))],extension(87,bind([[_2548, _2549], [64 ^ [], 65 ^ []]]))).
cnf('1.23.1',plain,[-(s1(64 ^ [])), -(66 ^ [])],extension(88)).
cnf('1.23.1.1',plain,[66 ^ []],reduction('1')).
cnf('1.23.2',plain,[p(64 ^ [], 65 ^ []), -(66 ^ [])],extension(89)).
cnf('1.23.2.1',plain,[66 ^ []],reduction('1')).
cnf('1.24',plain,[-(69 ^ []), 67 ^ [], 68 ^ []],extension(84)).
cnf('1.24.1',plain,[-(67 ^ []), a0],extension(83)).
cnf('1.24.1.1',plain,[-(a0), -(69 ^ [])],extension(86)).
cnf('1.24.1.1.1',plain,[69 ^ []],reduction('1')).
cnf('1.24.2',plain,[-(68 ^ []), b0],extension(82)).
cnf('1.24.2.1',plain,[-(b0), -(69 ^ [])],extension(85)).
cnf('1.24.2.1.1',plain,[69 ^ []],reduction('1')).
cnf('1.25',plain,[-(71 ^ []), -(q1(70 ^ []))],extension(80,bind([[_2598], [70 ^ []]]))).
cnf('1.25.1',plain,[q1(70 ^ []), -(71 ^ [])],extension(81)).
cnf('1.25.1.1',plain,[71 ^ []],reduction('1')).
cnf('1.26',plain,[-(72 ^ []), p1(z)],extension(78)).
cnf('1.26.1',plain,[-(p1(z)), -(72 ^ [])],extension(79)).
cnf('1.26.1.1',plain,[72 ^ []],reduction('1')).
cnf('1.27',plain,[-(75 ^ []), p(73 ^ [], 74 ^ [])],extension(76,bind([[_2629], [73 ^ []]]))).
cnf('1.27.1',plain,[-(p(73 ^ [], 74 ^ [])), -(75 ^ [])],extension(77,bind([[_2621], [74 ^ []]]))).
cnf('1.27.1.1',plain,[75 ^ []],reduction('1')).
cnf('1.28',plain,[-(77 ^ []), p1(76 ^ [_14603])],extension(74,bind([[_1923], [76 ^ [_14603]]]))).
cnf('1.28.1',plain,[-(p1(76 ^ [_14603])), -(77 ^ [])],extension(75,bind([[_1923], [_14603]]))).
cnf('1.28.1.1',plain,[77 ^ []],reduction('1')).
cnf('1.29',plain,[-(79 ^ []), r1(78 ^ []), -(p1(78 ^ []))],extension(70,bind([[_2664], [78 ^ []]]))).
cnf('1.29.1',plain,[-(r1(78 ^ [])), -(79 ^ [])],extension(73)).
cnf('1.29.1.1',plain,[79 ^ []],reduction('1')).
cnf('1.29.2',plain,[p1(78 ^ []), -(79 ^ []), -(q1(78 ^ []))],extension(72,bind([[_2659], [78 ^ []]]))).
cnf('1.29.2.1',plain,[79 ^ []],reduction('1')).
cnf('1.29.2.2',plain,[q1(78 ^ []), -(79 ^ [])],extension(71)).
cnf('1.29.2.2.1',plain,[79 ^ []],lemmata('1.29.2')).
cnf('1.30',plain,[-(84 ^ []), 82 ^ [80 ^ []], 83 ^ [80 ^ []]],extension(68,bind([[_2692], [80 ^ []]]))).
cnf('1.30.1',plain,[-(82 ^ [80 ^ []]), p1(81 ^ [])],extension(66,bind([[_2692], [80 ^ []]]))).
cnf('1.30.1.1',plain,[-(p1(81 ^ [])), -(83 ^ [81 ^ []])],extension(65,bind([[_2692], [81 ^ []]]))).
cnf('1.30.1.1.1',plain,[83 ^ [81 ^ []], -(84 ^ []), 82 ^ [81 ^ []]],extension(68,bind([[_2692], [81 ^ []]]))).
cnf('1.30.1.1.1.1',plain,[84 ^ []],reduction('1')).
cnf('1.30.1.1.1.2',plain,[-(82 ^ [81 ^ []]), -(q1(81 ^ []))],extension(67,bind([[_2692], [81 ^ []]]))).
cnf('1.30.1.1.1.2.1',plain,[q1(81 ^ []), -(84 ^ []), -(p1(81 ^ []))],extension(69,bind([[_2687], [81 ^ []]]))).
cnf('1.30.1.1.1.2.1.1',plain,[84 ^ []],lemmata('1.30.1.1.1')).
cnf('1.30.1.1.1.2.1.2',plain,[p1(81 ^ [])],reduction('1.30.1')).
cnf('1.30.2',plain,[-(83 ^ [80 ^ []]), p1(80 ^ [])],extension(64,bind([[_2692], [80 ^ []]]))).
cnf('1.30.2.1',plain,[-(p1(80 ^ [])), -(83 ^ [80 ^ []])],extension(65,bind([[_2692], [80 ^ []]]))).
cnf('1.30.2.1.1',plain,[83 ^ [80 ^ []]],reduction('1.30')).
cnf('1.31',plain,[-(91 ^ []), eq(89 ^ [], 90 ^ []), 88 ^ [90 ^ [], 89 ^ []]],extension(60,bind([[_1927, _1926], [90 ^ [], 89 ^ []]]))).
cnf('1.31.1',plain,[-(eq(89 ^ [], 90 ^ [])), -(91 ^ []), 86 ^ [90 ^ [], 89 ^ []], 87 ^ [90 ^ [], 89 ^ []]],extension(61,bind([[_1927, _1926], [90 ^ [], 89 ^ []]]))).
cnf('1.31.1.1',plain,[91 ^ []],reduction('1')).
cnf('1.31.1.2',plain,[-(86 ^ [90 ^ [], 89 ^ []]), a_member_of(85 ^ [90 ^ [], 89 ^ []], 89 ^ [])],extension(58,bind([[_1927, _1926], [90 ^ [], 89 ^ []]]))).
cnf('1.31.1.2.1',plain,[-(a_member_of(85 ^ [90 ^ [], 89 ^ []], 89 ^ [])), -(88 ^ [89 ^ [], 90 ^ []]), a_member_of(85 ^ [90 ^ [], 89 ^ []], 90 ^ [])],extension(54,bind([[_1927, _1928, _1926], [89 ^ [], 85 ^ [90 ^ [], 89 ^ []], 90 ^ []]]))).
cnf('1.31.1.2.1.1',plain,[88 ^ [89 ^ [], 90 ^ []], -(91 ^ []), eq(90 ^ [], 89 ^ [])],extension(60,bind([[_1926, _1927], [90 ^ [], 89 ^ []]]))).
cnf('1.31.1.2.1.1.1',plain,[91 ^ []],lemmata('1.31.1')).
cnf('1.31.1.2.1.1.2',plain,[-(eq(90 ^ [], 89 ^ [])), -(91 ^ []), 86 ^ [89 ^ [], 90 ^ []], 87 ^ [89 ^ [], 90 ^ []]],extension(61,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.31.1.2.1.1.2.1',plain,[91 ^ []],lemmata('1.31.1.2.1.1')).
cnf('1.31.1.2.1.1.2.2',plain,[-(86 ^ [89 ^ [], 90 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])],extension(58,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.31.1.2.1.1.2.2.1',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])), -(88 ^ [90 ^ [], 89 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])],extension(54,bind([[_1927, _1928, _1926], [90 ^ [], 85 ^ [89 ^ [], 90 ^ []], 89 ^ []]]))).
cnf('1.31.1.2.1.1.2.2.1.1',plain,[88 ^ [90 ^ [], 89 ^ []], -(91 ^ []), eq(89 ^ [], 90 ^ [])],extension(60,bind([[_1926, _1927], [89 ^ [], 90 ^ []]]))).
cnf('1.31.1.2.1.1.2.2.1.1.1',plain,[91 ^ []],lemmata('1.31.1.2.1.1.2')).
cnf('1.31.1.2.1.1.2.2.1.1.2',plain,[-(eq(89 ^ [], 90 ^ [])), -(91 ^ [])],extension(63)).
cnf('1.31.1.2.1.1.2.2.1.1.2.1',plain,[91 ^ []],lemmata('1.31.1.2.1.1.2.2.1.1')).
cnf('1.31.1.2.1.1.2.2.1.2',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])), -(86 ^ [89 ^ [], 90 ^ []])],extension(59,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.31.1.2.1.1.2.2.1.2.1',plain,[86 ^ [89 ^ [], 90 ^ []]],reduction('1.31.1.2.1.1.2')).
cnf('1.31.1.2.1.1.2.3',plain,[-(87 ^ [89 ^ [], 90 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])],extension(56,bind([[_1926, _1927], [90 ^ [], 89 ^ []]]))).
cnf('1.31.1.2.1.1.2.3.1',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])), -(88 ^ [90 ^ [], 89 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])],extension(55,bind([[_1926, _1928, _1927], [89 ^ [], 85 ^ [89 ^ [], 90 ^ []], 90 ^ []]]))).
cnf('1.31.1.2.1.1.2.3.1.1',plain,[88 ^ [90 ^ [], 89 ^ []], -(91 ^ []), eq(89 ^ [], 90 ^ [])],extension(60,bind([[_1926, _1927], [89 ^ [], 90 ^ []]]))).
cnf('1.31.1.2.1.1.2.3.1.1.1',plain,[91 ^ []],lemmata('1.31.1.2.1.1.2')).
cnf('1.31.1.2.1.1.2.3.1.1.2',plain,[-(eq(89 ^ [], 90 ^ [])), -(91 ^ [])],extension(63)).
cnf('1.31.1.2.1.1.2.3.1.1.2.1',plain,[91 ^ []],lemmata('1.31.1.2.1.1.2.3.1.1')).
cnf('1.31.1.2.1.1.2.3.1.2',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])), -(87 ^ [89 ^ [], 90 ^ []])],extension(57,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.31.1.2.1.1.2.3.1.2.1',plain,[87 ^ [89 ^ [], 90 ^ []]],reduction('1.31.1.2.1.1.2')).
cnf('1.31.1.2.1.2',plain,[-(a_member_of(85 ^ [90 ^ [], 89 ^ []], 90 ^ [])), -(86 ^ [90 ^ [], 89 ^ []])],extension(59,bind([[_1927, _1926], [90 ^ [], 89 ^ []]]))).
cnf('1.31.1.2.1.2.1',plain,[86 ^ [90 ^ [], 89 ^ []]],reduction('1.31.1')).
cnf('1.31.1.3',plain,[-(87 ^ [90 ^ [], 89 ^ []]), a_member_of(85 ^ [90 ^ [], 89 ^ []], 90 ^ [])],extension(56,bind([[_1926, _1927], [89 ^ [], 90 ^ []]]))).
cnf('1.31.1.3.1',plain,[-(a_member_of(85 ^ [90 ^ [], 89 ^ []], 90 ^ [])), -(88 ^ [90 ^ [], 89 ^ []]), a_member_of(85 ^ [90 ^ [], 89 ^ []], 89 ^ [])],extension(54,bind([[_1927, _1928, _1926], [90 ^ [], 85 ^ [90 ^ [], 89 ^ []], 89 ^ []]]))).
cnf('1.31.1.3.1.1',plain,[88 ^ [90 ^ [], 89 ^ []], -(91 ^ []), eq(89 ^ [], 90 ^ [])],extension(60,bind([[_1926, _1927], [89 ^ [], 90 ^ []]]))).
cnf('1.31.1.3.1.1.1',plain,[91 ^ []],lemmata('1.31.1')).
cnf('1.31.1.3.1.1.2',plain,[-(eq(89 ^ [], 90 ^ [])), -(91 ^ [])],extension(63)).
cnf('1.31.1.3.1.1.2.1',plain,[91 ^ []],lemmata('1.31.1.3.1.1')).
cnf('1.31.1.3.1.2',plain,[-(a_member_of(85 ^ [90 ^ [], 89 ^ []], 89 ^ [])), -(87 ^ [90 ^ [], 89 ^ []])],extension(57,bind([[_1927, _1926], [90 ^ [], 89 ^ []]]))).
cnf('1.31.1.3.1.2.1',plain,[87 ^ [90 ^ [], 89 ^ []]],reduction('1.31.1')).
cnf('1.31.2',plain,[-(88 ^ [90 ^ [], 89 ^ []]), -(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])), a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])],extension(54,bind([[_1927, _1928, _1926], [90 ^ [], 85 ^ [89 ^ [], 90 ^ []], 89 ^ []]]))).
cnf('1.31.2.1',plain,[a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ []), -(88 ^ [90 ^ [], 89 ^ []]), -(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ []))],extension(55,bind([[_1927, _1928, _1926], [90 ^ [], 85 ^ [89 ^ [], 90 ^ []], 89 ^ []]]))).
cnf('1.31.2.1.1',plain,[88 ^ [90 ^ [], 89 ^ []]],reduction('1.31')).
cnf('1.31.2.1.2',plain,[a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ []), -(87 ^ [89 ^ [], 90 ^ []])],extension(56,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.31.2.1.2.1',plain,[87 ^ [89 ^ [], 90 ^ []], -(91 ^ []), -(eq(90 ^ [], 89 ^ [])), 86 ^ [89 ^ [], 90 ^ []]],extension(61,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.31.2.1.2.1.1',plain,[91 ^ []],reduction('1')).
cnf('1.31.2.1.2.1.2',plain,[eq(90 ^ [], 89 ^ []), -(91 ^ [])],extension(62)).
cnf('1.31.2.1.2.1.2.1',plain,[91 ^ []],lemmata('1.31.2.1.2.1')).
cnf('1.31.2.1.2.1.3',plain,[-(86 ^ [89 ^ [], 90 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])],extension(58,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.31.2.1.2.1.3.1',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ []))],reduction('1.31.2')).
cnf('1.31.2.2',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])), -(88 ^ [90 ^ [], 89 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])],extension(55,bind([[_1926, _1928, _1927], [89 ^ [], 85 ^ [89 ^ [], 90 ^ []], 90 ^ []]]))).
cnf('1.31.2.2.1',plain,[88 ^ [90 ^ [], 89 ^ []]],reduction('1.31')).
cnf('1.31.2.2.2',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])), -(87 ^ [89 ^ [], 90 ^ []])],extension(57,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.31.2.2.2.1',plain,[87 ^ [89 ^ [], 90 ^ []], -(91 ^ []), -(eq(90 ^ [], 89 ^ [])), 86 ^ [89 ^ [], 90 ^ []]],extension(61,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.31.2.2.2.1.1',plain,[91 ^ []],reduction('1')).
cnf('1.31.2.2.2.1.2',plain,[eq(90 ^ [], 89 ^ []), -(91 ^ []), 88 ^ [89 ^ [], 90 ^ []]],extension(60,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.31.2.2.2.1.2.1',plain,[91 ^ []],lemmata('1.31.2.2.2.1')).
cnf('1.31.2.2.2.1.2.2',plain,[-(88 ^ [89 ^ [], 90 ^ []]), a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ []), -(a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ []))],extension(55,bind([[_1927, _1928, _1926], [89 ^ [], 85 ^ [89 ^ [], 90 ^ []], 90 ^ []]]))).
cnf('1.31.2.2.2.1.2.2.1',plain,[-(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])), -(86 ^ [89 ^ [], 90 ^ []])],extension(59,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.31.2.2.2.1.2.2.1.1',plain,[86 ^ [89 ^ [], 90 ^ []], -(91 ^ []), -(eq(90 ^ [], 89 ^ [])), 87 ^ [89 ^ [], 90 ^ []]],extension(61,bind([[_1927, _1926], [89 ^ [], 90 ^ []]]))).
cnf('1.31.2.2.2.1.2.2.1.1.1',plain,[91 ^ []],lemmata('1.31.2.2.2.1.2')).
cnf('1.31.2.2.2.1.2.2.1.1.2',plain,[eq(90 ^ [], 89 ^ []), -(91 ^ [])],extension(62)).
cnf('1.31.2.2.2.1.2.2.1.1.2.1',plain,[91 ^ []],lemmata('1.31.2.2.2.1.2.2.1.1')).
cnf('1.31.2.2.2.1.2.2.1.1.3',plain,[-(87 ^ [89 ^ [], 90 ^ []])],reduction('1.31.2.2.2')).
cnf('1.31.2.2.2.1.2.2.2',plain,[a_member_of(85 ^ [89 ^ [], 90 ^ []], 90 ^ [])],lemmata('1.31.2')).
cnf('1.31.2.2.2.1.3',plain,[-(86 ^ [89 ^ [], 90 ^ []]), -(a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ []))],extension(59,bind([[_1926, _1927], [90 ^ [], 89 ^ []]]))).
cnf('1.31.2.2.2.1.3.1',plain,[a_member_of(85 ^ [89 ^ [], 90 ^ []], 89 ^ [])],reduction('1.31.2')).
cnf('1.32',plain,[-(93 ^ []), p1(92 ^ [])],extension(52,bind([[_1938], [92 ^ []]]))).
cnf('1.32.1',plain,[-(p1(92 ^ [])), -(93 ^ [])],extension(53)).
cnf('1.32.1.1',plain,[93 ^ []],reduction('1')).
cnf('1.33',plain,[-(96 ^ []), p1(94 ^ []), p1(95 ^ [])],extension(50)).
cnf('1.33.1',plain,[-(p1(94 ^ [])), -(96 ^ [])],extension(51,bind([[_1941], [94 ^ []]]))).
cnf('1.33.1.1',plain,[96 ^ []],reduction('1')).
cnf('1.33.2',plain,[-(p1(95 ^ [])), -(96 ^ [])],extension(51,bind([[_1941], [95 ^ []]]))).
cnf('1.33.2.1',plain,[96 ^ []],reduction('1')).
cnf('1.34',plain,[-(99 ^ []), p1(98 ^ []), p1(97 ^ [])],extension(48)).
cnf('1.34.1',plain,[-(p1(98 ^ [])), -(99 ^ [])],extension(49,bind([[_2810], [98 ^ []]]))).
cnf('1.34.1.1',plain,[99 ^ []],reduction('1')).
cnf('1.34.2',plain,[-(p1(97 ^ [])), -(99 ^ [])],extension(49,bind([[_2810], [97 ^ []]]))).
cnf('1.34.2.1',plain,[99 ^ []],reduction('1')).
cnf('1.35',plain,[-(101 ^ []), b(100 ^ []), a1(100 ^ [])],extension(45,bind([[_1947], [100 ^ []]]))).
cnf('1.35.1',plain,[-(b(100 ^ [])), -(101 ^ [])],extension(46,bind([[_1944], [100 ^ []]]))).
cnf('1.35.1.1',plain,[101 ^ []],reduction('1')).
cnf('1.35.2',plain,[-(a1(100 ^ [])), -(101 ^ [])],extension(47)).
cnf('1.35.2.1',plain,[101 ^ []],reduction('1')).
cnf('1.36',plain,[-(103 ^ []), -(a(102 ^ [], 102 ^ [])), -(a(102 ^ [], 102 ^ []))],extension(43,bind([[_2837], [102 ^ []]]))).
cnf('1.36.1',plain,[a(102 ^ [], 102 ^ []), -(103 ^ []), a(102 ^ [], 102 ^ [])],extension(44,bind([[_2837], [102 ^ []]]))).
cnf('1.36.1.1',plain,[103 ^ []],reduction('1')).
cnf('1.36.1.2',plain,[-(a(102 ^ [], 102 ^ []))],reduction('1.36')).
cnf('1.36.2',plain,[a(102 ^ [], 102 ^ [])],lemmata('1.36')).
cnf('1.37',plain,[-(105 ^ []), a1(104 ^ []), -(b(104 ^ []))],extension(40,bind([[_1952], [104 ^ []]]))).
cnf('1.37.1',plain,[-(a1(104 ^ [])), -(105 ^ [])],extension(42)).
cnf('1.37.1.1',plain,[105 ^ []],reduction('1')).
cnf('1.37.2',plain,[b(104 ^ []), -(105 ^ [])],extension(41,bind([[_1957], [104 ^ []]]))).
cnf('1.37.2.1',plain,[105 ^ []],reduction('1')).
cnf('1.38',plain,[-(107 ^ []), p1(106 ^ []), -(q1(106 ^ []))],extension(37,bind([[_1960], [106 ^ []]]))).
cnf('1.38.1',plain,[-(p1(106 ^ [])), -(107 ^ [])],extension(39,bind([[_1965], [106 ^ []]]))).
cnf('1.38.1.1',plain,[107 ^ []],reduction('1')).
cnf('1.38.2',plain,[q1(106 ^ []), -(107 ^ [])],extension(38)).
cnf('1.38.2.1',plain,[107 ^ []],reduction('1')).
cnf('1.39',plain,[-(108 ^ []), p1(_16244)],extension(35,bind([[_1971], [_16244]]))).
cnf('1.39.1',plain,[-(p1(_16244)), -(108 ^ [])],extension(36,bind([[_1968], [_16244]]))).
cnf('1.39.1.1',plain,[108 ^ []],reduction('1')).
cnf('1.40',plain,[-(113 ^ []), p1(109 ^ []), 112 ^ []],extension(33,bind([[_1974], [109 ^ []]]))).
cnf('1.40.1',plain,[-(p1(109 ^ [])), -(113 ^ [])],extension(34)).
cnf('1.40.1.1',plain,[113 ^ []],reduction('1')).
cnf('1.40.2',plain,[-(112 ^ []), 110 ^ [], 111 ^ []],extension(32)).
cnf('1.40.2.1',plain,[-(110 ^ []), -(b0)],extension(30)).
cnf('1.40.2.1.1',plain,[b0, -(110 ^ [])],extension(31)).
cnf('1.40.2.1.1.1',plain,[110 ^ []],reduction('1.40.2')).
cnf('1.40.2.2',plain,[-(111 ^ []), q0],extension(28)).
cnf('1.40.2.2.1',plain,[-(q0), -(111 ^ [])],extension(29)).
cnf('1.40.2.2.1.1',plain,[111 ^ []],reduction('1.40.2')).
cnf('1.41',plain,[-(116 ^ []), p1(115 ^ [_16402])],extension(26,bind([[_1980], [_16402]]))).
cnf('1.41.1',plain,[-(p1(115 ^ [_16402])), -(116 ^ [])],extension(27,bind([[_1977], [115 ^ [_16402]]]))).
cnf('1.41.1.1',plain,[116 ^ []],reduction('1')).
cnf('1.42',plain,[-(119 ^ []), p1(117 ^ []), p1(118 ^ [])],extension(24)).
cnf('1.42.1',plain,[-(p1(117 ^ [])), -(119 ^ [])],extension(25,bind([[_1981], [117 ^ []]]))).
cnf('1.42.1.1',plain,[119 ^ []],reduction('1')).
cnf('1.42.2',plain,[-(p1(118 ^ [])), -(119 ^ [])],extension(25,bind([[_1981], [118 ^ []]]))).
cnf('1.42.2.1',plain,[119 ^ []],reduction('1')).
cnf('1.43',plain,[-(133 ^ []), 131 ^ [130 ^ [], f(130 ^ [])], q1(f(130 ^ [])), 132 ^ [130 ^ [], f(130 ^ [])]],extension(5,bind([[_3079, _3078], [130 ^ [], f(130 ^ [])]]))).
cnf('1.43.1',plain,[-(131 ^ [130 ^ [], f(130 ^ [])]), p1(f(130 ^ []))],extension(3,bind([[_3079, _3078], [130 ^ [], f(130 ^ [])]]))).
cnf('1.43.1.1',plain,[-(p1(f(130 ^ []))), -(131 ^ [130 ^ [], f(130 ^ [])])],extension(4,bind([[_3079, _3078], [130 ^ [], f(130 ^ [])]]))).
cnf('1.43.1.1.1',plain,[131 ^ [130 ^ [], f(130 ^ [])]],reduction('1.43')).
cnf('1.43.2',plain,[-(q1(f(130 ^ []))), -(133 ^ [])],extension(6,bind([[_3073], [130 ^ []]]))).
cnf('1.43.2.1',plain,[133 ^ []],reduction('1')).
cnf('1.43.3',plain,[-(132 ^ [130 ^ [], f(130 ^ [])]), r1(130 ^ []), r1(129 ^ [])],extension(1,bind([[_3079, _3078], [130 ^ [], f(130 ^ [])]]))).
cnf('1.43.3.1',plain,[-(r1(130 ^ [])), -(132 ^ [130 ^ [], f(130 ^ [])])],extension(2,bind([[_3079, _3078], [130 ^ [], f(130 ^ [])]]))).
cnf('1.43.3.1.1',plain,[132 ^ [130 ^ [], f(130 ^ [])]],reduction('1.43')).
cnf('1.43.3.2',plain,[-(r1(129 ^ [])), -(132 ^ [129 ^ [], f(129 ^ [])])],extension(2,bind([[_3079, _3078], [129 ^ [], f(129 ^ [])]]))).
cnf('1.43.3.2.1',plain,[132 ^ [129 ^ [], f(129 ^ [])], -(133 ^ []), 131 ^ [129 ^ [], f(129 ^ [])], q1(f(129 ^ []))],extension(5,bind([[_3079, _3078], [129 ^ [], f(129 ^ [])]]))).
cnf('1.43.3.2.1.1',plain,[133 ^ []],reduction('1')).
cnf('1.43.3.2.1.2',plain,[-(131 ^ [129 ^ [], f(129 ^ [])]), p1(f(129 ^ []))],extension(3,bind([[_3079, _3078], [129 ^ [], f(129 ^ [])]]))).
cnf('1.43.3.2.1.2.1',plain,[-(p1(f(129 ^ []))), -(131 ^ [129 ^ [], f(129 ^ [])])],extension(4,bind([[_3079, _3078], [129 ^ [], f(129 ^ [])]]))).
cnf('1.43.3.2.1.2.1.1',plain,[131 ^ [129 ^ [], f(129 ^ [])]],reduction('1.43.3.2.1')).
cnf('1.43.3.2.1.3',plain,[-(q1(f(129 ^ []))), -(133 ^ [])],extension(6,bind([[_3073], [129 ^ []]]))).
cnf('1.43.3.2.1.3.1',plain,[133 ^ []],lemmata('1.43.3.2.1')).
cnf('1.44',plain,[-(128 ^ []), q1(f(124 ^ [])), 127 ^ [124 ^ [], f(124 ^ [])]],extension(11,bind([[_3028, _3027], [124 ^ [], f(124 ^ [])]]))).
cnf('1.44.1',plain,[-(q1(f(124 ^ []))), -(128 ^ [])],extension(12)).
cnf('1.44.1.1',plain,[128 ^ []],reduction('1')).
cnf('1.44.2',plain,[-(127 ^ [124 ^ [], f(124 ^ [])]), p1(f(124 ^ [])), 126 ^ [124 ^ [], f(124 ^ [])]],extension(9,bind([[_3028, _3027], [124 ^ [], f(124 ^ [])]]))).
cnf('1.44.2.1',plain,[-(p1(f(124 ^ []))), -(127 ^ [124 ^ [], f(124 ^ [])])],extension(10,bind([[_3028, _3027], [124 ^ [], f(124 ^ [])]]))).
cnf('1.44.2.1.1',plain,[127 ^ [124 ^ [], f(124 ^ [])]],reduction('1.44')).
cnf('1.44.2.2',plain,[-(126 ^ [124 ^ [], f(124 ^ [])]), r1(124 ^ []), r1(125 ^ [])],extension(7,bind([[_3028, _3027], [124 ^ [], f(124 ^ [])]]))).
cnf('1.44.2.2.1',plain,[-(r1(124 ^ [])), -(126 ^ [124 ^ [], f(124 ^ [])])],extension(8,bind([[_3028, _3027], [124 ^ [], f(124 ^ [])]]))).
cnf('1.44.2.2.1.1',plain,[126 ^ [124 ^ [], f(124 ^ [])]],reduction('1.44.2')).
cnf('1.44.2.2.2',plain,[-(r1(125 ^ [])), -(126 ^ [125 ^ [], f(124 ^ [])])],extension(8,bind([[_3028, _3027], [125 ^ [], f(124 ^ [])]]))).
cnf('1.44.2.2.2.1',plain,[126 ^ [125 ^ [], f(124 ^ [])], -(127 ^ [125 ^ [], f(124 ^ [])]), p1(f(124 ^ []))],extension(9,bind([[_3028, _3027], [125 ^ [], f(124 ^ [])]]))).
cnf('1.44.2.2.2.1.1',plain,[127 ^ [125 ^ [], f(124 ^ [])], -(128 ^ []), q1(f(124 ^ []))],extension(11,bind([[_3028, _3027], [125 ^ [], f(124 ^ [])]]))).
cnf('1.44.2.2.2.1.1.1',plain,[128 ^ []],reduction('1')).
cnf('1.44.2.2.2.1.1.2',plain,[-(q1(f(124 ^ []))), -(128 ^ [])],extension(12)).
cnf('1.44.2.2.2.1.1.2.1',plain,[128 ^ []],lemmata('1.44.2.2.2.1.1')).
cnf('1.44.2.2.2.1.2',plain,[-(p1(f(124 ^ [])))],lemmata('1.44.2')).
cnf('1.45',plain,[-(123 ^ []), a1(122 ^ []), -(b(122 ^ [])), -(c(122 ^ []))],extension(13,bind([[_1984], [122 ^ []]]))).
cnf('1.45.1',plain,[-(a1(122 ^ [])), -(123 ^ [])],extension(15)).
cnf('1.45.1.1',plain,[123 ^ []],reduction('1')).
cnf('1.45.2',plain,[b(122 ^ []), -(123 ^ [])],extension(14)).
cnf('1.45.2.1',plain,[123 ^ []],reduction('1')).
cnf('1.45.3',plain,[c(122 ^ []), -(123 ^ []), a1(122 ^ [])],extension(16,bind([[_1991], [122 ^ []]]))).
cnf('1.45.3.1',plain,[123 ^ []],reduction('1')).
cnf('1.45.3.2',plain,[-(a1(122 ^ []))],lemmata('1.45')).
cnf('1.46',plain,[-(121 ^ []), e(120 ^ []), -(c(f(120 ^ []))), -(g(120 ^ []))],extension(17,bind([[_2955], [120 ^ []]]))).
cnf('1.46.1',plain,[-(e(120 ^ [])), -(121 ^ [])],extension(20)).
cnf('1.46.1.1',plain,[121 ^ []],reduction('1')).
cnf('1.46.2',plain,[c(f(120 ^ [])), -(121 ^ []), p1(f(120 ^ []))],extension(22,bind([[_2957], [f(120 ^ [])]]))).
cnf('1.46.2.1',plain,[121 ^ []],reduction('1')).
cnf('1.46.2.2',plain,[-(p1(f(120 ^ []))), -(121 ^ []), s(120 ^ [], f(120 ^ []))],extension(18,bind([[_2958], [f(120 ^ [])]]))).
cnf('1.46.2.2.1',plain,[121 ^ []],lemmata('1.46.2')).
cnf('1.46.2.2.2',plain,[-(s(120 ^ [], f(120 ^ []))), -(121 ^ []), e(120 ^ []), -(g(120 ^ []))],extension(19,bind([[_2954], [120 ^ []]]))).
cnf('1.46.2.2.2.1',plain,[121 ^ []],lemmata('1.46.2.2')).
cnf('1.46.2.2.2.2',plain,[-(e(120 ^ []))],lemmata('1.46')).
cnf('1.46.2.2.2.3',plain,[g(120 ^ []), -(121 ^ []), p1(120 ^ [])],extension(23,bind([[_2956], [120 ^ []]]))).
cnf('1.46.2.2.2.3.1',plain,[121 ^ []],lemmata('1.46.2.2.2')).
cnf('1.46.2.2.2.3.2',plain,[-(p1(120 ^ [])), -(121 ^ [])],extension(21)).
cnf('1.46.2.2.2.3.2.1',plain,[121 ^ []],lemmata('1.46.2.2.2.3')).
cnf('1.46.3',plain,[g(120 ^ []), -(121 ^ []), p1(120 ^ [])],extension(23,bind([[_2956], [120 ^ []]]))).
cnf('1.46.3.1',plain,[121 ^ []],reduction('1')).
cnf('1.46.3.2',plain,[-(p1(120 ^ [])), -(121 ^ [])],extension(21)).
cnf('1.46.3.2.1',plain,[121 ^ []],lemmata('1.46.3')).
%-----------------------------------------------------
End of proof for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE063.p

WATCH: 30.32 CPU 29.90 WC

FINAL WATCH: 30.32 CPU 29.90 WC