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