The dog is blue. The dog is kind. The dog is nice. The dog is young. The dog needs the mouse. The dog sees the mouse. The mouse is blue. The mouse is nice. The mouse is young. The mouse needs the dog. The mouse sees the dog. The mouse visits the dog. If someone sees the dog and the dog visits the mouse then the mouse visits the dog. If someone is young and they visit the mouse then the mouse sees the dog. If someone needs the dog and the dog is nice then the dog needs the mouse. If someone is nice then they are blue. If someone sees the mouse and they are kind then the mouse visits the dog. If someone needs the mouse and they see the dog then they visit the dog. If someone visits the dog then the dog is kind. If someone sees the dog and the dog visits the mouse then the dog sees the mouse.
The dog is blue.
("dog" "is" "blue" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If someone sees the dog and the dog visits the mouse then the mouse visits the dog.
((("someone" "sees" "dog" "+") ("dog" "visits" "mouse" "+")) -> ("mouse" "visits" "dog" "+"))
If someone is young and they visit the mouse then the mouse sees the dog.
((("someone" "is" "young" "+") ("someone" "visits" "mouse" "+")) -> ("mouse" "sees" "dog" "+"))
If someone needs the dog and the dog is nice then the dog needs the mouse.
((("someone" "needs" "dog" "+") ("dog" "is" "nice" "+")) -> ("dog" "needs" "mouse" "+"))
If someone is nice then they are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone sees the mouse and they are kind then the mouse visits the dog.
((("someone" "sees" "mouse" "+") ("someone" "is" "kind" "+")) -> ("mouse" "visits" "dog" "+"))
If someone needs the mouse and they see the dog then they visit the dog.
((("someone" "needs" "mouse" "+") ("someone" "sees" "dog" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the dog then the dog is kind.
((("someone" "visits" "dog" "+")) -> ("dog" "is" "kind" "+"))
If someone sees the dog and the dog visits the mouse then the dog sees the mouse.
((("someone" "sees" "dog" "+") ("dog" "visits" "mouse" "+")) -> ("dog" "sees" "mouse" "+"))
The dog is blue.
True
1
proof
[(triple1 OR ((triple3) -> rule4))]
("dog" "is" "blue" "+")
triple1
((triple3) -> (rule4 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not blue.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule4))]
("dog" "is" "blue" "-")
triple1
((triple3) -> (rule4 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog does not visit the dog.
Unknown
inv-rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "visits" "dog" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The dog is blue.[(triple1 OR ((triple3) -> rule4))] The dog is kind.[(triple2 OR ((triple12) -> rule7))] The dog is nice.[(triple3)] The dog is young.[(triple4)] The dog needs the mouse.[(triple5 OR ((triple10 triple3) -> rule3))] The dog sees the mouse.[(triple6)] The mouse is blue.[(triple7 OR ((triple8) -> rule4))] The mouse is nice.[(triple8)] The mouse is young.[(triple9)] The mouse needs the dog.[(triple10)] The mouse sees the dog.[(triple11)] The mouse visits the dog.[(triple12 OR ((triple6 triple2) -> rule5))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
((triple3) -> (rule4 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
triple2
((triple12) -> (rule7 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
triple4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple5
((triple10 triple3) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple6
The mouse is blue.
("mouse" "is" "blue" "+")
triple7
((triple8) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse is young.
("mouse" "is" "young" "+")
triple9
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple10
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple11
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple12
((triple6 triple2) -> (rule5 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1