The bear visits the cow. The cat likes the mouse. The cow is blue. The mouse is green. If something chases the bear then it likes the mouse. If something visits the cow then it is kind. If something likes the cat then it likes the bear. All green things are cold. If something chases the cow then it is cold. If something chases the bear then it is kind. If the cat chases the mouse and the cat likes the bear then the bear visits the cow. If something likes the bear and the bear likes the cat then the bear visits the cow.
The bear visits the cow.
("bear" "visits" "cow" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cow is blue.
("cow" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
If something chases the bear then it likes the mouse.
((("something" "chases" "bear" "+")) -> ("something" "likes" "mouse" "+"))
If something visits the cow then it is kind.
((("something" "visits" "cow" "+")) -> ("something" "is" "kind" "+"))
If something likes the cat then it likes the bear.
((("something" "likes" "cat" "+")) -> ("something" "likes" "bear" "+"))
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something chases the cow then it is cold.
((("something" "chases" "cow" "+")) -> ("something" "is" "cold" "+"))
If something chases the bear then it is kind.
((("something" "chases" "bear" "+")) -> ("something" "is" "kind" "+"))
If the cat chases the mouse and the cat likes the bear then the bear visits the cow.
((("cat" "chases" "mouse" "+") ("cat" "likes" "bear" "+")) -> ("bear" "visits" "cow" "+"))
If something likes the bear and the bear likes the cat then the bear visits the cow.
((("something" "likes" "bear" "+") ("bear" "likes" "cat" "+")) -> ("bear" "visits" "cow" "+"))
The cat likes the mouse.
True
1
proof
[(triple2)]
("cat" "likes" "mouse" "+")
triple2
The bear does not visit the cow.
False
1
inv-proof
[(triple1)]
("bear" "visits" "cow" "-")
triple1
The mouse is cold.
True
2
proof
[(((triple4) -> rule4))]
("mouse" "is" "cold" "+")
((triple4) -> (rule4 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The bear is not kind.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "is" "kind" "-")
((triple1) -> (rule2 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The cow is not cold.
Unknown
inv-rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "cold" "-")
The bear is cold.
Unknown
rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "cold" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The mouse likes the cow.
Unknown
random
[@0: The mouse likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "cow" "+")
@0: The bear visits the cow.[(triple1)] The cat likes the mouse.[(triple2)] The cow is blue.[(triple3)] The mouse is green.[(triple4)] @1: The bear is kind.[(((triple1) -> rule2))] The mouse is cold.[(((triple4) -> rule4))]
The bear visits the cow.
("bear" "visits" "cow" "+")
triple1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple2
The cow is blue.
("cow" "is" "blue" "+")
triple3
The mouse is green.
("mouse" "is" "green" "+")
triple4
The bear is kind.
("bear" "is" "kind" "+")
((triple1) -> (rule2 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((triple4) -> (rule4 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1