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