(set-logic HORN)

; benchmark generated from python API
(set-info :status unknown)
(declare-datatypes ((|Pc[b]| 0)) (((b_0) (b_1) (b_2))))
 (declare-datatypes ((|Pc[a]| 0)) (((a_0) (a_1) (a_2))))
 (declare-fun D_10 (|Pc[a]| Int Int Int |Pc[b]| Int Int Int) Bool)
(declare-fun D_01 (|Pc[a]| Int Int Int |Pc[b]| Int Int Int) Bool)
(declare-fun D_11 (|Pc[a]| Int Int Int |Pc[b]| Int Int Int) Bool)
(assert
 (forall ((pc_a |Pc[a]|) (pc_b |Pc[b]|) (c_b Int) (c_a Int) (a_a Int) (b_a Int) (a_b Int) (b_b Int) )(let (($x1799 (D_10 pc_a a_a b_a c_a pc_b a_b b_b c_b)))
 (let (($x1763 (= pc_a a_2)))
 (let (($x14392 (or $x1763)))
 (let (($x1020 (not $x14392)))
 (let (($x1005 (not $x1020)))
 (let (($x1189 (= pc_b b_2)))
 (let (($x855 (or $x1189)))
 (let (($x1780 (and $x14392 $x855 (not (< c_b c_a)))))
 (let (($x1046 (or $x1780 $x1005)))
 (let (($x1062 (and $x1046 and)))
 (=> $x1062 $x1799))))))))))))
 )
(assert
 (forall ((pc_a |Pc[a]|) (pc_b |Pc[b]|) (c_b Int) (c_a Int) (a_a Int) (b_a Int) (a_b Int) (b_b Int) )(let (($x6580 (D_01 pc_a a_a b_a c_a pc_b a_b b_b c_b)))
 (let (($x1189 (= pc_b b_2)))
 (let (($x855 (or $x1189)))
 (let (($x785 (not $x855)))
 (let (($x1480 (not $x785)))
 (let (($x1763 (= pc_a a_2)))
 (let (($x14392 (or $x1763)))
 (let (($x1780 (and $x14392 $x855 (not (< c_b c_a)))))
 (let (($x1236 (or $x1780 $x1480)))
 (let (($x1550 (and $x1236 and)))
 (=> $x1550 $x6580))))))))))))
 )
(assert
 (forall ((pc_a |Pc[a]|) (pc_b |Pc[b]|) (c_b Int) (c_a Int) (a_a Int) (b_a Int) (a_b Int) (b_b Int) )(let (($x1760 (D_11 pc_a a_a b_a c_a pc_b a_b b_b c_b)))
 (let (($x1189 (= pc_b b_2)))
 (let (($x855 (or $x1189)))
 (let (($x1763 (= pc_a a_2)))
 (let (($x14392 (or $x1763)))
 (let (($x1948 (= $x14392 $x855)))
 (let (($x1659 (not $x1948)))
 (let (($x1780 (and $x14392 $x855 (not (< c_b c_a)))))
 (let (($x4221 (or $x1780 $x1659)))
 (let (($x8249 (and $x4221 and)))
 (=> $x8249 $x1760))))))))))))
 )
