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