; IMPORTANT NOTE!!!
; For each test datum, name it x, 
; call:
;   (wang (car x) (cadr x))
; and compare the resulting value with (caddr x)

; case 1
((s3) (s3) #t)
((s3) (s3) #t)
((s2) (s1) ())
((s3) (s1) ())
((s2) (s1) ())
((s1) (s3) ())
((s3) (s1) ())
((s2) (s3) ())
((s2) (s3) ())
((s2) (s1) ())
((s2) (s1) ())
((s2) (s1) ())
((s1) (s1) #t)
((s2) (s1) ())
((s1) (s1) #t)
((s3) (s3) #t)
((s1) (s3) ())
((s1) (s3) ())
((s1) (s3) ())
((s3) (s2) ())

; case 2
(((or s2 s1)) ((and s2 s2)) ())
(((or s3 s3)) ((not s3)) ())
(((> s3 s2)) ((not s1)) ())
(((or s2 s1)) ((or s1 s2)) #t)
(((and s3 s1)) ((> s1 s3)) #t)
(((not s2)) ((or s1 s2)) ())
(((not s1)) ((and s2 s3)) ())
(((or s2 s3)) ((not s1)) ())
(((> s1 s2)) ((> s3 s1)) ())
(((and s1 s2)) ((not s3)) ())
(((and s1 s3)) ((not s2)) ())
(((not s3)) ((not s1)) ())
(((and s3 s3)) ((not s3)) ())
(((not s1)) ((not s2)) ())
(((> s3 s1)) ((or s3 s1)) ())
(((not s2)) ((or s1 s1)) ())
(((or s1 s1)) ((not s1)) ())
(((and s1 s2)) ((> s1 s2)) #t)
(((not s2)) ((> s2 s3)) #t)
(((not s3)) ((not s3)) #t)
(((> s2 s1)) ((not s2)) ())
(((not s1)) ((not s1)) #t)
(((or s2 s1)) ((and s3 s3)) ())
(((and s3 s1)) ((and s3 s3)) #t)
(((and s3 s2)) ((and s3 s2)) #t)
(((not s1)) ((and s2 s2)) ())
(((and s2 s3)) ((or s3 s2)) #t)
(((or s2 s2)) ((> s3 s2)) #t)
(((not s2)) ((and s1 s3)) ())
(((> s2 s1)) ((and s1 s3)) ())
(((and s1 s3)) ((and s3 s1)) #t)
(((and s2 s1)) ((> s2 s1)) #t)
(((not s2)) ((and s3 s2)) ())
(((> s3 s1)) ((> s1 s3)) ())
(((and s1 s1)) ((> s1 s2)) ())
(((or s3 s1)) ((or s3 s1)) #t)
(((not s3)) ((and s3 s2)) ())
(((> s3 s2)) ((or s3 s1)) ())
(((and s3 s2)) ((> s3 s2)) #t)
(((not s3)) ((or s2 s2)) ())
(((or s1 s3)) ((and s1 s1)) ())
(((not s3)) ((> s1 s3)) ())
(((and s3 s1)) ((and s1 s3)) #t)
(((or s3 s1)) ((or s2 s2)) ())
(((or s1 s1)) ((not s3)) ())
(((or s2 s2)) ((not s3)) ())
(((not s2)) ((not s1)) ())
(((or s1 s2)) ((and s1 s1)) ())
(((> s3 s2)) ((and s3 s3)) ())
(((> s1 s2)) ((> s2 s1)) ())

; case 3
(((and s4 s1)) ((not s3)) ())
(((> s2 s4)) ((or s3 s4)) ())
(((> s4 s1)) ((> s2 s4)) ())
(((and s2 s2)) ((and s3 s4)) ())
(((or s3 s1)) ((and s4 s3)) ())
(((not s1)) ((or s3 s1)) ())
(((or s2 s2)) ((not s2)) ())
((s4) ((> s4 s1)) ())
(((or s2 s4)) ((and s3 s1)) ())
(((> s4 s2)) (s2) ())
(((not s2)) (s4) ())
(((not s1)) ((not s3)) ())
(((not s2)) (s2) ())
(((not s3)) (s3) ())
(((not s1)) ((and s3 s2)) ())
(((> s2 s1)) ((and s4 s2)) ())
((s4) ((> s1 s4)) #t)
((s1) ((or s1 s2)) #t)
(((> s1 s3)) ((or s3 s4)) ())
(((and s4 s3)) ((> s2 s4)) #t)
(((or s4 s4)) ((and s3 s3)) ())
(((not s2)) (s1) ())
(((or s4 s4)) (s1) ())
(((and s4 s4)) ((> s1 s2)) ())
((s3) ((or s1 s2)) ())
(((> s1 s2)) ((or s1 s4)) ())
(((and s2 s4)) ((and s4 s1)) ())
((s4) ((and s4 s1)) ())
((s3) ((or s3 s4)) #t)
(((> s2 s3)) (s4) ())
(((or s3 s4)) (s4) ())
(((and s4 s4)) ((not s1)) ())
(((and s3 s1)) ((not s3)) ())
((s1) ((not s2)) ())
(((and s3 s3)) ((and s4 s4)) ())
((s3) ((not s2)) ())
(((or s1 s4)) ((> s4 s2)) ())
(((or s2 s3)) ((and s3 s2)) ())
(((not s4)) ((> s2 s1)) ())
(((or s4 s1)) ((or s4 s3)) ())
(((> s1 s4)) ((> s1 s3)) ())
(((or s4 s1)) ((> s1 s3)) ())
(((and s4 s3)) (s4) #t)
(((> s2 s3)) ((and s2 s2)) ())
(((or s4 s3)) ((not s4)) ())
((s1) ((and s3 s4)) ())
(((and s4 s1)) ((not s4)) ())
((s3) ((or s1 s1)) ())
(((or s2 s3)) ((not s2)) ())
(((or s4 s3)) ((not s2)) ())

; case 4
(((not (or s3 s3))) ((not (or s2 s3))) ())
(((or (and s4 s2) (or s3 s2))) (s3) ())
(((> (and s2 s4) (> s5 s2))) ((> (> s1 s5) (> s3 s2))) ())
(((or (or s5 s2) (and s4 s2))) ((not (or s3 s3))) ())
(((not s1)) ((and (> s5 s1) (not s3))) ())
(((> (not s4) (or s5 s1))) (s2) ())
(((or (not s5) s2)) ((or (not s2) (> s3 s5))) ())
(((not (not s4))) ((> (and s1 s5) (or s5 s4))) #t)
(((and (or s5 s4) s3)) ((or (and s3 s1) (or s2 s4))) ())
(((not (not s1))) ((or (> s5 s1) (> s3 s4))) #t)
(((and (not s5) (and s5 s3))) (s5) #t)
((s5) ((not (and s1 s5))) ())
(((or (or s3 s4) (not s2))) (s4) ())
(((not (and s1 s3))) ((not (and s3 s3))) ())
(((> (not s2) (or s2 s3))) ((or (or s3 s1) (not s2))) ())
(((not (or s5 s5))) (s3) ())
(((and s1 s3)) ((or (not s1) (or s3 s3))) #t)
((s4) ((not (not s4))) #t)
(((not (and s1 s1))) ((not (or s3 s4))) ())
(((and (and s1 s5) (> s1 s3))) (s1) #t)
((s3) ((> (or s2 s5) s5)) ())
(((not s3)) ((not s2)) ())
(((not s1)) (s4) ())
(((> (not s4) s2)) ((> (and s2 s5) (and s3 s4))) ())
(((not (not s5))) ((not (not s1))) ())
((s3) ((and (or s5 s1) (not s1))) ())
((s1) ((not (and s4 s3))) ())
(((and (not s2) (and s3 s2))) ((and (and s4 s3) (> s3 s5))) #t)
(((or (or s5 s4) (or s5 s1))) ((> (not s2) (or s1 s4))) ())
(((> (> s2 s1) s3)) ((> (and s3 s4) (not s3))) ())
(((or (not s3) (not s2))) ((not (not s1))) ())
(((> (not s2) (or s1 s2))) ((> (and s3 s1) (not s1))) ())
(((and s3 (and s1 s2))) ((and (not s3) (> s3 s4))) ())
(((> (or s4 s3) (not s1))) ((or s4 s5)) ())
((s3) ((> s5 (not s2))) ())
((s4) ((> (> s1 s5) (and s5 s1))) ())
(((> (and s1 s1) (or s3 s5))) (s1) ())
(((> (and s1 s5) (not s5))) ((> s5 (> s1 s2))) #t)
((s1) ((or (or s4 s2) (or s4 s5))) ())
(((or (> s5 s3) (and s1 s4))) ((> (or s3 s3) (not s4))) ())

; case 5
(((> (and (not (or (and s4 s2) (or s10 s1))) (not (> (not s8) (not s9)))) (not (or (not s4) (not (not s4)))))) ((> (and s9 (and (or (> s10 s6) (not s2)) (or s4 (and s4 s2)))) (and (not s3) s5))) ())
(((or (not s2) (not (or s6 (and (not s2) (not s3)))))) ((or (and (and (not (> s3 s9)) (and (or s2 s7) (and s5 s1))) (not (or (or s3 s10) (or s9 s6)))) (not s6))) ())
(((and (not (> (not (not s8)) (or (not s9) (not s2)))) (> (and s9 (or (> s10 s8) (not s2))) (> s1 (and (> s7 s6) (and s1 s3)))))) ((and (not s7) (> s7 s10))) ())
((s3) ((not (or (not s6) s10))) ())
((s8) ((not (or (and s8 (or (not s3) (not s1))) (not (or (> s3 s4) (> s4 s6)))))) ())
((s8) (s10) ())
(((or (or (or (or s9 (not s4)) s2) s4) (or (> (not (or s7 s7)) (and s10 (and s8 s10))) (or (and (or s1 s3) (not s9)) (> (and s9 s8) (not s5)))))) ((> (or (and (not s2) s3) (> (or (> s3 s2) (or s4 s6)) (not (> s7 s6)))) (> (and (and (not s4) (not s3)) (> (> s8 s4) (> s4 s1))) (not (not (and s1 s10)))))) ())
(((not s6)) ((and s10 (not (or (> (or s5 s8) s2) (> (> s3 s1) (or s7 s5)))))) ())
(((not s10)) (s1) ())
(((and (or (not (> (not s3) (> s8 s10))) (or (or (or s4 s4) (or s1 s6)) (or (> s6 s2) (or s9 s10)))) (not (> (> (or s3 s6) s4) (or (or s2 s9) (and s9 s5)))))) ((or s4 s9)) ())
(((and (and (> (not (> s1 s5)) (and s3 s7)) (or (or s8 (or s4 s1)) (and (or s5 s8) (not s4)))) (and (and (not s2) s7) (> (not (and s9 s7)) (and s10 (or s7 s9)))))) ((> (> (not (and (> s4 s1) (or s4 s4))) (or s4 (> (> s5 s2) (and s2 s6)))) (and s6 (and (and (and s4 s9) (or s10 s5)) (and (and s10 s7) (and s4 s4)))))) ())
(((> (not (> (and (> s9 s10) s10) (> (or s6 s5) s3))) s1)) (s6) ())
((s9) ((not (> (not (or (not s5) (> s7 s6))) (> (> s3 (> s7 s1)) s2)))) ())
((s7) ((and (or s10 (or (not (or s7 s2)) (not (or s9 s9)))) (or (and s1 (not (not s9))) (> (and (or s2 s9) s3) s6)))) ())
(((and s6 (not (not (> (> s6 s10) (or s3 s10)))))) ((> (not s7) (> (and (> s4 (and s9 s2)) (or (and s1 s10) (> s2 s4))) (or (not (not s3)) (or s7 (> s10 s2)))))) ())
(((> (> (not (and (or s6 s8) (or s3 s7))) (or (or (not s3) (or s3 s10)) (not (> s7 s10)))) (not (and (and (and s9 s5) (and s6 s4)) (and (or s8 s10) (and s10 s6)))))) (s8) ())
(((not (and s4 (or (not (and s8 s3)) (and (or s2 s7) (or s8 s4)))))) ((or (or s4 (and (not s2) (or (not s1) (or s3 s3)))) (> (> (or (and s4 s1) (not s7)) (or (or s1 s5) s2)) (not (or s4 (and s8 s8)))))) ())
((s7) (s4) ())
((s9) ((and (and (> (> (> s2 s1) s5) s8) (and (> (and s3 s6) (not s10)) (not s6))) (and (not (> s6 (and s7 s2))) (and (> s4 (or s9 s3)) (and (and s5 s7) s1))))) ())
(((not (not (> (and s8 (or s1 s9)) (> (not s1) s7))))) (s8) ())
(((and (and (and (or (and s8 s4) (or s1 s1)) (or (and s7 s7) (not s7))) (not s8)) (not s1))) ((not (or (not (and s6 (and s4 s7))) (> s10 (> s7 (and s9 s9)))))) #t)
(((and (or s7 (and (and (or s1 s4) s1) (> (not s10) (and s9 s7)))) s8)) (s6) ())
(((or (and (and (and (and s5 s6) (and s5 s4)) (and (or s2 s6) (or s10 s10))) (> (> s4 (> s2 s4)) (not (not s8)))) (or (not s2) (not (> (and s7 s1) (> s7 s3)))))) ((or (not (or (and (and s2 s2) s9) (and (or s1 s10) s2))) (and s4 (or (> (not s8) (not s10)) (and (or s2 s1) (and s6 s10)))))) ())
(((> (> (and (and (or s8 s3) (not s1)) s6) (> (or (> s4 s10) s2) (or (not s1) (not s10)))) (and (> (not (and s6 s9)) (or (or s1 s8) (and s8 s2))) (or (or (> s7 s3) (or s9 s3)) s3)))) ((not (not (not s3)))) ())
(((and (> s3 (not (and (and s9 s1) (or s7 s5)))) (or s3 (> (and (not s3) (> s7 s6)) (or (or s10 s8) (or s10 s4)))))) (s2) ())
(((and (or (and (or (not s5) (> s8 s3)) (not (or s1 s6))) (> s7 (> (not s6) (or s1 s6)))) s2)) ((not (not (> (or (and s10 s8) (and s4 s5)) (and (or s4 s6) s5))))) ())
((s6) ((and (not s8) (and (not (or (not s1) s1)) (> s2 (not (and s1 s6)))))) ())
(((> (not (not s7)) (and (not (and (not s10) (and s5 s9))) (> (or (or s9 s3) s10) (not (and s9 s9)))))) ((not s10)) ())
(((not (or (and (and (> s9 s10) (and s8 s8)) (not s10)) (and (and (or s6 s2) (and s7 s8)) (or (not s9) (and s10 s4)))))) ((or s1 (not s7))) ())
((s7) ((> (> (> (> (or s3 s8) (not s1)) (and (and s7 s9) (not s3))) s9) (and (> (> (> s7 s5) (and s3 s3)) s5) (and (and (not s9) (or s6 s1)) (and (and s8 s7) (> s8 s7)))))) ())

; case 6
(((and s1 (not (or (and (> s3 s2) (not s10)) s10)))) ((and (not (or (> (or s7 s6) (or s2 s2)) s10)) (and (> (not (and s2 s10)) (> (not s7) (> s2 s8))) (not (or (or s1 s3) s8))))) ())
(((not (or (> (not s5) (not (not s7))) (not (> (or s7 s8) (or s3 s6)))))) ((not (not s6))) ())
(((> (> (and (not s7) s1) (or (or (not s3) (and s4 s10)) (and s10 (or s2 s4)))) s2)) ((not (> (> (> s8 (and s7 s5)) (not (not s9))) (> (> s5 s6) (> s5 (not s5)))))) ())
(((> (or (or (not s9) (and (and s9 s2) (not s10))) s6) s4)) ((or (> (not (not (and s9 s8))) (and (not s5) s8)) (> (> (or (or s6 s7) (or s2 s2)) (> (and s10 s9) s1)) s8))) #t)
(((> (and (> (> (> s6 s7) s9) (and s5 (not s3))) (not (not s4))) s2)) ((not (> (and (> (not s3) (and s1 s1)) s7) (> (not (not s2)) (> (or s6 s4) s6))))) ())
(((or s2 (and s2 s9))) ((and (or s4 s8) (or (> (> (and s5 s3) (or s3 s3)) s10) (and (or s8 (not s7)) (and (or s4 s7) (and s5 s4)))))) ())
(((> s5 (or (> s10 (or (and s2 s8) (and s1 s4))) (> (> s8 s2) (> (not s3) (> s5 s4)))))) ((not s9)) ())
(((and (not (not (not (> s7 s9)))) (and (and (and s10 (or s4 s10)) (not (not s4))) (not s4)))) ((or (not s7) (and (or (> (or s1 s2) (> s3 s8)) (or (or s7 s7) (and s7 s1))) (or (or s10 (> s10 s8)) (not (not s8)))))) #t)
(((not s2)) ((and (not (> (and (> s4 s8) (not s6)) (> s6 (and s1 s8)))) (not s4))) ())
(((> s3 s9)) ((> (> (not s10) (and (and (or s4 s8) (and s8 s3)) s5)) (or (> (or (not s3) (and s9 s9)) s1) (and (not (or s10 s2)) s2)))) ())
(((> (and (or s2 (not (> s9 s5))) (or (or (> s9 s6) (not s6)) (and (and s2 s10) (> s9 s8)))) s4)) ((or (or (> (and s2 (and s10 s6)) s7) (not (and (and s1 s8) s7))) (or (> (and (> s4 s1) (and s9 s4)) s9) (> (and s10 (> s7 s8)) s8)))) #t)
(((not (not (or (not (or s4 s3)) s4)))) ((or (not s5) (and (and s10 (not (or s1 s9))) (> (not (and s4 s4)) (and s7 (or s7 s1)))))) ())
(((not (not (not (or (or s3 s7) (or s9 s10)))))) ((or (and (and (and (not s8) (and s10 s4)) (not (or s4 s3))) (and (or (or s7 s5) (or s8 s7)) (or (or s8 s7) (and s3 s7)))) (or (or (and (> s8 s2) (and s6 s2)) s4) (> s8 s1)))) ())
(((> (or (and (or (> s6 s4) s8) (and (> s2 s10) s1)) s10) (> s4 (not (not s6))))) ((not (> (and (not (> s6 s1)) (and (not s3) s3)) (and (and (and s7 s6) (or s4 s2)) (> (> s10 s4) s2))))) ())
(((> (> (> s9 (> (> s4 s5) (> s1 s4))) (> (or (or s1 s7) (> s8 s4)) (or (> s8 s5) (> s1 s9)))) (> (and (not (not s9)) (not (and s10 s6))) (or s5 (and (or s2 s4) (and s4 s7)))))) ((not (or (> (not s9) (and s10 s5)) (> (not (not s3)) (> (not s4) (and s3 s1)))))) ())
(((not (and (not (> s9 (> s9 s2))) (> (and (not s1) (or s10 s3)) (not (> s3 s4)))))) ((> (> (> (and (> s2 s3) (and s8 s3)) (and (not s10) (or s10 s5))) (or (not (not s1)) (or s9 s1))) (and s6 (not (and (> s1 s5) (and s1 s1)))))) ())
(((or s5 (not (and (and (> s1 s10) (> s5 s8)) (or (not s10) (not s6)))))) ((and (or s1 (> (not (> s8 s10)) s5)) s6)) ())
(((> (and s9 s5) (> s6 s8))) ((and (not (> (not s8) (or (or s2 s4) (and s4 s10)))) (and s5 (not (not (not s9)))))) ())
(((> (> (> (or (and s10 s7) s3) (not (or s1 s9))) (> (> (or s6 s6) s6) s6)) (and (> (or (or s9 s5) (> s6 s7)) (> s6 (not s10))) (and s8 (and (> s7 s6) s5))))) ((and (not (and s5 (or (or s6 s6) s9))) (or (or (or (or s9 s8) (and s7 s2)) (and (not s6) (or s10 s10))) (and (and s4 (or s4 s2)) (> (or s2 s10) s5))))) ())
(((and (or s1 (> (and (and s5 s5) (or s10 s9)) (> (and s5 s5) (not s10)))) (or s4 (and (> (> s8 s6) (or s9 s9)) (not s6))))) ((> s3 (> (not s8) (or (and (or s5 s7) (and s10 s3)) s8)))) ())
(((not (not (> (or s5 (> s7 s6)) (not (and s10 s1)))))) ((not (and (and s5 (not s1)) (and (or s8 (or s6 s3)) s6)))) ())
(((and (or (> (and (and s4 s1) (or s7 s2)) (not (not s9))) s7) (> (and (and (or s5 s1) (not s4)) (> (and s7 s10) (> s6 s2))) s4))) ((or (or (> (and (or s6 s10) s2) (> s6 s4)) (and s1 (> (or s2 s5) (> s5 s6)))) (> (and s2 (and s5 s2)) (and (not (or s5 s8)) (and (not s5) (and s3 s2)))))) #t)
(((not (not s4))) ((not s4)) ())
(((> (or (or (> (or s10 s2) s8) (not (not s1))) s8) (> s3 (and (and (or s9 s10) (and s6 s2)) (and (not s3) (or s8 s7)))))) ((not (not s3))) ())
(((and (or (and s9 s9) (and (or (not s7) (or s5 s6)) (not s6))) s2)) ((> (not (and (and (or s9 s1) (and s9 s4)) (not (and s3 s1)))) (and (not (not s1)) s3))) ())
(((and (not (or (or s5 s9) (> (not s10) (not s4)))) (> (not (and (not s6) s9)) (> (not s3) s10)))) ((and s6 (and (and s2 (> (> s1 s10) (and s5 s8))) (and (and (and s8 s10) (> s8 s6)) (or (not s5) (not s9)))))) ())
(((> (or s8 (and s7 (not (> s6 s1)))) (or (> (and (> s3 s4) (or s1 s5)) (or (> s6 s9) (not s5))) (and (and s10 s8) (or (and s10 s4) (not s9)))))) ((or (not (not (and (and s5 s7) (not s4)))) (and (not (or (> s9 s6) (and s7 s3))) s8))) ())
(((and (or (and (or s7 s9) (not (> s3 s6))) (not s9)) (or (and (not (> s7 s1)) (or (not s7) (and s3 s8))) (not (and (and s8 s3) (> s7 s8)))))) ((and s3 (> s10 s7))) ())
(((> s3 (or (or (> (> s1 s4) (and s9 s6)) s5) (not (not s1))))) ((not (and (and (> (not s8) s7) s6) s10))) ())
(((not (and (and (or (> s9 s5) s6) (not (> s8 s5))) (or (> (or s3 s2) (not s6)) s5)))) ((> (and s9 (> (not s4) (and (> s9 s5) (not s4)))) (and (> (not s8) s10) (not (> (not s5) (> s1 s8)))))) ())

; case 7
(((> s5 (or (> s2 s5) (or s10 s10 s10) (or s2 s5 s8)))) ((or (and (not s10) s6 (or s5 s9 s8)) (not s3) (not (and s7 s9 s9)))) ())
((s7) (s9) ())
(((> (or s1 (and s9 s8 s3) (not s8)) s5)) ((not (> s7 (> s2 s10)))) ())
(((and (not (not s7)) (or s4 (and s6 s7 s7) (not s1)) (or (> s9 s3) (or s7 s3 s7) s3))) ((> s9 (> (or s4 s3 s8) (not s5)))) ())
(((not (and (not s7) s7 (and s2 s8 s6)))) ((or (or (or s10 s5 s5) s4 (and s9 s7 s1)) s5 s9)) ())
(((not (and (and s1 s6 s9) (and s2 s1 s7) (> s8 s9)))) ((not (> s6 s2))) ())
(((or (not s9) (not (> s10 s3)) (or (and s2 s7 s8) (not s7) s4))) (s2) ())
(((or (or (or s9 s6 s3) (> s5 s10) (and s10 s4 s1)) s8 s3)) ((or s10 (and s10 (and s10 s4 s9) (not s8)) (> (> s4 s9) (and s8 s8 s6)))) ())
(((and (> s5 (not s3)) (or (> s7 s8) (not s10) (and s10 s6 s6)) (> (and s9 s5 s4) (not s3)))) ((> (and (or s2 s7 s8) (> s9 s4) s1) s8)) ())
(((not (> (> s1 s6) (and s4 s6 s9)))) ((or (not (not s10)) (> (not s5) (and s7 s5 s10)) (not s10))) #t)
(((> s9 s4)) ((or (or (and s9 s3 s8) (or s6 s6 s5) (or s7 s10 s9)) (and s5 (> s3 s8) (not s4)) (not (not s6)))) ())
(((not s2)) ((not (> (not s9) (and s5 s10 s7)))) ())
(((> (and s5 (and s6 s8 s9) (> s2 s4)) (not (or s3 s6 s5)))) ((> (and (or s8 s4 s10) (> s8 s6) (and s4 s7 s6)) (or (> s7 s4) (not s1) (and s7 s2 s6)))) #t)
((s1) ((> (not (not s2)) (or (or s9 s4 s3) (> s7 s5) (and s3 s8 s1)))) ())
((s4) ((and (and (or s4 s3 s5) (or s4 s1 s5) (or s5 s2 s10)) (and (or s1 s2 s7) (> s5 s3) (not s9)) (or s2 (not s7) (> s8 s4)))) ())
((s7) ((not s8)) ())
((s1) ((and (or s1 (not s5) (and s9 s2 s1)) s3 (not (or s8 s2 s3)))) ())
((s7) ((or (or s1 (or s8 s7 s8) s7) (and (and s2 s8 s9) (or s1 s10 s9) (or s3 s3 s5)) s1)) #t)
((s3) ((and (> s9 (not s6)) (> (not s9) (or s10 s5 s6)) (> (not s4) s3))) ())
(((and s4 (and (> s1 s6) (not s9) (not s3)) (and (not s7) s2 s4))) ((or (not (> s9 s5)) (or (not s9) (or s7 s5 s6) s4) (not (> s10 s5)))) #t)
(((> (not s2) (and (or s6 s4 s5) (and s3 s5 s9) s8))) (s2) ())
(((> (and (or s3 s2 s8) s9 (not s7)) (not (and s1 s9 s1)))) (s2) ())
(((and (or (> s2 s8) (> s3 s8) (and s6 s8 s6)) (or (not s8) s5 (or s7 s8 s3)) (> (or s10 s7 s10) s3))) ((not (or (not s4) (or s3 s8 s10) (and s7 s10 s4)))) ())
(((or (and (and s8 s10 s4) (> s4 s9) (not s9)) (> (not s1) (not s6)) (not (or s5 s6 s9)))) (s7) ())
(((or (or (> s3 s2) (not s8) s9) (> s10 (not s2)) (not (> s4 s1)))) (s3) ())
(((> (or (or s2 s9 s1) (and s3 s3 s2) (or s5 s3 s10)) s5)) ((> (> (or s7 s1 s8) s2) (and (or s8 s8 s9) (> s7 s5) (> s3 s10)))) ())
(((not (and s2 (not s5) (> s8 s7)))) ((and s7 s7 (> (and s8 s3 s10) (and s8 s3 s4)))) ())
(((or s8 s7 s3)) ((not (and s2 s10 (> s9 s2)))) ())
(((not s1)) (s4) ())
(((> (> (not s5) (or s9 s9 s1)) s8)) ((or (or s7 (or s7 s6 s4) (not s2)) (not (and s7 s3 s9)) (and (or s9 s4 s9) (and s7 s6 s7) (> s4 s7)))) #t)

; case 8
(((> s3 s8)) ((or s9 s3 s9 s8 s6)) ())
(((and s6 s1 s3 s8)) ((not s3)) ())
(((> s7 s4)) ((or s3 s5)) ())
(((and s3 s3 s5 s10 s3)) ((not s10)) ())
(((or s4 s9 s1)) ((and s7 s5 s5 s1)) ())
((s8) ((not s10)) ())
(((not s8)) ((not s2)) ())
(((not s10)) (s9) ())
(((not s1)) ((> s10 s5)) ())
(((or s1 s5 s6 s4 s9)) (s2) ())
(((not s9)) ((and s1 s6 s10 s1 s3)) ())
(((> s10 s8)) ((or s2 s6 s4)) ())
((s2) ((and s2 s4 s6 s6)) ())
(((or s1 s7 s6 s10 s2)) ((and s2 s7)) ())
(((not s6)) ((> s3 s2)) ())
(((> s5 s10)) ((or s8 s2)) ())
(((not s1)) (s5) ())
(((or s5 s8 s8 s10 s7)) ((not s10)) ())
(((> s2 s7)) ((or s4 s6 s7 s5)) ())
(((and s4 s10 s6 s10 s3)) ((> s9 s6)) #t)
((s1) ((and s9 s1 s6 s10 s3)) ())
(((or s2 s6 s4 s7 s3)) ((or s8 s7 s7 s8)) ())
(((and s3 s10 s7)) ((and s8 s4)) ())
((s9) ((or s4 s7 s6 s3)) ())
((s5) ((not s6)) ())
(((> s9 s2)) ((> s10 s2)) ())
(((> s6 s9)) ((or s3 s7)) ())
(((not s5)) (s9) ())
(((and s5 s1)) ((not s4)) ())
((s2) (s9) ())
(((> s7 s8)) ((and s5 s5 s9)) ())
(((and s8 s3 s9)) ((> s6 s2)) ())
(((and s4 s7 s8 s3 s2)) ((> s6 s2)) #t)
((s4) ((or s1 s2)) ())
((s9) ((not s7)) ())
(((and s8 s2 s2)) ((not s8)) ())
(((and s1 s6 s2)) ((> s3 s8)) ())
(((or s1 s4)) ((> s2 s5)) ())
(((> s8 s6)) ((and s2 s5 s2 s10 s10)) ())
(((and s9 s8 s9 s9 s8)) (s7) ())
((s3) ((and s7 s5 s5 s10 s4)) ())
(((or s2 s9)) ((or s9 s4 s3 s8)) ())
(((not s3)) ((not s7)) ())
((s3) (s1) ())
(((and s2 s9)) ((or s5 s7)) ())
((s1) ((not s10)) ())
(((or s8 s10 s8 s9)) ((and s2 s2 s4)) ())
((s6) ((or s8 s2)) ())
(((> s9 s10)) ((and s6 s2 s4)) ())
(((and s9 s8 s4 s9)) ((> s3 s4)) #t)

; case 9
(((or (or (> s3 s4) (not s6) (and s5 s1 s6) (or s7 s3 s6 s10 s7)) s9 (or (> s8 s6) (and s4 s8) (or s3 s4 s5 s8)))) ((> s1 (and (not s3) (and s10 s2 s8 s8 s10) (or s6 s10 s3 s2) (and s6 s1 s7 s6 s8)))) ())
(((and (and (> s7 s9) (or s10 s4)) (> (or s1 s7 s4) (> s8 s9)) (and s10 (and s2 s3 s5) (and s10 s2)) (not (and s10 s7)))) ((or (not (> s2 s10)) (not s3) (or (not s6) (or s10 s10 s2 s7) (> s3 s1) s5) (or (or s9 s6 s9) (and s10 s8 s9 s5)))) #t)
(((> (and (> s1 s3) (and s8 s2 s5 s7) (or s2 s4 s7 s8 s4) (> s6 s3)) (not (> s4 s1)))) ((> (> (not s6) (not s10)) (not (or s10 s7 s8)))) ())
(((not (> (not s2) s5))) ((> (or (and s5 s10) (not s5) (not s10) (and s10 s7)) (or s9 s8 (not s10)))) ())
(((or (and (and s6 s3) s3 s3) (> (> s7 s1) (> s6 s10)) s1)) ((or s4 (> (> s6 s1) (or s6 s5 s7)) (and (and s3 s6) (not s5)))) ())
(((or s9 (> (not s9) (or s2 s7 s6 s3)) s9 (and s7 (> s9 s5) s7 (> s10 s4)))) ((or (not (> s3 s4)) s2 (not (or s5 s6)))) ())
(((> (and s8 s3 (not s1) (not s4)) (> (and s9 s6) s2))) ((not (and (or s3 s6) (not s2) (not s5) (> s9 s7)))) ())
(((> (or (and s3 s1 s8) (or s4 s9 s4 s5)) (not (not s7)))) ((> (> s8 s10) (> (and s10 s4 s4 s10) s9))) ())
(((not (and (not s9) (not s4) (and s2 s1 s6 s2 s5) (or s1 s2 s1 s2) (or s2 s3 s10)))) ((or (not (> s2 s8)) (not (or s4 s10 s8 s5)) (not (or s5 s5 s5 s7 s10)))) ())
(((or (> (or s1 s3 s8) s10) s2)) ((or (or (and s10 s5 s2 s7 s3) (and s3 s10 s7) (> s8 s9) (or s3 s1 s10 s10 s10)) (and (and s6 s7) (and s6 s6 s1 s3) (not s8)))) ())
(((and (or (and s9 s1 s4) (not s6) (or s3 s7 s9) (and s1 s9 s1 s10) (not s9)) (not (and s7 s5 s5 s10)))) ((or (or (and s10 s2 s5 s6 s7) (and s1 s3 s3) (> s3 s7)) (or (and s4 s1 s9) (> s10 s7) (> s1 s8) (not s8)))) #t)
(((not (and (and s9 s5 s10) (or s10 s3 s4 s7) (> s9 s10)))) ((not (> (not s8) (or s6 s6)))) ())
(((and (not (and s9 s9)) (or (> s5 s1) (or s5 s8 s10 s1) (or s6 s6 s8 s6 s8)))) ((and (or s3 s6 s2 (> s5 s8) (or s3 s3 s8 s2 s7)) s10 (not (and s2 s4 s2 s9)))) ())
(((not (not (and s4 s6 s6 s1)))) ((> (and (and s3 s2) s1 (and s6 s9 s10) (and s2 s10 s2 s3 s8)) (and (or s4 s2 s9 s10 s3) (or s10 s10 s3)))) #t)
(((and (not (and s7 s8)) (and (and s3 s2) (> s3 s4) (not s2) s1) (not (or s1 s4 s8)))) ((not (> (> s1 s4) (and s10 s5 s5 s5 s1)))) #t)
(((or (and (and s5 s10 s2 s4) (and s2 s10) (not s9)) s1)) ((not s10)) ())
(((> (> (> s9 s1) (not s4)) (> (not s6) (not s8)))) ((and (and (not s8) (or s10 s5 s5 s5) s6 (and s3 s4 s7 s6) (and s3 s2 s8)) (> (or s1 s6 s10 s10 s7) (or s10 s1 s8 s2 s1)) (or (and s10 s9 s1) (and s8 s1 s8)) (or (and s8 s5 s7 s5 s9) s1 (> s10 s9) s7 s5) s8)) ())
(((or (> (and s5 s2) s5) s9 (> (or s8 s3) (and s2 s2 s2)))) ((> (not (and s2 s6 s9)) (and (not s4) (or s9 s7 s9 s10) s9 (> s8 s3)))) ())
(((not (or (or s10 s2 s10 s8 s3) (not s2)))) ((not (not (or s2 s6)))) #t)
(((not (or (and s5 s6) (> s1 s6) (> s5 s6) (not s7) (not s5)))) ((not (or (> s1 s3) (or s2 s10 s10 s1 s2) (not s1) (or s1 s6 s8)))) ())
(((and s2 (> s6 s2) (and s2 (and s1 s4 s1 s10) (> s6 s5) (not s7) (or s7 s9 s10)))) ((and (> s1 (> s10 s2)) (> (> s4 s6) s3) (or (not s9) (and s9 s1 s7) s7))) ())
(((not (> (> s5 s3) (not s3)))) ((not (and s9 (not s7) s1))) ())
(((or (not (and s5 s2 s7)) (and (or s10 s7 s7 s7) (and s1 s10 s2 s3)) s5 (not (or s5 s3 s6)) (and (not s10) (and s1 s4 s5 s6 s10) (not s6) (> s9 s6)))) ((not s9)) ())
(((> (not (> s10 s3)) (or s8 (and s6 s8 s6 s7 s1)))) ((not (or (and s2 s9) (and s4 s5 s4)))) ())
(((or (or (and s1 s6 s4 s7 s3) s9 (and s10 s5) (or s6 s4) (> s6 s9)) s9 (and (or s7 s9 s3) (or s3 s5 s5 s5 s8)) (or s5 (and s3 s5 s6) (and s7 s8 s9) (not s9)) (> (> s10 s8) s9))) ((not (and (or s8 s6 s2) (or s7 s8 s7) (not s10) (and s4 s1 s7)))) ())
(((or (not (not s2)) (and s9 (not s9)))) ((not (and (or s3 s4 s4 s8) (not s9) (> s3 s8) (or s10 s5 s10) (or s2 s3 s9 s10)))) ())
(((and (> s6 (or s3 s7)) (> (or s9 s2 s4 s1 s4) (or s2 s2)) (> (not s4) (> s6 s1)))) ((or s9 s6 (or (or s4 s5 s5 s5 s10) (> s7 s10)))) ())
(((and (or s6 (or s9 s3) (or s4 s5 s10 s5 s7) s10 (or s10 s10 s4 s4)) s10 (> s9 (> s3 s1)) (and (or s10 s5) (and s1 s8 s2 s5 s9) (> s3 s2)) (or (not s6) (not s3) s2 s7))) ((or (or (or s6 s4 s6 s8 s7) (or s4 s1 s5) (not s8) (or s6 s2 s9 s5 s4) (and s4 s3 s9 s9 s7)) (> (not s6) (or s2 s1 s3 s6)))) #t)
(((not (not s5))) ((> (and (not s9) (and s4 s8 s6) (and s3 s8) (not s9) (or s6 s7)) (or s5 (or s7 s7)))) #t)
(((or (or (and s5 s4 s9) (> s4 s2) (or s6 s5 s5 s10)) s5 (and s8 (or s10 s7 s5) (> s4 s3)) (and (and s8 s1) (not s10)) (not (> s6 s4)))) ((and s10 (> (not s2) (> s7 s10)) (and (not s8) (not s5) (not s3)) (not (and s2 s1 s9 s9)) (not s6))) ())

; case 10
(((not (not (> s6 s14)))) (s15) ())
((s8) ((and (not (not s8)) (> (> s5 s12) (or s6 s2 s15)) (and (and s3 s15) s13 (or s7 s8 s9 s5) (and s15 s7 s12 s11 s13) (and s3 s6 s5 s11 s11)) (> (> s2 s12) (or s11 s2)))) ())
(((and (not (or s3 s11)) (> (not s2) (> s15 s7)) s7 (or (not s15) (and s11 s5 s8 s12 s14) (> s11 s14)) (and (not s11) (not s14)))) ((and (> (> s2 s4) (> s4 s14)) (or (not s1) s6 (and s1 s3 s5 s9 s15) (> s8 s3) (> s12 s6)) (not (and s6 s3)) (not (and s13 s11)))) ())
(((not s10)) ((not (> (or s8 s14) (not s1)))) ())
(((or (and (> s5 s8) (and s4 s7 s9 s4) (> s14 s4) s7 (> s6 s7)) (or (and s14 s11 s3 s1 s7) (and s12 s15) (or s15 s9 s7 s13 s2)))) ((and (not (or s1 s10 s11 s9)) (and (and s4 s6 s3) (not s11) (not s14) (or s11 s6 s15)) (or s12 s14 s13 s10) (or s10 s8))) ())
(((not (not s14))) ((or (and (not s12) s5 (and s8 s9) s11 (or s11 s5 s8)) (or (or s15 s12) (> s5 s10) (or s7 s13 s12 s2 s5) (and s11 s12 s2)) (> (not s10) (and s13 s12)) (> (not s7) s13) s13)) #t)
(((or (not (or s6 s8 s15 s4 s15)) s14 (> (> s8 s11) (and s5 s13 s5 s7)))) ((and (> (and s3 s2 s7 s6 s13) (or s6 s1 s4 s3)) (> (not s2) (or s2 s14 s4 s5 s10)) s2 (> (> s4 s3) (> s10 s8)) s5)) ())
(((or (and (not s12) (> s1 s5) (or s12 s5) (and s7 s7 s3 s9 s3)) (or (not s1) s6 (or s11 s6 s6 s1 s4) s2 (or s13 s15 s7 s1)))) ((> s2 s6)) ())
((s8) ((> (and (or s5 s13 s4) (or s11 s12 s4 s12) s8 (and s8 s2 s3 s10)) (and (> s9 s6) (or s8 s11 s1 s13 s15)))) ())
(((not (and (or s8 s2 s4) (and s5 s2) (not s3) (or s3 s14) (> s1 s5)))) ((or s7 (not (not s12)) s8 s3)) ())
(((or (> (and s14 s13) (not s14)) (or (> s15 s5) (> s8 s4) (not s2) s5) (> (or s12 s10 s6) (and s14 s12 s6 s9 s6)))) (s11) ())
(((not (or (or s5 s13 s14) (and s15 s9 s6 s6 s12) (and s14 s8 s3 s5)))) ((not (and s7 (and s7 s5 s5 s11) (or s14 s7 s10) (or s5 s1 s7 s14 s12) (> s11 s15)))) #t)
(((or (> (and s5 s9 s1) (and s15 s13 s15 s4 s4)) (or (or s12 s3 s5 s5 s2) (or s14 s9) (or s14 s9 s6 s14 s3)))) ((> (or (or s5 s10 s14 s13) (> s10 s12)) (> (not s8) (and s1 s6 s5 s9 s4)))) ())
(((> s10 (> s5 (not s5)))) ((> (and (or s13 s4 s10) (> s8 s11) (and s3 s4 s10 s12 s8) (and s8 s12 s11) (or s7 s8 s3 s11)) (or s11 (> s1 s3)))) #t)
((s8) ((and (and (and s8 s15 s9) (or s4 s6 s11 s12 s8)) (> (> s5 s8) (> s13 s8)))) ())
(((not (and (not s11) (or s6 s4)))) ((> (> (and s1 s4) (or s11 s10 s2 s4 s2)) s14)) ())
(((and s6 (not (and s7 s9 s15 s5 s1)) (or (> s2 s13) (or s4 s6 s2 s9) (or s10 s12) s3 (or s9 s4 s7 s13)) (and (not s7) (> s2 s13) (or s7 s10 s6 s12 s14)))) ((not (and (not s5) (> s10 s5) s14 (and s7 s7 s8 s13) s11))) #t)
(((or s4 (not (and s15 s13)))) ((not s7)) ())
(((and s1 (not (or s14 s3 s6 s4)) (> (and s14 s6 s11 s1) (not s2)))) ((not s3)) #t)
((s8) ((> (or s13 (and s12 s10) (> s15 s4) (not s13)) s14)) ())

• sample solution 1
• sample solution 2
• sample solution 3