(assert
 (forall ((pc_a_prime |Pc[a]|) (a_a_prime Int) (b_a_prime Int) (c_a_prime Int) (pc_b_prime |Pc[b]|) (a_b_prime Int) (b_b_prime Int) (c_b_prime Int) (a_a Int) (a_b Int) (sqa_0 Int) (sqa_1 Int) (pc_a |Pc[a]|) (b_a Int) (c_a Int) (pc_b |Pc[b]|) (b_b Int) (c_b Int) )(let (($x29326 (D_10 pc_a a_a b_a c_a pc_b a_b b_b c_b)))
 (let (($x49245 (= c_b c_b_prime)))
 (let (($x13380 (= b_b b_b_prime)))
 (let (($x71439 (= a_b a_b_prime)))
 (let (($x302 (= pc_b pc_b_prime)))
 (let (($x1972 (and $x302 $x71439 $x13380 $x49245)))
 (let (($x958 (= c_a_prime c_a)))
 (let (($x1450 (= b_a_prime b_a)))
 (let (($x64498 (= a_a_prime a_a)))
 (let (($x243 (= pc_a_prime a_2)))
 (let (($x1724 (and $x243 $x64498 $x1450 $x958)))
 (let (($x382 (= pc_a a_2)))
 (let (($x934 (and $x382 $x1724)))
 (let (($x476 (>= a_a b_a)))
 (let (($x1366 (= pc_a a_1)))
 (let (($x4416 (and $x1366 $x476 $x1724)))
 (let (($x80124 (= a_a_prime (+ a_a 1))))
 (let (($x451 (= pc_a_prime a_1)))
 (let (($x71592 (and $x451 $x80124 $x1450 (= c_a_prime (+ c_a sqa_0)))))
 (let (($x1623 (< a_a b_a)))
 (let (($x1118 (and $x1366 $x1623 $x71592)))
 (let (($x39127 (= pc_a a_0)))
 (let (($x356 (and $x39127 (and $x451 $x64498 $x1450 (= c_a_prime 0)))))
 (let (($x890 (or $x356 $x1118 $x4416 $x934)))
 (let (($x558 (or $x382)))
 (let (($x1074 (not $x558)))
 (let (($x835 (and $x1074 $x890 $x1972)))
 (let (($x4074 (> sqa_1 0)))
 (let (($x879138 (> a_b 0)))
 (let (($x362 (=> $x879138 $x4074)))
 (let (($x61399 (> sqa_0 0)))
 (let (($x1655 (> a_a 0)))
 (let (($x5527 (=> $x1655 $x61399)))
 (let (($x1992 (= sqa_0 sqa_1)))
 (let (($x1804 (= a_a a_b)))
 (let (($x1052 (=> $x1804 $x1992)))
 (let (($x472 (D_11 pc_a_prime a_a_prime b_a_prime c_a_prime pc_b_prime a_b_prime b_b_prime c_b_prime)))
 (let (($x812 (D_01 pc_a_prime a_a_prime b_a_prime c_a_prime pc_b_prime a_b_prime b_b_prime c_b_prime)))
 (let (($x70882 (D_10 pc_a_prime a_a_prime b_a_prime c_a_prime pc_b_prime a_b_prime b_b_prime c_b_prime)))
 (let (($x67573 (and $x70882 $x812 $x472)))
 (let (($x806377 (and $x67573 and and $x1052 $x5527 $x362 $x835)))
 (=> $x806377 $x29326)))))))))))))))))))))))))))))))))))))))))))
 )
