The cow eats the mouse. The cow eats the rabbit. The cow is blue. The cow likes the mouse. The cow likes the rabbit. The cow sees the mouse. The mouse eats the cow. The mouse eats the rabbit. The mouse is blue. The mouse is kind. The mouse likes the cow. The mouse likes the rabbit. The mouse sees the cow. The mouse does not see the rabbit. The rabbit eats the mouse. The rabbit likes the mouse. Red people are not kind. If someone sees the cow then the cow eats the rabbit. If the cow does not see the rabbit then the rabbit is blue. If someone eats the rabbit then they like the cow. If someone likes the mouse and they like the cow then they are red. If the mouse is rough and the mouse is not big then the mouse is kind.
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse does not see the rabbit.
("mouse" "sees" "rabbit" "-")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
Red people are not kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "-"))
If someone sees the cow then the cow eats the rabbit.
((("someone" "sees" "cow" "+")) -> ("cow" "eats" "rabbit" "+"))
If the cow does not see the rabbit then the rabbit is blue.
((("cow" "sees" "rabbit" "~")) -> ("rabbit" "is" "blue" "+"))
If someone eats the rabbit then they like the cow.
((("someone" "eats" "rabbit" "+")) -> ("someone" "likes" "cow" "+"))
If someone likes the mouse and they like the cow then they are red.
((("someone" "likes" "mouse" "+") ("someone" "likes" "cow" "+")) -> ("someone" "is" "red" "+"))
If the mouse is rough and the mouse is not big then the mouse is kind.
((("mouse" "is" "rough" "+") ("mouse" "is" "big" "~")) -> ("mouse" "is" "kind" "+"))
The mouse likes the cow.
True
1
proof
[(triple11 OR ((triple8) -> rule4))]
("mouse" "likes" "cow" "+")
triple11
((triple8) -> (rule4 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The rabbit does not like the mouse.
False
1
inv-proof
[(triple16)]
("rabbit" "likes" "mouse" "-")
triple16
The cow likes the cow.
True
2
proof
[(((triple2) -> rule4) OR ((((triple13) -> rule2)) -> rule4))]
("cow" "likes" "cow" "+")
((triple2) -> (rule4 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule4 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The cow does not like the cow.
False
2
inv-proof
[(((triple2) -> rule4) OR ((((triple13) -> rule2)) -> rule4))]
("cow" "likes" "cow" "-")
((triple2) -> (rule4 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule4 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The cow is red.
True
4
proof
[(((triple4 ((triple2) -> rule4)) -> rule5) OR ((triple4 ((((triple13) -> rule2)) -> rule4)) -> rule5))]
("cow" "is" "red" "+")
((triple4 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
((triple4 ((((triple13) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int3
The cow is not red.
False
4
inv-proof
[(((triple4 ((triple2) -> rule4)) -> rule5) OR ((triple4 ((((triple13) -> rule2)) -> rule4)) -> rule5))]
("cow" "is" "red" "-")
((triple4 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
((triple4 ((((triple13) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int3
The cow is not kind.
True
5
proof
[(((((triple4 ((triple2) -> rule4)) -> rule5)) -> rule1) OR ((((triple4 ((((triple13) -> rule2)) -> rule4)) -> rule5)) -> rule1))]
("cow" "is" "kind" "-")
((((triple4 ((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cow is not kind.
("cow" "is" "kind" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
((((triple4 ((((triple13) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cow is not kind.
("cow" "is" "kind" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int4
The cow is kind.
False
5
inv-proof
[(((((triple4 ((triple2) -> rule4)) -> rule5)) -> rule1) OR ((((triple4 ((((triple13) -> rule2)) -> rule4)) -> rule5)) -> rule1))]
("cow" "is" "kind" "+")
((((triple4 ((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cow is not kind.
("cow" "is" "kind" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
((((triple4 ((((triple13) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cow is not kind.
("cow" "is" "kind" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int4
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "red" "-")
The rabbit is red.
Unknown
rconc
[@2: The rabbit is red.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("rabbit" "is" "red" "+")
The rabbit is not blue.
Unknown
inv-rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit likes the cow.
Unknown
rconc
[@1: The rabbit likes the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "likes" "cow" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit sees the cow.
Unknown
random
[@0: The rabbit sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "cow" "+")
@0: The cow eats the mouse.[(triple1)] The cow eats the rabbit.[(triple2 OR ((triple13) -> rule2))] The cow is blue.[(triple3)] The cow likes the mouse.[(triple4)] The cow likes the rabbit.[(triple5)] The cow sees the mouse.[(triple6)] The mouse does not see the rabbit.[(triple14)] The mouse eats the cow.[(triple7)] The mouse eats the rabbit.[(triple8)] The mouse is blue.[(triple9)] The mouse is kind.[(triple10)] The mouse likes the cow.[(triple11 OR ((triple8) -> rule4))] The mouse likes the rabbit.[(triple12)] The mouse sees the cow.[(triple13)] The rabbit eats the mouse.[(triple15)] The rabbit likes the mouse.[(triple16)] @1: The cow likes the cow.[(((triple2) -> rule4) OR ((((triple13) -> rule2)) -> rule4))] @2: The cow is red.[(((triple4 ((triple2) -> rule4)) -> rule5) OR ((triple4 ((((triple13) -> rule2)) -> rule4)) -> rule5))] @3: The cow is not kind.[(((((triple4 ((triple2) -> rule4)) -> rule5)) -> rule1) OR ((((triple4 ((((triple13) -> rule2)) -> rule4)) -> rule5)) -> rule1))]
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple2
((triple13) -> (rule2 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
triple3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple4
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple5
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple6
The mouse does not see the rabbit.
("mouse" "sees" "rabbit" "-")
triple14
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple7
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple8
The mouse is blue.
("mouse" "is" "blue" "+")
triple9
The mouse is kind.
("mouse" "is" "kind" "+")
triple10
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple11
((triple8) -> (rule4 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple12
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple13
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple15
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple16
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple2) -> (rule4 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule4 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The cow is red.
("cow" "is" "red" "+")
((triple4 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
((triple4 ((((triple13) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int3
The cow is not kind.
("cow" "is" "kind" "-")
((((triple4 ((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cow is not kind.
("cow" "is" "kind" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
((((triple4 ((((triple13) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cow is not kind.
("cow" "is" "kind" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int4