The cow eats the lion. The cow eats the rabbit. The cow is red. The cow sees the lion. The cow visits the lion. The lion eats the rabbit. The lion is cold. The lion is kind. The rabbit does not eat the cow. The rabbit does not eat the tiger. The rabbit is not red. The rabbit visits the cow. The rabbit visits the lion. The tiger eats the rabbit. The tiger visits the rabbit. If someone eats the lion then the lion is not young. If the lion is red then the lion does not visit the tiger. If someone visits the cow then they see the lion. If the rabbit is not young then the rabbit is rough. If someone visits the tiger then they do not see the tiger. If someone visits the tiger then they see the tiger. If someone visits the rabbit and the rabbit does not eat the tiger then they do not see the rabbit. If the cow eats the rabbit then the cow does not see the rabbit.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The cow is red.
("cow" "is" "red" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
The rabbit is not red.
("rabbit" "is" "red" "-")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If someone eats the lion then the lion is not young.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "young" "-"))
If the lion is red then the lion does not visit the tiger.
((("lion" "is" "red" "+")) -> ("lion" "visits" "tiger" "-"))
If someone visits the cow then they see the lion.
((("someone" "visits" "cow" "+")) -> ("someone" "sees" "lion" "+"))
If the rabbit is not young then the rabbit is rough.
((("rabbit" "is" "young" "~")) -> ("rabbit" "is" "rough" "+"))
If someone visits the tiger then they do not see the tiger.
((("someone" "visits" "tiger" "+")) -> ("someone" "sees" "tiger" "-"))
If someone visits the tiger then they see the tiger.
((("someone" "visits" "tiger" "+")) -> ("someone" "sees" "tiger" "+"))
If someone visits the rabbit and the rabbit does not eat the tiger then they do not see the rabbit.
((("someone" "visits" "rabbit" "+") ("rabbit" "eats" "tiger" "~")) -> ("someone" "sees" "rabbit" "-"))
If the cow eats the rabbit then the cow does not see the rabbit.
((("cow" "eats" "rabbit" "+")) -> ("cow" "sees" "rabbit" "-"))
The rabbit does not eat the cow.
True
1
proof
[(triple9)]
("rabbit" "eats" "cow" "-")
triple9
The cow does not see the lion.
False
1
inv-proof
[(triple4)]
("cow" "sees" "lion" "-")
triple4
The cow does not see the tiger.
Unknown
inv-rconc
[@1: The cow sees the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "sees" "tiger" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
@0: The cow eats the lion.[(triple1)] The cow eats the rabbit.[(triple2)] The cow is red.[(triple3)] The cow sees the lion.[(triple4)] The cow visits the lion.[(triple5)] The lion eats the rabbit.[(triple6)] The lion is cold.[(triple7)] The lion is kind.[(triple8)] The rabbit does not eat the cow.[(triple9)] The rabbit does not eat the tiger.[(triple10)] The rabbit is not red.[(triple11)] The rabbit visits the cow.[(triple12)] The rabbit visits the lion.[(triple13)] The tiger eats the rabbit.[(triple14)] The tiger visits the rabbit.[(triple15)] @1: The cow does not see the rabbit.[(((triple2) -> rule8))] The lion is not young.[(((triple1) -> rule1))] The rabbit sees the lion.[(((triple12) -> rule3))] The tiger does not see the rabbit.[(((triple15 triple10) -> rule7))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
The cow sees the lion.
("cow" "sees" "lion" "+")
triple4
The cow visits the lion.
("cow" "visits" "lion" "+")
triple5
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple6
The lion is cold.
("lion" "is" "cold" "+")
triple7
The lion is kind.
("lion" "is" "kind" "+")
triple8
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
triple9
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
triple10
The rabbit is not red.
("rabbit" "is" "red" "-")
triple11
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple12
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple13
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple14
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple15
The cow does not see the rabbit.
("cow" "sees" "rabbit" "-")
((triple2) -> (rule8 % int1))
The cow does not see the rabbit.
("cow" "sees" "rabbit" "-")
int1
The lion is not young.
("lion" "is" "young" "-")
((triple1) -> (rule1 % int1))
The lion is not young.
("lion" "is" "young" "-")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
((triple12) -> (rule3 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
((triple15 triple10) -> (rule7 % int1))
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
int1