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