The dog is blue. The dog is cold. The dog is kind. The dog is round. The dog is young. The dog likes the mouse. The dog needs the mouse. The dog visits the mouse. The mouse is blue. The mouse is cold. The mouse is kind. The mouse is round. The mouse is young. The mouse likes the dog. The mouse needs the dog. The mouse visits the dog. If someone is blue then they visit the dog.
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If someone is blue then they visit the dog.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "dog" "+"))
The dog is blue.
True
1
proof
[(triple1)]
("dog" "is" "blue" "+")
triple1
The dog is not kind.
False
1
inv-proof
[(triple3)]
("dog" "is" "kind" "-")
triple3
The dog visits the dog.
True
2
proof
[(((triple1) -> rule1))]
("dog" "visits" "dog" "+")
((triple1) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog does not visit the dog.
False
2
inv-proof
[(((triple1) -> rule1))]
("dog" "visits" "dog" "-")
((triple1) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The dog is blue.[(triple1)] The dog is cold.[(triple2)] The dog is kind.[(triple3)] The dog is round.[(triple4)] The dog is young.[(triple5)] The dog likes the mouse.[(triple6)] The dog needs the mouse.[(triple7)] The dog visits the mouse.[(triple8)] The mouse is blue.[(triple9)] The mouse is cold.[(triple10)] The mouse is kind.[(triple11)] The mouse is round.[(triple12)] The mouse is young.[(triple13)] The mouse likes the dog.[(triple14)] The mouse needs the dog.[(triple15)] The mouse visits the dog.[(triple16 OR ((triple9) -> rule1))] @1: The dog visits the dog.[(((triple1) -> rule1))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog is round.
("dog" "is" "round" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple6
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple7
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple8
The mouse is blue.
("mouse" "is" "blue" "+")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
triple11
The mouse is round.
("mouse" "is" "round" "+")
triple12
The mouse is young.
("mouse" "is" "young" "+")
triple13
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple14
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple15
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple16
((triple9) -> (rule1 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple1) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1