The dog is blue. The dog is green. The dog is round. The dog is young. The dog likes the mouse. The dog sees the mouse. The mouse chases the dog. The mouse is not blue. The mouse is cold. The mouse is not round. The mouse likes the dog. The mouse sees the dog. If something chases the dog and it sees the dog then the dog chases the mouse.
The dog is blue.
("dog" "is" "blue" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is round.
("dog" "is" "round" "+")
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 chases the dog.
("mouse" "chases" "dog" "+")
The mouse is not blue.
("mouse" "is" "blue" "-")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is not round.
("mouse" "is" "round" "-")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If something chases the dog and it sees the dog then the dog chases the mouse.
((("something" "chases" "dog" "+") ("something" "sees" "dog" "+")) -> ("dog" "chases" "mouse" "+"))
The dog sees the mouse.
True
1
proof
[(triple6)]
("dog" "sees" "mouse" "+")
triple6
The dog is not green.
False
1
inv-proof
[(triple2)]
("dog" "is" "green" "-")
triple2
The dog chases the mouse.
True
3
proof
[(((triple7 triple12) -> rule1))]
("dog" "chases" "mouse" "+")
((triple7 triple12) -> (rule1 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The dog does not chase the mouse.
False
3
inv-proof
[(((triple7 triple12) -> rule1))]
("dog" "chases" "mouse" "-")
((triple7 triple12) -> (rule1 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
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 blue.[(triple1)] The dog is green.[(triple2)] The dog is round.[(triple3)] The dog is young.[(triple4)] The dog likes the mouse.[(triple5)] The dog sees the mouse.[(triple6)] The mouse chases the dog.[(triple7)] The mouse is cold.[(triple9)] The mouse is not blue.[(triple8)] The mouse is not round.[(triple10)] The mouse likes the dog.[(triple11)] The mouse sees the dog.[(triple12)] @1: The dog chases the mouse.[(((triple7 triple12) -> rule1))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is round.
("dog" "is" "round" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
triple4
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple5
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple6
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
triple9
The mouse is not blue.
("mouse" "is" "blue" "-")
triple8
The mouse is not round.
("mouse" "is" "round" "-")
triple10
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple11
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple12
The dog chases the mouse.
("dog" "chases" "mouse" "+")
((triple7 triple12) -> (rule1 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1