The cow sees the rabbit. The rabbit eats the tiger. The tiger sees the cow. If something visits the rabbit and it visits the tiger then the tiger eats the cow. If something is cold and it visits the tiger then it eats the tiger. If something is nice and cold then it visits the rabbit. If the cow sees the tiger then the cow visits the tiger. If something visits the cow and the cow is round then it is young. If something eats the cow then it eats the rabbit. If something sees the rabbit then the rabbit eats the cow. If the rabbit is green and the rabbit sees the tiger then the rabbit visits the tiger.
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If something visits the rabbit and it visits the tiger then the tiger eats the cow.
((("something" "visits" "rabbit" "+") ("something" "visits" "tiger" "+")) -> ("tiger" "eats" "cow" "+"))
If something is cold and it visits the tiger then it eats the tiger.
((("something" "is" "cold" "+") ("something" "visits" "tiger" "+")) -> ("something" "eats" "tiger" "+"))
If something is nice and cold then it visits the rabbit.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "visits" "rabbit" "+"))
If the cow sees the tiger then the cow visits the tiger.
((("cow" "sees" "tiger" "+")) -> ("cow" "visits" "tiger" "+"))
If something visits the cow and the cow is round then it is young.
((("something" "visits" "cow" "+") ("cow" "is" "round" "+")) -> ("something" "is" "young" "+"))
If something eats the cow then it eats the rabbit.
((("something" "eats" "cow" "+")) -> ("something" "eats" "rabbit" "+"))
If something sees the rabbit then the rabbit eats the cow.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "eats" "cow" "+"))
If the rabbit is green and the rabbit sees the tiger then the rabbit visits the tiger.
((("rabbit" "is" "green" "+") ("rabbit" "sees" "tiger" "+")) -> ("rabbit" "visits" "tiger" "+"))
The rabbit eats the tiger.
True
1
proof
[(triple2)]
("rabbit" "eats" "tiger" "+")
triple2
The rabbit does not eat the tiger.
False
1
inv-proof
[(triple2)]
("rabbit" "eats" "tiger" "-")
triple2
The rabbit eats the cow.
True
2
proof
[(((triple1) -> rule7))]
("rabbit" "eats" "cow" "+")
((triple1) -> (rule7 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit does not eat the cow.
False
2
inv-proof
[(((triple1) -> rule7))]
("rabbit" "eats" "cow" "-")
((triple1) -> (rule7 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit eats the rabbit.
True
3
proof
[(((((triple1) -> rule7)) -> rule6))]
("rabbit" "eats" "rabbit" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
The rabbit does not eat the rabbit.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule6))]
("rabbit" "eats" "rabbit" "-")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
The tiger does not eat the cow.
Unknown
inv-rconc
[@2: The tiger eats the cow.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("tiger" "eats" "cow" "-")
The rabbit is young.
Unknown
rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "young" "+")
The cow does not eat the tiger.
Unknown
inv-rconc
[@1: The cow eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "eats" "tiger" "-")
The rabbit sees the tiger.
Unknown
random
[@0: The rabbit sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
@0: The cow sees the rabbit.[(triple1)] The rabbit eats the tiger.[(triple2)] The tiger sees the cow.[(triple3)] @1: The rabbit eats the cow.[(((triple1) -> rule7))] @2: The rabbit eats the rabbit.[(((((triple1) -> rule7)) -> rule6))]
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple2
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple3
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
((triple1) -> (rule7 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2