The bear is not rough. The bear visits the mouse. The cat is blue. The cat is not nice. The cat is red. The mouse does not eat the bear. The mouse eats the cat. The mouse is not rough. The mouse likes the bear. The mouse does not visit the bear. If something likes the bear then the bear visits the cat. If something visits the cat then it visits the bear. If something eats the cat and it is not nice then it is blue. If something visits the mouse then it does not like the cat. If the bear likes the cat and the bear does not visit the cat then the cat visits the bear. If the cat visits the mouse and the mouse does not like the cat then the mouse visits the bear.
The bear is not rough.
("bear" "is" "rough" "-")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is not nice.
("cat" "is" "nice" "-")
The cat is red.
("cat" "is" "red" "+")
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
If something likes the bear then the bear visits the cat.
((("something" "likes" "bear" "+")) -> ("bear" "visits" "cat" "+"))
If something visits the cat then it visits the bear.
((("something" "visits" "cat" "+")) -> ("something" "visits" "bear" "+"))
If something eats the cat and it is not nice then it is blue.
((("something" "eats" "cat" "+") ("something" "is" "nice" "~")) -> ("something" "is" "blue" "+"))
If something visits the mouse then it does not like the cat.
((("something" "visits" "mouse" "+")) -> ("something" "likes" "cat" "-"))
If the bear likes the cat and the bear does not visit the cat then the cat visits the bear.
((("bear" "likes" "cat" "+") ("bear" "visits" "cat" "~")) -> ("cat" "visits" "bear" "+"))
If the cat visits the mouse and the mouse does not like the cat then the mouse visits the bear.
((("cat" "visits" "mouse" "+") ("mouse" "likes" "cat" "~")) -> ("mouse" "visits" "bear" "+"))
The cat is not nice.
True
1
proof
[(triple4)]
("cat" "is" "nice" "-")
triple4
The mouse does not like the bear.
False
1
inv-proof
[(triple9)]
("mouse" "likes" "bear" "-")
triple9
The bear does not like the cat.
True
2
proof
[(((triple2) -> rule4))]
("bear" "likes" "cat" "-")
((triple2) -> (rule4 % int1))
The bear does not like the cat.
("bear" "likes" "cat" "-")
int1
The bear does not visit the cat.
False
2
inv-proof
[(((triple9) -> rule1))]
("bear" "visits" "cat" "-")
((triple9) -> (rule1 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear visits the bear.
True
3
proof
[(((((triple9) -> rule1)) -> rule2))]
("bear" "visits" "bear" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear does not visit the bear.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule2))]
("bear" "visits" "bear" "-")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear is not blue.
Unknown
inv-rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "blue" "-")
The cat visits the bear.
Unknown
rconc
[@1: The cat visits the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "bear" "+")
The mouse is not blue.
Unknown
inv-rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "blue" "-")
The cat visits the mouse.
Unknown
random
[@0: The cat visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "mouse" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
@0: The bear is not rough.[(triple1)] The bear visits the mouse.[(triple2)] The cat is blue.[(triple3)] The cat is not nice.[(triple4)] The cat is red.[(triple5)] The mouse does not eat the bear.[(triple6)] The mouse does not visit the bear.[(triple10)] The mouse eats the cat.[(triple7)] The mouse is not rough.[(triple8)] The mouse likes the bear.[(triple9)] @1: The bear does not like the cat.[(((triple2) -> rule4))] The bear visits the cat.[(((triple9) -> rule1))] @2: The bear visits the bear.[(((((triple9) -> rule1)) -> rule2))]
The bear is not rough.
("bear" "is" "rough" "-")
triple1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is not nice.
("cat" "is" "nice" "-")
triple4
The cat is red.
("cat" "is" "red" "+")
triple5
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
triple6
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
triple10
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple7
The mouse is not rough.
("mouse" "is" "rough" "-")
triple8
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple9
The bear does not like the cat.
("bear" "likes" "cat" "-")
((triple2) -> (rule4 % int1))
The bear does not like the cat.
("bear" "likes" "cat" "-")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
((triple9) -> (rule1 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2