The cow does not see the lion. The lion visits the cow. The rabbit is not rough. The tiger sees the rabbit. If someone visits the lion then the lion sees the cow. If someone sees the rabbit then they visit the lion. If the rabbit needs the tiger and the tiger does not need the rabbit then the rabbit visits the lion. If someone sees the lion then the lion sees the tiger. If the lion sees the tiger then the tiger is green. If someone visits the cow and the cow is not blue then they see the cow. If someone visits the tiger then the tiger sees the cow. If someone sees the cow then the cow visits the rabbit.
The cow does not see the lion.
("cow" "sees" "lion" "-")
The lion visits the cow.
("lion" "visits" "cow" "+")
The rabbit is not rough.
("rabbit" "is" "rough" "-")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If someone visits the lion then the lion sees the cow.
((("someone" "visits" "lion" "+")) -> ("lion" "sees" "cow" "+"))
If someone sees the rabbit then they visit the lion.
((("someone" "sees" "rabbit" "+")) -> ("someone" "visits" "lion" "+"))
If the rabbit needs the tiger and the tiger does not need the rabbit then the rabbit visits the lion.
((("rabbit" "needs" "tiger" "+") ("tiger" "needs" "rabbit" "~")) -> ("rabbit" "visits" "lion" "+"))
If someone sees the lion then the lion sees the tiger.
((("someone" "sees" "lion" "+")) -> ("lion" "sees" "tiger" "+"))
If the lion sees the tiger then the tiger is green.
((("lion" "sees" "tiger" "+")) -> ("tiger" "is" "green" "+"))
If someone visits the cow and the cow is not blue then they see the cow.
((("someone" "visits" "cow" "+") ("cow" "is" "blue" "~")) -> ("someone" "sees" "cow" "+"))
If someone visits the tiger then the tiger sees the cow.
((("someone" "visits" "tiger" "+")) -> ("tiger" "sees" "cow" "+"))
If someone sees the cow then the cow visits the rabbit.
((("someone" "sees" "cow" "+")) -> ("cow" "visits" "rabbit" "+"))
The cow does not see the lion.
True
1
proof
[(triple1)]
("cow" "sees" "lion" "-")
triple1
The lion does not visit the cow.
False
1
inv-proof
[(triple2)]
("lion" "visits" "cow" "-")
triple2
The tiger visits the lion.
True
2
proof
[(((triple4) -> rule2))]
("tiger" "visits" "lion" "+")
((triple4) -> (rule2 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The tiger does not visit the lion.
False
2
inv-proof
[(((triple4) -> rule2))]
("tiger" "visits" "lion" "-")
((triple4) -> (rule2 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The lion sees the cow.
True
3
proof
[(((((triple4) -> rule2)) -> rule1))]
("lion" "sees" "cow" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The lion does not see the cow.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule1))]
("lion" "sees" "cow" "-")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The cow visits the rabbit.
True
4
proof
[(((((((triple4) -> rule2)) -> rule1)) -> rule8))]
("cow" "visits" "rabbit" "+")
((((((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int3
The cow does not visit the rabbit.
False
4
inv-proof
[(((((((triple4) -> rule2)) -> rule1)) -> rule8))]
("cow" "visits" "rabbit" "-")
((((((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int3
The rabbit does not see the cow.
Unknown
inv-rconc
[@1: The rabbit sees the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "sees" "cow" "-")
The tiger is green.
Unknown
rconc
[@2: The tiger is green.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("tiger" "is" "green" "+")
The tiger does not see the cow.
Unknown
inv-rconc
[@1: The tiger sees the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "sees" "cow" "-")
The cow sees the cow.
Unknown
rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "sees" "cow" "+")
The lion does not need the cow.
Unknown
inv-random
[@0: The lion needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cow" "-")
The rabbit needs the tiger.
Unknown
random
[@0: The rabbit needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "tiger" "+")
The tiger does not visit the rabbit.
Unknown
inv-random
[@0: The tiger visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "rabbit" "-")
The cow sees the tiger.
Unknown
random
[@0: The cow sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "tiger" "+")
@0: The cow does not see the lion.[(triple1)] The lion visits the cow.[(triple2)] The rabbit is not rough.[(triple3)] The tiger sees the rabbit.[(triple4)] @1: The tiger visits the lion.[(((triple4) -> rule2))] @2: The lion sees the cow.[(((((triple4) -> rule2)) -> rule1))] @3: The cow visits the rabbit.[(((((((triple4) -> rule2)) -> rule1)) -> rule8))]
The cow does not see the lion.
("cow" "sees" "lion" "-")
triple1
The lion visits the cow.
("lion" "visits" "cow" "+")
triple2
The rabbit is not rough.
("rabbit" "is" "rough" "-")
triple3
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple4
The tiger visits the lion.
("tiger" "visits" "lion" "+")
((triple4) -> (rule2 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
((((((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int3