The dog eats the rabbit. The dog eats the tiger. The dog likes the rabbit. The dog visits the rabbit. The dog visits the tiger. The rabbit eats the dog. The rabbit eats the tiger. The rabbit is nice. The rabbit likes the tiger. The rabbit visits the dog. The rabbit visits the tiger. The tiger is nice. If someone visits the dog then the dog likes the rabbit. If someone is nice then they like the dog. If someone is young and rough then they visit the tiger.
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If someone visits the dog then the dog likes the rabbit.
((("someone" "visits" "dog" "+")) -> ("dog" "likes" "rabbit" "+"))
If someone is nice then they like the dog.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "dog" "+"))
If someone is young and rough then they visit the tiger.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "visits" "tiger" "+"))
The tiger is nice.
True
1
proof
[(triple12)]
("tiger" "is" "nice" "+")
triple12
The dog does not eat the rabbit.
False
1
inv-proof
[(triple1)]
("dog" "eats" "rabbit" "-")
triple1
The tiger likes the dog.
True
2
proof
[(((triple12) -> rule2))]
("tiger" "likes" "dog" "+")
((triple12) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger does not like the dog.
False
2
inv-proof
[(((triple12) -> rule2))]
("tiger" "likes" "dog" "-")
((triple12) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The dog likes the dog.
Unknown
rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "likes" "dog" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
@0: The dog eats the rabbit.[(triple1)] The dog eats the tiger.[(triple2)] The dog likes the rabbit.[(triple3 OR ((triple10) -> rule1))] The dog visits the rabbit.[(triple4)] The dog visits the tiger.[(triple5)] The rabbit eats the dog.[(triple6)] The rabbit eats the tiger.[(triple7)] The rabbit is nice.[(triple8)] The rabbit likes the tiger.[(triple9)] The rabbit visits the dog.[(triple10)] The rabbit visits the tiger.[(triple11)] The tiger is nice.[(triple12)] @1: The rabbit likes the dog.[(((triple8) -> rule2))] The tiger likes the dog.[(((triple12) -> rule2))]
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple3
((triple10) -> (rule1 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple4
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple5
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple6
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple7
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple8
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple9
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple10
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple11
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
((triple8) -> (rule2 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
((triple12) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1