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