The cow sees the tiger. The rabbit sees the cow. The tiger eats the cow. If someone sees the tiger then the tiger likes the cow. If someone likes the rabbit and they like the cow then the rabbit is red. If someone likes the cow then they eat the rabbit.
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
If someone sees the tiger then the tiger likes the cow.
((("someone" "sees" "tiger" "+")) -> ("tiger" "likes" "cow" "+"))
If someone likes the rabbit and they like the cow then the rabbit is red.
((("someone" "likes" "rabbit" "+") ("someone" "likes" "cow" "+")) -> ("rabbit" "is" "red" "+"))
If someone likes the cow then they eat the rabbit.
((("someone" "likes" "cow" "+")) -> ("someone" "eats" "rabbit" "+"))
The cow sees the tiger.
True
1
proof
[(triple1)]
("cow" "sees" "tiger" "+")
triple1
The cow does not see the tiger.
False
1
inv-proof
[(triple1)]
("cow" "sees" "tiger" "-")
triple1
The tiger likes the cow.
True
2
proof
[(((triple1) -> rule1))]
("tiger" "likes" "cow" "+")
((triple1) -> (rule1 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger does not like the cow.
False
2
inv-proof
[(((triple1) -> rule1))]
("tiger" "likes" "cow" "-")
((triple1) -> (rule1 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger eats the rabbit.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("tiger" "eats" "rabbit" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger does not eat the rabbit.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("tiger" "eats" "rabbit" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The cow does not eat the rabbit.
Unknown
inv-rconc
[@1: The cow eats the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "eats" "rabbit" "-")
The rabbit is red.
Unknown
rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "red" "+")
The rabbit does not eat the rabbit.
Unknown
inv-rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "eats" "rabbit" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
@0: The cow sees the tiger.[(triple1)] The rabbit sees the cow.[(triple2)] The tiger eats the cow.[(triple3)] @1: The tiger likes the cow.[(((triple1) -> rule1))] @2: The tiger eats the rabbit.[(((((triple1) -> rule1)) -> rule3))]
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple2
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
((triple1) -> (rule1 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2