The dog is round. The dog visits the mouse. The lion visits the tiger. The mouse eats the tiger. The mouse likes the dog. The mouse visits the dog. The tiger visits the lion. If something visits the dog then the dog likes the lion. If something likes the mouse then it visits the tiger. If something eats the mouse and it likes the mouse then it eats the lion. If something likes the lion and it is cold then the lion is blue. If something visits the lion then it is big. If something is nice then it likes the dog. If the dog eats the tiger then the tiger likes the mouse. If something visits the lion then it eats the tiger.
The dog is round.
("dog" "is" "round" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If something visits the dog then the dog likes the lion.
((("something" "visits" "dog" "+")) -> ("dog" "likes" "lion" "+"))
If something likes the mouse then it visits the tiger.
((("something" "likes" "mouse" "+")) -> ("something" "visits" "tiger" "+"))
If something eats the mouse and it likes the mouse then it eats the lion.
((("something" "eats" "mouse" "+") ("something" "likes" "mouse" "+")) -> ("something" "eats" "lion" "+"))
If something likes the lion and it is cold then the lion is blue.
((("something" "likes" "lion" "+") ("something" "is" "cold" "+")) -> ("lion" "is" "blue" "+"))
If something visits the lion then it is big.
((("something" "visits" "lion" "+")) -> ("something" "is" "big" "+"))
If something is nice then it likes the dog.
((("something" "is" "nice" "+")) -> ("something" "likes" "dog" "+"))
If the dog eats the tiger then the tiger likes the mouse.
((("dog" "eats" "tiger" "+")) -> ("tiger" "likes" "mouse" "+"))
If something visits the lion then it eats the tiger.
((("something" "visits" "lion" "+")) -> ("something" "eats" "tiger" "+"))
The dog is round.
True
1
proof
[(triple1)]
("dog" "is" "round" "+")
triple1
The dog does not visit the mouse.
False
1
inv-proof
[(triple2)]
("dog" "visits" "mouse" "-")
triple2
The tiger is big.
True
2
proof
[(((triple7) -> rule5))]
("tiger" "is" "big" "+")
((triple7) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The dog does not like the lion.
False
2
inv-proof
[(((triple6) -> rule1))]
("dog" "likes" "lion" "-")
((triple6) -> (rule1 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The tiger does not visit the tiger.
Unknown
inv-rconc
[@3: The tiger visits the tiger.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule8 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The lion is blue.
Unknown
rconc
[@1: The lion is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "blue" "+")
The tiger does not like the lion.
Unknown
inv-random
[@0: The tiger likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "lion" "-")
The dog eats the mouse.
Unknown
random
[@0: The dog eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "mouse" "+")
@0: The dog is round.[(triple1)] The dog visits the mouse.[(triple2)] The lion visits the tiger.[(triple3)] The mouse eats the tiger.[(triple4)] The mouse likes the dog.[(triple5)] The mouse visits the dog.[(triple6)] The tiger visits the lion.[(triple7)] @1: The dog likes the lion.[(((triple6) -> rule1))] The tiger eats the tiger.[(((triple7) -> rule8))] The tiger is big.[(((triple7) -> rule5))]
The dog is round.
("dog" "is" "round" "+")
triple1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple2
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple4
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple5
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple6
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple7
The dog likes the lion.
("dog" "likes" "lion" "+")
((triple6) -> (rule1 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple7) -> (rule8 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((triple7) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1