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