The cow does not see the rabbit. The mouse chases the rabbit. The mouse chases the squirrel. The mouse likes the cow. The mouse likes the squirrel. The mouse does not see the cow. The rabbit chases the mouse. The rabbit is nice. The squirrel is not cold. The squirrel likes the cow. The squirrel likes the rabbit. If someone is young then they see the rabbit. If someone is nice then they see the squirrel. If someone likes the rabbit then they are young. If someone sees the squirrel then they like the mouse. If someone chases the cow and they see the cow then the cow is nice. If someone likes the mouse then they like the rabbit. If someone sees the cow then they like the cow.
The cow does not see the rabbit.
("cow" "sees" "rabbit" "-")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The squirrel is not cold.
("squirrel" "is" "cold" "-")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
If someone is young then they see the rabbit.
((("someone" "is" "young" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone is nice then they see the squirrel.
((("someone" "is" "nice" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone likes the rabbit then they are young.
((("someone" "likes" "rabbit" "+")) -> ("someone" "is" "young" "+"))
If someone sees the squirrel then they like the mouse.
((("someone" "sees" "squirrel" "+")) -> ("someone" "likes" "mouse" "+"))
If someone chases the cow and they see the cow then the cow is nice.
((("someone" "chases" "cow" "+") ("someone" "sees" "cow" "+")) -> ("cow" "is" "nice" "+"))
If someone likes the mouse then they like the rabbit.
((("someone" "likes" "mouse" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone sees the cow then they like the cow.
((("someone" "sees" "cow" "+")) -> ("someone" "likes" "cow" "+"))
The squirrel likes the cow.
True
1
proof
[(triple10)]
("squirrel" "likes" "cow" "+")
triple10
The squirrel does not like the rabbit.
False
1
inv-proof
[(triple11)]
("squirrel" "likes" "rabbit" "-")
triple11
The squirrel is young.
True
2
proof
[(((triple11) -> rule3))]
("squirrel" "is" "young" "+")
((triple11) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The rabbit does not see the squirrel.
False
2
inv-proof
[(((triple8) -> rule2))]
("rabbit" "sees" "squirrel" "-")
((triple8) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit likes the mouse.
True
3
proof
[(((((triple8) -> rule2)) -> rule4))]
("rabbit" "likes" "mouse" "+")
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The rabbit does not like the mouse.
False
3
inv-proof
[(((((triple8) -> rule2)) -> rule4))]
("rabbit" "likes" "mouse" "-")
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The rabbit likes the rabbit.
True
4
proof
[(((((((triple8) -> rule2)) -> rule4)) -> rule6))]
("rabbit" "likes" "rabbit" "+")
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The rabbit does not like the rabbit.
False
4
inv-proof
[(((((((triple8) -> rule2)) -> rule4)) -> rule6))]
("rabbit" "likes" "rabbit" "-")
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The rabbit is young.
True
5
proof
[(((((((((triple8) -> rule2)) -> rule4)) -> rule6)) -> rule3))]
("rabbit" "is" "young" "+")
((((((((triple8) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int3
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int4
The rabbit is not young.
False
5
inv-proof
[(((((((((triple8) -> rule2)) -> rule4)) -> rule6)) -> rule3))]
("rabbit" "is" "young" "-")
((((((((triple8) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int3
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int4
The rabbit sees the rabbit.
True
6
proof
[(((((((((((triple8) -> rule2)) -> rule4)) -> rule6)) -> rule3)) -> rule1))]
("rabbit" "sees" "rabbit" "+")
((((((((((triple8) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int3
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int4
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int5
The rabbit does not see the rabbit.
False
6
inv-proof
[(((((((((((triple8) -> rule2)) -> rule4)) -> rule6)) -> rule3)) -> rule1))]
("rabbit" "sees" "rabbit" "-")
((((((((((triple8) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int3
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int4
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int5
The cow is not young.
Unknown
inv-rconc
[@5: The cow is young.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule4 <- rule2 <- rule5 <- FAIL)]]
("cow" "is" "young" "-")
The rabbit likes the cow.
Unknown
rconc
[@1: The rabbit likes the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "likes" "cow" "+")
The squirrel does not like the mouse.
Unknown
inv-rconc
[@2: The squirrel likes the mouse.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("squirrel" "likes" "mouse" "-")
The mouse sees the squirrel.
Unknown
rconc
[@1: The mouse sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "squirrel" "+")
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "likes" "cow" "-")
The mouse is young.
Unknown
rconc
[@4: The mouse is young.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule4 <- rule2 <- FAIL)]]
("mouse" "is" "young" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The rabbit sees the cow.
Unknown
random
[@0: The rabbit sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "cow" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The cow does not see the rabbit.[(triple1)] The mouse chases the rabbit.[(triple2)] The mouse chases the squirrel.[(triple3)] The mouse does not see the cow.[(triple6)] The mouse likes the cow.[(triple4)] The mouse likes the squirrel.[(triple5)] The rabbit chases the mouse.[(triple7)] The rabbit is nice.[(triple8)] The squirrel is not cold.[(triple9)] The squirrel likes the cow.[(triple10)] The squirrel likes the rabbit.[(triple11)] @1: The rabbit sees the squirrel.[(((triple8) -> rule2))] The squirrel is young.[(((triple11) -> rule3))] @2: The rabbit likes the mouse.[(((((triple8) -> rule2)) -> rule4))] The squirrel sees the rabbit.[(((((triple11) -> rule3)) -> rule1))] @3: The rabbit likes the rabbit.[(((((((triple8) -> rule2)) -> rule4)) -> rule6))] @4: The rabbit is young.[(((((((((triple8) -> rule2)) -> rule4)) -> rule6)) -> rule3))] @5: The rabbit sees the rabbit.[(((((((((((triple8) -> rule2)) -> rule4)) -> rule6)) -> rule3)) -> rule1))]
The cow does not see the rabbit.
("cow" "sees" "rabbit" "-")
triple1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple2
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple3
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
triple6
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple4
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple5
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple7
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple8
The squirrel is not cold.
("squirrel" "is" "cold" "-")
triple9
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple10
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple11
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
((triple8) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
((triple11) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The rabbit is young.
("rabbit" "is" "young" "+")
((((((((triple8) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int3
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int4
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((((((((triple8) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int3
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int4
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int5