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