The bear chases the mouse. The bear likes the cat. The bear visits the cat. The cat is nice. The cat is round. The cat visits the cow. The cow chases the cat. The cow likes the cat. The cow visits the mouse. The mouse is nice. The mouse is young. The mouse visits the cow. If something visits the cow then it chases the bear. If something likes the mouse and it visits the cat then the mouse is cold.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is round.
("cat" "is" "round" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If something visits the cow then it chases the bear.
((("something" "visits" "cow" "+")) -> ("something" "chases" "bear" "+"))
If something likes the mouse and it visits the cat then the mouse is cold.
((("something" "likes" "mouse" "+") ("something" "visits" "cat" "+")) -> ("mouse" "is" "cold" "+"))
The mouse visits the cow.
True
1
proof
[(triple12)]
("mouse" "visits" "cow" "+")
triple12
The bear does not like the cat.
False
1
inv-proof
[(triple2)]
("bear" "likes" "cat" "-")
triple2
The mouse chases the bear.
True
2
proof
[(((triple12) -> rule1))]
("mouse" "chases" "bear" "+")
((triple12) -> (rule1 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse does not chase the bear.
False
2
inv-proof
[(((triple12) -> rule1))]
("mouse" "chases" "bear" "-")
((triple12) -> (rule1 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The bear does not chase the bear.
Unknown
inv-rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "chases" "bear" "-")
The mouse is cold.
Unknown
rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "cold" "+")
The cat does not like the mouse.
Unknown
inv-random
[@0: The cat likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "mouse" "-")
The mouse chases the cow.
Unknown
random
[@0: The mouse chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cow" "+")
@0: The bear chases the mouse.[(triple1)] The bear likes the cat.[(triple2)] The bear visits the cat.[(triple3)] The cat is nice.[(triple4)] The cat is round.[(triple5)] The cat visits the cow.[(triple6)] The cow chases the cat.[(triple7)] The cow likes the cat.[(triple8)] The cow visits the mouse.[(triple9)] The mouse is nice.[(triple10)] The mouse is young.[(triple11)] The mouse visits the cow.[(triple12)] @1: The cat chases the bear.[(((triple6) -> rule1))] The mouse chases the bear.[(((triple12) -> rule1))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear likes the cat.
("bear" "likes" "cat" "+")
triple2
The bear visits the cat.
("bear" "visits" "cat" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple4
The cat is round.
("cat" "is" "round" "+")
triple5
The cat visits the cow.
("cat" "visits" "cow" "+")
triple6
The cow chases the cat.
("cow" "chases" "cat" "+")
triple7
The cow likes the cat.
("cow" "likes" "cat" "+")
triple8
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple9
The mouse is nice.
("mouse" "is" "nice" "+")
triple10
The mouse is young.
("mouse" "is" "young" "+")
triple11
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple12
The cat chases the bear.
("cat" "chases" "bear" "+")
((triple6) -> (rule1 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
((triple12) -> (rule1 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1