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