The dog chases the mouse. The dog is big. The dog is round. The dog likes the mouse. The dog sees the mouse. The mouse chases the dog. The mouse is green. The mouse is nice. The mouse likes the dog. The mouse sees the dog. If something is nice then it chases the mouse. If something is red and it likes the mouse then it chases the mouse. If the dog is nice and the dog likes the mouse then the dog is green. If the mouse chases the dog then the mouse sees the dog. If something is big then it sees the mouse. If something chases the mouse and the mouse sees the dog then the mouse chases the dog.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is round.
("dog" "is" "round" "+")
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 green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If something is nice then it chases the mouse.
((("something" "is" "nice" "+")) -> ("something" "chases" "mouse" "+"))
If something is red and it likes the mouse then it chases the mouse.
((("something" "is" "red" "+") ("something" "likes" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
If the dog is nice and the dog likes the mouse then the dog is green.
((("dog" "is" "nice" "+") ("dog" "likes" "mouse" "+")) -> ("dog" "is" "green" "+"))
If the mouse chases the dog then the mouse sees the dog.
((("mouse" "chases" "dog" "+")) -> ("mouse" "sees" "dog" "+"))
If something is big then it sees the mouse.
((("something" "is" "big" "+")) -> ("something" "sees" "mouse" "+"))
If something chases the mouse and the mouse sees the dog then the mouse chases the dog.
((("something" "chases" "mouse" "+") ("mouse" "sees" "dog" "+")) -> ("mouse" "chases" "dog" "+"))
The dog is big.
True
1
proof
[(triple2)]
("dog" "is" "big" "+")
triple2
The dog does not chase the mouse.
False
1
inv-proof
[(triple1)]
("dog" "chases" "mouse" "-")
triple1
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The dog chases the mouse.[(triple1)] The dog is big.[(triple2)] The dog is round.[(triple3)] The dog likes the mouse.[(triple4)] The dog sees the mouse.[(triple5 OR ((triple2) -> rule5))] The mouse chases the dog.[(triple6 OR ((triple1 triple10) -> rule6) OR ((((triple8) -> rule1) triple10) -> rule6))] The mouse is green.[(triple7)] The mouse is nice.[(triple8)] The mouse likes the dog.[(triple9)] The mouse sees the dog.[(triple10 OR ((triple6) -> rule4))] @1: The mouse chases the mouse.[(((triple8) -> rule1))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is round.
("dog" "is" "round" "+")
triple3
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple4
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple5
((triple2) -> (rule5 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple6
((triple1 triple10) -> (rule6 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
((((triple8) -> (rule1 % int2)) triple10) -> (rule6 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple9
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple10
((triple6) -> (rule4 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple8) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1