The bear is green. The dog chases the mouse. The lion needs the dog. The mouse chases the bear. If someone visits the bear and the bear is nice then they chase the dog. If the mouse chases the lion and the mouse needs the dog then the mouse needs the lion. If someone visits the dog then the dog is young. If someone is nice then they need the lion. If someone chases the bear then the bear needs the mouse. If someone needs the bear then they visit the lion.
The bear is green.
("bear" "is" "green" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
If someone visits the bear and the bear is nice then they chase the dog.
((("someone" "visits" "bear" "+") ("bear" "is" "nice" "+")) -> ("someone" "chases" "dog" "+"))
If the mouse chases the lion and the mouse needs the dog then the mouse needs the lion.
((("mouse" "chases" "lion" "+") ("mouse" "needs" "dog" "+")) -> ("mouse" "needs" "lion" "+"))
If someone visits the dog then the dog is young.
((("someone" "visits" "dog" "+")) -> ("dog" "is" "young" "+"))
If someone is nice then they need the lion.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "lion" "+"))
If someone chases the bear then the bear needs the mouse.
((("someone" "chases" "bear" "+")) -> ("bear" "needs" "mouse" "+"))
If someone needs the bear then they visit the lion.
((("someone" "needs" "bear" "+")) -> ("someone" "visits" "lion" "+"))
The mouse chases the bear.
True
1
proof
[(triple4)]
("mouse" "chases" "bear" "+")
triple4
The lion does not need the dog.
False
1
inv-proof
[(triple3)]
("lion" "needs" "dog" "-")
triple3
The bear needs the mouse.
True
2
proof
[(((triple4) -> rule5))]
("bear" "needs" "mouse" "+")
((triple4) -> (rule5 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear does not need the mouse.
False
2
inv-proof
[(((triple4) -> rule5))]
("bear" "needs" "mouse" "-")
((triple4) -> (rule5 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "visits" "lion" "-")
The dog chases the dog.
Unknown
rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "dog" "+")
The dog does not chase the lion.
Unknown
inv-random
[@0: The dog chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "lion" "-")
The mouse visits the bear.
Unknown
random
[@0: The mouse visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bear" "+")
@0: The bear is green.[(triple1)] The dog chases the mouse.[(triple2)] The lion needs the dog.[(triple3)] The mouse chases the bear.[(triple4)] @1: The bear needs the mouse.[(((triple4) -> rule5))]
The bear is green.
("bear" "is" "green" "+")
triple1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple2
The lion needs the dog.
("lion" "needs" "dog" "+")
triple3
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple4
The bear needs the mouse.
("bear" "needs" "mouse" "+")
((triple4) -> (rule5 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1