The dog chases the mouse. The dog is blue. The dog is cold. The dog is green. The dog needs the mouse. The dog visits the mouse. The mouse chases the dog. The mouse is cold. The mouse does not need the dog. The mouse does not visit the dog. If something chases the mouse and it needs the mouse then it is nice. If something is nice and it chases the mouse then it does not chase the dog. If something needs the mouse and it is not green then the mouse visits the dog.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse does not need the dog.
("mouse" "needs" "dog" "-")
The mouse does not visit the dog.
("mouse" "visits" "dog" "-")
If something chases the mouse and it needs the mouse then it is nice.
((("something" "chases" "mouse" "+") ("something" "needs" "mouse" "+")) -> ("something" "is" "nice" "+"))
If something is nice and it chases the mouse then it does not chase the dog.
((("something" "is" "nice" "+") ("something" "chases" "mouse" "+")) -> ("something" "chases" "dog" "-"))
If something needs the mouse and it is not green then the mouse visits the dog.
((("something" "needs" "mouse" "+") ("something" "is" "green" "~")) -> ("mouse" "visits" "dog" "+"))
The mouse does not visit the dog.
True
1
proof
[(triple10)]
("mouse" "visits" "dog" "-")
triple10
The dog does not need the mouse.
False
1
inv-proof
[(triple5)]
("dog" "needs" "mouse" "-")
triple5
The dog is nice.
True
3
proof
[(((triple1 triple5) -> rule1))]
("dog" "is" "nice" "+")
((triple1 triple5) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is not nice.
False
3
inv-proof
[(((triple1 triple5) -> rule1))]
("dog" "is" "nice" "-")
((triple1 triple5) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog does not chase the dog.
True
5
proof
[(((((triple1 triple5) -> rule1) triple1) -> rule2))]
("dog" "chases" "dog" "-")
((((triple1 triple5) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog chases the dog.
False
5
inv-proof
[(((((triple1 triple5) -> rule1) triple1) -> rule2))]
("dog" "chases" "dog" "+")
((((triple1 triple5) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The mouse is not nice.
Unknown
inv-rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "nice" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
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 mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
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 chases the mouse.[(triple1)] The dog is blue.[(triple2)] The dog is cold.[(triple3)] The dog is green.[(triple4)] The dog needs the mouse.[(triple5)] The dog visits the mouse.[(triple6)] The mouse chases the dog.[(triple7)] The mouse does not need the dog.[(triple9)] The mouse does not visit the dog.[(triple10)] The mouse is cold.[(triple8)] @1: The dog is nice.[(((triple1 triple5) -> rule1))] @2: The dog does not chase the dog.[(((((triple1 triple5) -> rule1) triple1) -> rule2))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
triple4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple5
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple6
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple7
The mouse does not need the dog.
("mouse" "needs" "dog" "-")
triple9
The mouse does not visit the dog.
("mouse" "visits" "dog" "-")
triple10
The mouse is cold.
("mouse" "is" "cold" "+")
triple8
The dog is nice.
("dog" "is" "nice" "+")
((triple1 triple5) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog does not chase the dog.
("dog" "chases" "dog" "-")
((((triple1 triple5) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2