The bear is big. The bear is green. The bear likes the cat. The bear likes the mouse. The bear sees the mouse. The bear visits the cat. The bear visits the mouse. The cat likes the bear. The cat sees the bear. The mouse is cold. The mouse is nice. The mouse is round. The mouse likes the cat. The mouse sees the bear. The mouse sees the cat. The mouse visits the bear. If the mouse visits the cat then the cat likes the mouse. If something is round then it sees the cat. If something is nice then it visits the cat.
The bear is big.
("bear" "is" "big" "+")
The bear is green.
("bear" "is" "green" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If the mouse visits the cat then the cat likes the mouse.
((("mouse" "visits" "cat" "+")) -> ("cat" "likes" "mouse" "+"))
If something is round then it sees the cat.
((("something" "is" "round" "+")) -> ("something" "sees" "cat" "+"))
If something is nice then it visits the cat.
((("something" "is" "nice" "+")) -> ("something" "visits" "cat" "+"))
The mouse sees the bear.
True
1
proof
[(triple14)]
("mouse" "sees" "bear" "+")
triple14
The mouse does not see the cat.
False
1
inv-proof
[(triple15 OR ((triple12) -> rule2))]
("mouse" "sees" "cat" "-")
triple15
((triple12) -> (rule2 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The mouse visits the cat.
True
2
proof
[(((triple11) -> rule3))]
("mouse" "visits" "cat" "+")
((triple11) -> (rule3 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The mouse does not visit the cat.
False
2
inv-proof
[(((triple11) -> rule3))]
("mouse" "visits" "cat" "-")
((triple11) -> (rule3 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The cat likes the mouse.
True
3
proof
[(((((triple11) -> rule3)) -> rule1))]
("cat" "likes" "mouse" "+")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The cat does not like the mouse.
False
3
inv-proof
[(((((triple11) -> rule3)) -> rule1))]
("cat" "likes" "mouse" "-")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The bear does not see the cat.
Unknown
inv-rconc
[@1: The bear sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "cat" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "cat" "+")
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "visits" "cat" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The bear is big.[(triple1)] The bear is green.[(triple2)] The bear likes the cat.[(triple3)] The bear likes the mouse.[(triple4)] The bear sees the mouse.[(triple5)] The bear visits the cat.[(triple6)] The bear visits the mouse.[(triple7)] The cat likes the bear.[(triple8)] The cat sees the bear.[(triple9)] The mouse is cold.[(triple10)] The mouse is nice.[(triple11)] The mouse is round.[(triple12)] The mouse likes the cat.[(triple13)] The mouse sees the bear.[(triple14)] The mouse sees the cat.[(triple15 OR ((triple12) -> rule2))] The mouse visits the bear.[(triple16)] @1: The mouse visits the cat.[(((triple11) -> rule3))] @2: The cat likes the mouse.[(((((triple11) -> rule3)) -> rule1))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is green.
("bear" "is" "green" "+")
triple2
The bear likes the cat.
("bear" "likes" "cat" "+")
triple3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple4
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple5
The bear visits the cat.
("bear" "visits" "cat" "+")
triple6
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple7
The cat likes the bear.
("cat" "likes" "bear" "+")
triple8
The cat sees the bear.
("cat" "sees" "bear" "+")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
The mouse is nice.
("mouse" "is" "nice" "+")
triple11
The mouse is round.
("mouse" "is" "round" "+")
triple12
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple13
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple14
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple15
((triple12) -> (rule2 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple16
The mouse visits the cat.
("mouse" "visits" "cat" "+")
((triple11) -> (rule3 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2