The dog is big. The dog is blue. The dog is kind. The dog is red. The mouse chases the dog. The mouse is big. The mouse is blue. The mouse is kind. The mouse is red. The mouse is rough. The mouse likes the dog. The mouse sees the dog. If the dog likes the mouse and the mouse is rough then the dog is rough. If something chases the mouse and the mouse is blue then it is red. If something likes the dog then the dog likes the mouse.
The dog is big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If the dog likes the mouse and the mouse is rough then the dog is rough.
((("dog" "likes" "mouse" "+") ("mouse" "is" "rough" "+")) -> ("dog" "is" "rough" "+"))
If something chases the mouse and the mouse is blue then it is red.
((("something" "chases" "mouse" "+") ("mouse" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something likes the dog then the dog likes the mouse.
((("something" "likes" "dog" "+")) -> ("dog" "likes" "mouse" "+"))
The mouse chases the dog.
True
1
proof
[(triple5)]
("mouse" "chases" "dog" "+")
triple5
The mouse is not kind.
False
1
inv-proof
[(triple8)]
("mouse" "is" "kind" "-")
triple8
The dog likes the mouse.
True
2
proof
[(((triple11) -> rule3))]
("dog" "likes" "mouse" "+")
((triple11) -> (rule3 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog does not like the mouse.
False
2
inv-proof
[(((triple11) -> rule3))]
("dog" "likes" "mouse" "-")
((triple11) -> (rule3 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog is rough.
True
4
proof
[(((((triple11) -> rule3) triple10) -> rule1))]
("dog" "is" "rough" "+")
((((triple11) -> (rule3 % int2)) triple10) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog is not rough.
False
4
inv-proof
[(((((triple11) -> rule3) triple10) -> rule1))]
("dog" "is" "rough" "-")
((((triple11) -> (rule3 % int2)) triple10) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog does not chase the mouse.
Unknown
inv-random
[@0: The dog chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "mouse" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The dog does not see the mouse.
Unknown
inv-random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The dog is big.[(triple1)] The dog is blue.[(triple2)] The dog is kind.[(triple3)] The dog is red.[(triple4)] The mouse chases the dog.[(triple5)] The mouse is big.[(triple6)] The mouse is blue.[(triple7)] The mouse is kind.[(triple8)] The mouse is red.[(triple9)] The mouse is rough.[(triple10)] The mouse likes the dog.[(triple11)] The mouse sees the dog.[(triple12)] @1: The dog likes the mouse.[(((triple11) -> rule3))] @2: The dog is rough.[(((((triple11) -> rule3) triple10) -> rule1))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple5
The mouse is big.
("mouse" "is" "big" "+")
triple6
The mouse is blue.
("mouse" "is" "blue" "+")
triple7
The mouse is kind.
("mouse" "is" "kind" "+")
triple8
The mouse is red.
("mouse" "is" "red" "+")
triple9
The mouse is rough.
("mouse" "is" "rough" "+")
triple10
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple11
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple12
The dog likes the mouse.
("dog" "likes" "mouse" "+")
((triple11) -> (rule3 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
((((triple11) -> (rule3 % int2)) triple10) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2