The cat visits the tiger. The dog eats the tiger. The dog visits the tiger. The rabbit does not eat the cat. The rabbit eats the tiger. The rabbit is big. The rabbit sees the cat. The rabbit sees the dog. The rabbit visits the dog. The tiger is cold. The tiger is red. The tiger sees the cat. The tiger sees the dog. The tiger sees the rabbit. The tiger visits the rabbit. If something is cold then it sees the rabbit.
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If something is cold then it sees the rabbit.
((("something" "is" "cold" "+")) -> ("something" "sees" "rabbit" "+"))
The rabbit sees the cat.
True
1
proof
[(triple7)]
("rabbit" "sees" "cat" "+")
triple7
The dog does not visit the tiger.
False
1
inv-proof
[(triple3)]
("dog" "visits" "tiger" "-")
triple3
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The dog visits the rabbit.
Unknown
random
[@0: The dog visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "rabbit" "+")
@0: The cat visits the tiger.[(triple1)] The dog eats the tiger.[(triple2)] The dog visits the tiger.[(triple3)] The rabbit does not eat the cat.[(triple4)] The rabbit eats the tiger.[(triple5)] The rabbit is big.[(triple6)] The rabbit sees the cat.[(triple7)] The rabbit sees the dog.[(triple8)] The rabbit visits the dog.[(triple9)] The tiger is cold.[(triple10)] The tiger is red.[(triple11)] The tiger sees the cat.[(triple12)] The tiger sees the dog.[(triple13)] The tiger sees the rabbit.[(triple14 OR ((triple10) -> rule1))] The tiger visits the rabbit.[(triple15)]
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple2
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple3
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
triple4
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple5
The rabbit is big.
("rabbit" "is" "big" "+")
triple6
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple7
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple8
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is red.
("tiger" "is" "red" "+")
triple11
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple12
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple13
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple14
((triple10) -> (rule1 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple15