The dog is cold. The mouse does not see the dog. The tiger sees the mouse. If something sees the dog then the dog eats the mouse. If something eats the mouse then it does not visit the mouse. If something sees the mouse then the mouse eats the tiger. If something is young and blue then it eats the tiger. If something visits the tiger then the tiger is red. If something is red and it eats the tiger then it eats the mouse. If something eats the tiger then it is round. If something visits the mouse and it does not eat the mouse then it is round.
The dog is cold.
("dog" "is" "cold" "+")
The mouse does not see the dog.
("mouse" "sees" "dog" "-")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something sees the dog then the dog eats the mouse.
((("something" "sees" "dog" "+")) -> ("dog" "eats" "mouse" "+"))
If something eats the mouse then it does not visit the mouse.
((("something" "eats" "mouse" "+")) -> ("something" "visits" "mouse" "-"))
If something sees the mouse then the mouse eats the tiger.
((("something" "sees" "mouse" "+")) -> ("mouse" "eats" "tiger" "+"))
If something is young and blue then it eats the tiger.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "eats" "tiger" "+"))
If something visits the tiger then the tiger is red.
((("something" "visits" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If something is red and it eats the tiger then it eats the mouse.
((("something" "is" "red" "+") ("something" "eats" "tiger" "+")) -> ("something" "eats" "mouse" "+"))
If something eats the tiger then it is round.
((("something" "eats" "tiger" "+")) -> ("something" "is" "round" "+"))
If something visits the mouse and it does not eat the mouse then it is round.
((("something" "visits" "mouse" "+") ("something" "eats" "mouse" "~")) -> ("something" "is" "round" "+"))
The dog is cold.
True
1
proof
[(triple1)]
("dog" "is" "cold" "+")
triple1
The tiger does not see the mouse.
False
1
inv-proof
[(triple3)]
("tiger" "sees" "mouse" "-")
triple3
The tiger does not eat the mouse.
Unknown
inv-rconc
[@2: The tiger eats the mouse.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("tiger" "eats" "mouse" "-")
The dog visits the mouse.
Unknown
random
[@0: The dog visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "mouse" "+")
@0: The dog is cold.[(triple1)] The mouse does not see the dog.[(triple2)] The tiger sees the mouse.[(triple3)] @1: The mouse eats the tiger.[(((triple3) -> rule3))] @2: The mouse is round.[(((((triple3) -> rule3)) -> rule7))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The mouse does not see the dog.
("mouse" "sees" "dog" "-")
triple2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
((triple3) -> (rule3 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2