The bear is nice. The bear does not visit the mouse. The lion visits the squirrel. The mouse likes the squirrel. The mouse needs the bear. The mouse does not visit the squirrel. The squirrel is red. If something is nice then it visits the bear. If the lion is green then the lion likes the squirrel. If the mouse visits the bear and the bear visits the lion then the bear is not big. If something is big and it visits the mouse then the mouse visits the squirrel. If something likes the mouse then it is round. If something visits the bear then the bear needs the mouse.
The bear is nice.
("bear" "is" "nice" "+")
The bear does not visit the mouse.
("bear" "visits" "mouse" "-")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse does not visit the squirrel.
("mouse" "visits" "squirrel" "-")
The squirrel is red.
("squirrel" "is" "red" "+")
If something is nice then it visits the bear.
((("something" "is" "nice" "+")) -> ("something" "visits" "bear" "+"))
If the lion is green then the lion likes the squirrel.
((("lion" "is" "green" "+")) -> ("lion" "likes" "squirrel" "+"))
If the mouse visits the bear and the bear visits the lion then the bear is not big.
((("mouse" "visits" "bear" "+") ("bear" "visits" "lion" "+")) -> ("bear" "is" "big" "-"))
If something is big and it visits the mouse then the mouse visits the squirrel.
((("something" "is" "big" "+") ("something" "visits" "mouse" "+")) -> ("mouse" "visits" "squirrel" "+"))
If something likes the mouse then it is round.
((("something" "likes" "mouse" "+")) -> ("something" "is" "round" "+"))
If something visits the bear then the bear needs the mouse.
((("something" "visits" "bear" "+")) -> ("bear" "needs" "mouse" "+"))
The squirrel is red.
True
1
proof
[(triple7)]
("squirrel" "is" "red" "+")
triple7
The mouse visits the squirrel.
False
1
inv-proof
[(triple6)]
("mouse" "visits" "squirrel" "+")
triple6
The bear visits the bear.
True
2
proof
[(((triple1) -> rule1))]
("bear" "visits" "bear" "+")
((triple1) -> (rule1 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear does not visit the bear.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "visits" "bear" "-")
((triple1) -> (rule1 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear needs the mouse.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("bear" "needs" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear does not need the mouse.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("bear" "needs" "mouse" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The mouse does not visit the bear.
Unknown
inv-rconc
[@1: The mouse visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "bear" "-")
The lion visits the bear.
Unknown
rconc
[@1: The lion visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "bear" "+")
The lion does not like the squirrel.
Unknown
inv-rconc
[@1: The lion likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "likes" "squirrel" "-")
The squirrel needs the lion.
Unknown
random
[@0: The squirrel needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "lion" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The bear likes the squirrel.
Unknown
random
[@0: The bear likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "squirrel" "+")
@0: The bear does not visit the mouse.[(triple2)] The bear is nice.[(triple1)] The lion visits the squirrel.[(triple3)] The mouse does not visit the squirrel.[(triple6)] The mouse likes the squirrel.[(triple4)] The mouse needs the bear.[(triple5)] The squirrel is red.[(triple7)] @1: The bear visits the bear.[(((triple1) -> rule1))] @2: The bear needs the mouse.[(((((triple1) -> rule1)) -> rule6))]
The bear does not visit the mouse.
("bear" "visits" "mouse" "-")
triple2
The bear is nice.
("bear" "is" "nice" "+")
triple1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple3
The mouse does not visit the squirrel.
("mouse" "visits" "squirrel" "-")
triple6
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple4
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple5
The squirrel is red.
("squirrel" "is" "red" "+")
triple7
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple1) -> (rule1 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2