The cow is kind. The cow is rough. The cow is round. The cow likes the lion. The cow needs the lion. The lion is kind. The lion likes the cow. The lion likes the rabbit. The lion needs the cow. The rabbit is green. The rabbit is rough. The rabbit likes the cow. The rabbit likes the lion. The rabbit needs the lion. The rabbit sees the lion. If the rabbit is blue and the rabbit likes the lion then the rabbit sees the lion. If something needs the cow and it is kind then the cow likes the rabbit. If something sees the lion and it likes the rabbit then it needs the cow. If something likes the cow and the cow sees the rabbit then the cow is green. If the rabbit likes the cow and the rabbit sees the lion then the cow sees the rabbit. If something needs the cow and the cow sees the lion then the lion sees the rabbit. If something is blue and rough then it sees the rabbit. If something sees the cow and the cow sees the rabbit then it needs the cow.
The cow is kind.
("cow" "is" "kind" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is round.
("cow" "is" "round" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If the rabbit is blue and the rabbit likes the lion then the rabbit sees the lion.
((("rabbit" "is" "blue" "+") ("rabbit" "likes" "lion" "+")) -> ("rabbit" "sees" "lion" "+"))
If something needs the cow and it is kind then the cow likes the rabbit.
((("something" "needs" "cow" "+") ("something" "is" "kind" "+")) -> ("cow" "likes" "rabbit" "+"))
If something sees the lion and it likes the rabbit then it needs the cow.
((("something" "sees" "lion" "+") ("something" "likes" "rabbit" "+")) -> ("something" "needs" "cow" "+"))
If something likes the cow and the cow sees the rabbit then the cow is green.
((("something" "likes" "cow" "+") ("cow" "sees" "rabbit" "+")) -> ("cow" "is" "green" "+"))
If the rabbit likes the cow and the rabbit sees the lion then the cow sees the rabbit.
((("rabbit" "likes" "cow" "+") ("rabbit" "sees" "lion" "+")) -> ("cow" "sees" "rabbit" "+"))
If something needs the cow and the cow sees the lion then the lion sees the rabbit.
((("something" "needs" "cow" "+") ("cow" "sees" "lion" "+")) -> ("lion" "sees" "rabbit" "+"))
If something is blue and rough then it sees the rabbit.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "sees" "rabbit" "+"))
If something sees the cow and the cow sees the rabbit then it needs the cow.
((("something" "sees" "cow" "+") ("cow" "sees" "rabbit" "+")) -> ("something" "needs" "cow" "+"))
The cow is kind.
True
1
proof
[(triple1)]
("cow" "is" "kind" "+")
triple1
The cow is not round.
False
1
inv-proof
[(triple3)]
("cow" "is" "round" "-")
triple3
The cow likes the rabbit.
True
3
proof
[(((triple9 triple6) -> rule2))]
("cow" "likes" "rabbit" "+")
((triple9 triple6) -> (rule2 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The cow does not see the rabbit.
False
3
inv-proof
[(((triple12 triple15) -> rule5))]
("cow" "sees" "rabbit" "-")
((triple12 triple15) -> (rule5 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow is green.
True
5
proof
[(((triple12 ((triple12 triple15) -> rule5)) -> rule4) OR ((triple7 ((triple12 triple15) -> rule5)) -> rule4))]
("cow" "is" "green" "+")
((triple12 ((triple12 triple15) -> (rule5 % int2))) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
((triple7 ((triple12 triple15) -> (rule5 % int2))) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The cow is not green.
False
5
inv-proof
[(((triple12 ((triple12 triple15) -> rule5)) -> rule4) OR ((triple7 ((triple12 triple15) -> rule5)) -> rule4))]
("cow" "is" "green" "-")
((triple12 ((triple12 triple15) -> (rule5 % int2))) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
((triple7 ((triple12 triple15) -> (rule5 % int2))) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "needs" "cow" "-")
The lion sees the rabbit.
Unknown
rconc
[@1: The lion sees the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "sees" "rabbit" "+")
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
@0: The cow is kind.[(triple1)] The cow is rough.[(triple2)] The cow is round.[(triple3)] The cow likes the lion.[(triple4)] The cow needs the lion.[(triple5)] The lion is kind.[(triple6)] The lion likes the cow.[(triple7)] The lion likes the rabbit.[(triple8)] The lion needs the cow.[(triple9)] The rabbit is green.[(triple10)] The rabbit is rough.[(triple11)] The rabbit likes the cow.[(triple12)] The rabbit likes the lion.[(triple13)] The rabbit needs the lion.[(triple14)] The rabbit sees the lion.[(triple15)] @1: The cow likes the rabbit.[(((triple9 triple6) -> rule2))] The cow sees the rabbit.[(((triple12 triple15) -> rule5))] @2: The cow is green.[(((triple12 ((triple12 triple15) -> rule5)) -> rule4) OR ((triple7 ((triple12 triple15) -> rule5)) -> rule4))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The cow is round.
("cow" "is" "round" "+")
triple3
The cow likes the lion.
("cow" "likes" "lion" "+")
triple4
The cow needs the lion.
("cow" "needs" "lion" "+")
triple5
The lion is kind.
("lion" "is" "kind" "+")
triple6
The lion likes the cow.
("lion" "likes" "cow" "+")
triple7
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple8
The lion needs the cow.
("lion" "needs" "cow" "+")
triple9
The rabbit is green.
("rabbit" "is" "green" "+")
triple10
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple11
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple12
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple13
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple14
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple15
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
((triple9 triple6) -> (rule2 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
((triple12 triple15) -> (rule5 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow is green.
("cow" "is" "green" "+")
((triple12 ((triple12 triple15) -> (rule5 % int2))) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
((triple7 ((triple12 triple15) -> (rule5 % int2))) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2