The bear is rough. The bear likes the mouse. The bear sees the mouse. The lion does not visit the mouse. The mouse likes the lion. The squirrel is green. The squirrel sees the lion. If someone visits the lion and they are young then they do not visit the mouse. If the bear likes the lion and the bear does not visit the squirrel then the bear does not see the mouse. If someone is round then they like the lion. If someone likes the lion then they are not rough. If someone is round then they are nice. Green people are round.
The bear is rough.
("bear" "is" "rough" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If someone visits the lion and they are young then they do not visit the mouse.
((("someone" "visits" "lion" "+") ("someone" "is" "young" "+")) -> ("someone" "visits" "mouse" "-"))
If the bear likes the lion and the bear does not visit the squirrel then the bear does not see the mouse.
((("bear" "likes" "lion" "+") ("bear" "visits" "squirrel" "~")) -> ("bear" "sees" "mouse" "-"))
If someone is round then they like the lion.
((("someone" "is" "round" "+")) -> ("someone" "likes" "lion" "+"))
If someone likes the lion then they are not rough.
((("someone" "likes" "lion" "+")) -> ("someone" "is" "rough" "-"))
If someone is round then they are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
Green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
The squirrel sees the lion.
True
1
proof
[(triple7)]
("squirrel" "sees" "lion" "+")
triple7
The squirrel does not see the lion.
False
1
inv-proof
[(triple7)]
("squirrel" "sees" "lion" "-")
triple7
The mouse is not rough.
True
2
proof
[(((triple5) -> rule4))]
("mouse" "is" "rough" "-")
((triple5) -> (rule4 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
The squirrel is not round.
False
2
inv-proof
[(((triple6) -> rule6))]
("squirrel" "is" "round" "-")
((triple6) -> (rule6 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel likes the lion.
True
3
proof
[(((((triple6) -> rule6)) -> rule3))]
("squirrel" "likes" "lion" "+")
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel does not like the lion.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule3))]
("squirrel" "likes" "lion" "-")
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel is not rough.
True
4
proof
[(((((((triple6) -> rule6)) -> rule3)) -> rule4))]
("squirrel" "is" "rough" "-")
((((((triple6) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel is not rough.
("squirrel" "is" "rough" "-")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The squirrel is rough.
False
4
inv-proof
[(((((((triple6) -> rule6)) -> rule3)) -> rule4))]
("squirrel" "is" "rough" "+")
((((((triple6) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel is not rough.
("squirrel" "is" "rough" "-")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The mouse is not nice.
Unknown
inv-rconc
[@2: The mouse is nice.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("mouse" "is" "nice" "-")
The bear is nice.
Unknown
rconc
[@2: The bear is nice.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("bear" "is" "nice" "+")
The bear is not round.
Unknown
inv-rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "round" "-")
The lion likes the lion.
Unknown
rconc
[@2: The lion likes the lion.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("lion" "likes" "lion" "+")
The lion does not visit the bear.
Unknown
inv-random
[@0: The lion visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "bear" "-")
The mouse likes the bear.
Unknown
random
[@0: The mouse likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "bear" "+")
The squirrel does not like the mouse.
Unknown
inv-random
[@0: The squirrel likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "mouse" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The bear is rough.[(triple1)] The bear likes the mouse.[(triple2)] The bear sees the mouse.[(triple3)] The lion does not visit the mouse.[(triple4)] The mouse likes the lion.[(triple5)] The squirrel is green.[(triple6)] The squirrel sees the lion.[(triple7)] @1: The mouse is not rough.[(((triple5) -> rule4))] The squirrel is round.[(((triple6) -> rule6))] @2: The squirrel is nice.[(((((triple6) -> rule6)) -> rule5))] The squirrel likes the lion.[(((((triple6) -> rule6)) -> rule3))] @3: The squirrel is not rough.[(((((((triple6) -> rule6)) -> rule3)) -> rule4))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple3
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
triple4
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple5
The squirrel is green.
("squirrel" "is" "green" "+")
triple6
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple7
The mouse is not rough.
("mouse" "is" "rough" "-")
((triple5) -> (rule4 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
((triple6) -> (rule6 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((((triple6) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel is not rough.
("squirrel" "is" "rough" "-")
((((((triple6) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel is not rough.
("squirrel" "is" "rough" "-")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3