(assert
 (forall ((pc_a_prime |Pc[a]|) (a_a_prime Int) (b_a_prime Int) (c_a_prime Int) (pc_b_prime |Pc[b]|) (a_b_prime Int) (b_b_prime Int) (c_b_prime Int) (a_a Int) (a_b Int) (sqa_0 Int) (sqa_1 Int) (pc_b |Pc[b]|) (pc_a |Pc[a]|) (b_a Int) (c_a Int) (b_b Int) (c_b Int) )(let (($x2058 (D_01 pc_a a_a b_a c_a pc_b a_b b_b c_b)))
 (let (($x70746 (= c_b_prime c_b)))
 (let (($x7801 (= b_b_prime b_b)))
 (let (($x29683 (= a_b_prime a_b)))
 (let (($x4147 (= pc_b_prime b_2)))
 (let (($x1019 (and $x4147 $x29683 $x7801 $x70746)))
 (let (($x8356 (= pc_b b_2)))
 (let (($x508 (and $x8356 $x1019)))
 (let (($x1632 (>= a_b b_b)))
 (let (($x249 (= pc_b b_1)))
 (let (($x67756 (and $x249 $x1632 $x1019)))
 (let (($x1665 (= pc_b_prime b_1)))
 (let (($x804 (and $x1665 (= a_b_prime (+ a_b 1)) $x7801 (= c_b_prime (+ c_b sqa_1)))))
 (let (($x4178 (< a_b b_b)))
 (let (($x81308 (and $x249 $x4178 $x804)))
 (let (($x345 (= c_b_prime 0)))
 (let (($x30263 (and $x1665 $x29683 $x7801 $x345)))
 (let (($x80655 (= pc_b b_0)))
 (let (($x5931 (and $x80655 $x30263)))
 (let (($x883 (or $x5931 $x81308 $x67756 $x508)))
 (let (($x427 (= c_a c_a_prime)))
 (let (($x23385 (= b_a b_a_prime)))
 (let (($x1355 (= a_a a_a_prime)))
 (let (($x1199 (= pc_a pc_a_prime)))
 (let (($x1403 (and $x1199 $x1355 $x23385 $x427)))
 (let (($x1485 (not (or $x8356))))
 (let (($x2229 (and $x1485 $x1403 $x883 true)))
 (let (($x4074 (> sqa_1 0)))
 (let (($x879138 (> a_b 0)))
 (let (($x362 (=> $x879138 $x4074)))
 (let (($x61399 (> sqa_0 0)))
 (let (($x1655 (> a_a 0)))
 (let (($x5527 (=> $x1655 $x61399)))
 (let (($x1992 (= sqa_0 sqa_1)))
 (let (($x1804 (= a_a a_b)))
 (let (($x1052 (=> $x1804 $x1992)))
 (let (($x472 (D_11 pc_a_prime a_a_prime b_a_prime c_a_prime pc_b_prime a_b_prime b_b_prime c_b_prime)))
 (let (($x812 (D_01 pc_a_prime a_a_prime b_a_prime c_a_prime pc_b_prime a_b_prime b_b_prime c_b_prime)))
 (let (($x70882 (D_10 pc_a_prime a_a_prime b_a_prime c_a_prime pc_b_prime a_b_prime b_b_prime c_b_prime)))
 (let (($x67573 (and $x70882 $x812 $x472)))
 (let (($x1043225 (and $x67573 and and $x1052 $x5527 $x362 $x2229)))
 (=> $x1043225 $x2058)))))))))))))))))))))))))))))))))))))))))))
 )
