The dog is blue. The dog visits the tiger. The tiger visits the dog. If the tiger eats the dog and the tiger visits the dog then the tiger sees the dog. If the dog sees the tiger and the dog visits the tiger then the tiger visits the dog. If someone visits the tiger then they see the dog. If someone is green and they visit the tiger then the tiger is big. If someone eats the tiger then the tiger sees the dog. If the tiger is young then the tiger eats the dog. If someone sees the dog and they are green then the dog eats the tiger. If the dog eats the tiger and the tiger visits the dog then the dog is big.
The dog is blue.
("dog" "is" "blue" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If the tiger eats the dog and the tiger visits the dog then the tiger sees the dog.
((("tiger" "eats" "dog" "+") ("tiger" "visits" "dog" "+")) -> ("tiger" "sees" "dog" "+"))
If the dog sees the tiger and the dog visits the tiger then the tiger visits the dog.
((("dog" "sees" "tiger" "+") ("dog" "visits" "tiger" "+")) -> ("tiger" "visits" "dog" "+"))
If someone visits the tiger then they see the dog.
((("someone" "visits" "tiger" "+")) -> ("someone" "sees" "dog" "+"))
If someone is green and they visit the tiger then the tiger is big.
((("someone" "is" "green" "+") ("someone" "visits" "tiger" "+")) -> ("tiger" "is" "big" "+"))
If someone eats the tiger then the tiger sees the dog.
((("someone" "eats" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
If the tiger is young then the tiger eats the dog.
((("tiger" "is" "young" "+")) -> ("tiger" "eats" "dog" "+"))
If someone sees the dog and they are green then the dog eats the tiger.
((("someone" "sees" "dog" "+") ("someone" "is" "green" "+")) -> ("dog" "eats" "tiger" "+"))
If the dog eats the tiger and the tiger visits the dog then the dog is big.
((("dog" "eats" "tiger" "+") ("tiger" "visits" "dog" "+")) -> ("dog" "is" "big" "+"))
The dog is blue.
True
1
proof
[(triple1)]
("dog" "is" "blue" "+")
triple1
The tiger does not visit the dog.
False
1
inv-proof
[(triple3)]
("tiger" "visits" "dog" "-")
triple3
The dog sees the dog.
True
2
proof
[(((triple2) -> rule3))]
("dog" "sees" "dog" "+")
((triple2) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog does not see the dog.
False
2
inv-proof
[(((triple2) -> rule3))]
("dog" "sees" "dog" "-")
((triple2) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is not big.
Unknown
inv-rconc
[@2: The dog is big.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("dog" "is" "big" "-")
The tiger eats the dog.
Unknown
rconc
[@1: The tiger eats the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "eats" "dog" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
@0: The dog is blue.[(triple1)] The dog visits the tiger.[(triple2)] The tiger visits the dog.[(triple3)] @1: The dog sees the dog.[(((triple2) -> rule3))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple3
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple2) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1