(assert
 (forall ((pc_a_prime |Pc[a]|) (a_a_prime Int) (b_a_prime Int) (c_a_prime Int) (pc_b_prime |Pc[b]|) (a_b_prime Int) (b_b_prime Int) (c_b_prime Int) (a_a Int) (a_b Int) (sqa_0 Int) (sqa_1 Int) (pc_a |Pc[a]|) (pc_b |Pc[b]|) (b_a Int) (c_a Int) (b_b Int) (c_b Int) )(let (($x263 (D_11 pc_a a_a b_a c_a pc_b a_b b_b c_b)))
 (let (($x70746 (= c_b_prime c_b)))
 (let (($x7801 (= b_b_prime b_b)))
 (let (($x29683 (= a_b_prime a_b)))
 (let (($x4147 (= pc_b_prime b_2)))
 (let (($x1019 (and $x4147 $x29683 $x7801 $x70746)))
 (let (($x2015 (= pc_b b_2)))
 (let (($x79201 (and $x2015 $x1019)))
 (let (($x1632 (>= a_b b_b)))
 (let (($x1276 (= pc_b b_1)))
 (let (($x1159 (and $x1276 $x1632 $x1019)))
 (let (($x1665 (= pc_b_prime b_1)))
 (let (($x804 (and $x1665 (= a_b_prime (+ a_b 1)) $x7801 (= c_b_prime (+ c_b sqa_1)))))
 (let (($x4178 (< a_b b_b)))
 (let (($x1162 (and $x1276 $x4178 $x804)))
 (let (($x345 (= c_b_prime 0)))
 (let (($x30263 (and $x1665 $x29683 $x7801 $x345)))
 (let (($x58694 (= pc_b b_0)))
 (let (($x1716 (and $x58694 $x30263)))
 (let (($x5453 (or $x1716 $x1162 $x1159 $x79201)))
 (let (($x30290 (= c_a_prime c_a)))
 (let (($x1597 (= b_a_prime b_a)))
 (let (($x64498 (= a_a_prime a_a)))
 (let (($x243 (= pc_a_prime a_2)))
 (let (($x538 (and $x243 $x64498 $x1597 $x30290)))
 (let (($x382 (= pc_a a_2)))
 (let (($x89066 (and $x382 $x538)))
 (let (($x69819 (>= a_a b_a)))
 (let (($x1366 (= pc_a a_1)))
 (let (($x69814 (and $x1366 $x69819 $x538)))
 (let (($x80124 (= a_a_prime (+ a_a 1))))
 (let (($x451 (= pc_a_prime a_1)))
 (let (($x70618 (and $x451 $x80124 $x1597 (= c_a_prime (+ c_a sqa_0)))))
 (let (($x70773 (< a_a b_a)))
 (let (($x70683 (and $x1366 $x70773 $x70618)))
 (let (($x39127 (= pc_a a_0)))
 (let (($x321 (and $x39127 (and $x451 $x64498 $x1597 (= c_a_prime 0)))))
 (let (($x1599 (or $x321 $x70683 $x69814 $x89066)))
 (let (($x558 (or $x382)))
 (let (($x574 (= $x558 (or $x2015))))
 (let (($x30391 (and $x574 $x1599 $x5453 true)))
 (let (($x4074 (> sqa_1 0)))
 (let (($x879138 (> a_b 0)))
 (let (($x362 (=> $x879138 $x4074)))
 (let (($x61399 (> sqa_0 0)))
 (let (($x1655 (> a_a 0)))
 (let (($x5527 (=> $x1655 $x61399)))
 (let (($x1992 (= sqa_0 sqa_1)))
 (let (($x1804 (= a_a a_b)))
 (let (($x1052 (=> $x1804 $x1992)))
 (let (($x472 (D_11 pc_a_prime a_a_prime b_a_prime c_a_prime pc_b_prime a_b_prime b_b_prime c_b_prime)))
 (let (($x812 (D_01 pc_a_prime a_a_prime b_a_prime c_a_prime pc_b_prime a_b_prime b_b_prime c_b_prime)))
 (let (($x70882 (D_10 pc_a_prime a_a_prime b_a_prime c_a_prime pc_b_prime a_b_prime b_b_prime c_b_prime)))
 (let (($x67573 (and $x70882 $x812 $x472)))
 (let (($x411583 (and $x67573 and and $x1052 $x5527 $x362 $x30391)))
 (=> $x411583 $x263)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 )
(assert
 (forall ((pc_a |Pc[a]|) (a_a Int) (b_a Int) (c_a Int) (pc_b |Pc[b]|) (a_b Int) (b_b Int) (c_b Int) )(let (($x10302 (< a_a a_b)))
 (let (($x1098 (<= a_b b_b)))
 (let (($x744 (<= a_a b_a)))
 (let (($x14642 (< b_b b_a)))
 (let (($x4074 (> a_a 0)))
 (let (($x4024 (and $x4074 $x4074 $x14642 $x744 $x1098 $x10302)))
 (let (($x929 (= pc_b b_0)))
 (let (($x1758 (= pc_a a_0)))
 (let (($x1940 (and $x1758 $x929 $x4024)))
 (let (($x478 (D_11 pc_a a_a b_a c_a pc_b a_b b_b c_b)))
 (let (($x347 (D_01 pc_a a_a b_a c_a pc_b a_b b_b c_b)))
 (let (($x2107 (D_10 pc_a a_a b_a c_a pc_b a_b b_b c_b)))
 (let (($x1245 (and $x2107 $x347 $x478)))
 (let (($x2026 (and $x1245 and $x1940)))
 (=> $x2026 false))))))))))))))))
 )
(check-sat)