The cat chases the lion. The cat needs the rabbit. The cow chases the cat. The cow is young. The cow needs the rabbit. The lion chases the rabbit. The lion sees the rabbit. The rabbit chases the cat. The rabbit is kind. The rabbit is nice. The rabbit is round. The rabbit needs the cat. The rabbit needs the lion. The rabbit sees the lion. If someone sees the cat then they need the cow. If the lion is green and the lion needs the cat then the lion is kind. If someone is kind then they see the cat. If someone needs the cat and they are kind then the cat needs the cow. If someone sees the lion and they see the cow then the cow needs the rabbit. If the rabbit needs the cow then the cow is kind. If the rabbit sees the cat then the cat needs the lion.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone sees the cat then they need the cow.
((("someone" "sees" "cat" "+")) -> ("someone" "needs" "cow" "+"))
If the lion is green and the lion needs the cat then the lion is kind.
((("lion" "is" "green" "+") ("lion" "needs" "cat" "+")) -> ("lion" "is" "kind" "+"))
If someone is kind then they see the cat.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "cat" "+"))
If someone needs the cat and they are kind then the cat needs the cow.
((("someone" "needs" "cat" "+") ("someone" "is" "kind" "+")) -> ("cat" "needs" "cow" "+"))
If someone sees the lion and they see the cow then the cow needs the rabbit.
((("someone" "sees" "lion" "+") ("someone" "sees" "cow" "+")) -> ("cow" "needs" "rabbit" "+"))
If the rabbit needs the cow then the cow is kind.
((("rabbit" "needs" "cow" "+")) -> ("cow" "is" "kind" "+"))
If the rabbit sees the cat then the cat needs the lion.
((("rabbit" "sees" "cat" "+")) -> ("cat" "needs" "lion" "+"))
The cow chases the cat.
True
1
proof
[(triple3)]
("cow" "chases" "cat" "+")
triple3
The rabbit is not nice.
False
1
inv-proof
[(triple10)]
("rabbit" "is" "nice" "-")
triple10
The cat needs the cow.
True
3
proof
[(((triple12 triple9) -> rule4))]
("cat" "needs" "cow" "+")
((triple12 triple9) -> (rule4 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat does not need the cow.
False
3
inv-proof
[(((triple12 triple9) -> rule4))]
("cat" "needs" "cow" "-")
((triple12 triple9) -> (rule4 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The rabbit needs the cow.
True
3
proof
[(((((triple9) -> rule3)) -> rule1))]
("rabbit" "needs" "cow" "+")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit does not need the cow.
False
3
inv-proof
[(((((triple9) -> rule3)) -> rule1))]
("rabbit" "needs" "cow" "-")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The cow is kind.
True
4
proof
[(((((((triple9) -> rule3)) -> rule1)) -> rule6))]
("cow" "is" "kind" "+")
((((((triple9) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3
The cow is not kind.
False
4
inv-proof
[(((((((triple9) -> rule3)) -> rule1)) -> rule6))]
("cow" "is" "kind" "-")
((((((triple9) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3
The cow sees the cat.
True
5
proof
[(((((((((triple9) -> rule3)) -> rule1)) -> rule6)) -> rule3))]
("cow" "sees" "cat" "+")
((((((((triple9) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int3
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int4
The cow does not see the cat.
False
5
inv-proof
[(((((((((triple9) -> rule3)) -> rule1)) -> rule6)) -> rule3))]
("cow" "sees" "cat" "-")
((((((((triple9) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int3
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int4
The cow needs the cow.
True
6
proof
[(((((((((((triple9) -> rule3)) -> rule1)) -> rule6)) -> rule3)) -> rule1))]
("cow" "needs" "cow" "+")
((((((((((triple9) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int5
The cow does not need the cow.
False
6
inv-proof
[(((((((((((triple9) -> rule3)) -> rule1)) -> rule6)) -> rule3)) -> rule1))]
("cow" "needs" "cow" "-")
((((((((((triple9) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int5
The lion does not see the cat.
Unknown
inv-rconc
[@2: The lion sees the cat.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("lion" "sees" "cat" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "sees" "cat" "+")
The lion is not kind.
Unknown
inv-rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "kind" "-")
The lion needs the cow.
Unknown
rconc
[@3: The lion needs the cow.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("lion" "needs" "cow" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The cow does not chase the rabbit.
Unknown
inv-random
[@0: The cow chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "rabbit" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
The lion does not chase the cat.
Unknown
inv-random
[@0: The lion chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cat" "-")
The cow sees the lion.
Unknown
random
[@0: The cow sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "lion" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
@0: The cat chases the lion.[(triple1)] The cat needs the rabbit.[(triple2)] The cow chases the cat.[(triple3)] The cow is young.[(triple4)] The cow needs the rabbit.[(triple5)] The lion chases the rabbit.[(triple6)] The lion sees the rabbit.[(triple7)] The rabbit chases the cat.[(triple8)] The rabbit is kind.[(triple9)] The rabbit is nice.[(triple10)] The rabbit is round.[(triple11)] The rabbit needs the cat.[(triple12)] The rabbit needs the lion.[(triple13)] The rabbit sees the lion.[(triple14)] @1: The cat needs the cow.[(((triple12 triple9) -> rule4))] The rabbit sees the cat.[(((triple9) -> rule3))] @2: The cat needs the lion.[(((((triple9) -> rule3)) -> rule7))] The rabbit needs the cow.[(((((triple9) -> rule3)) -> rule1))] @3: The cow is kind.[(((((((triple9) -> rule3)) -> rule1)) -> rule6))] @4: The cow sees the cat.[(((((((((triple9) -> rule3)) -> rule1)) -> rule6)) -> rule3))] @5: The cow needs the cow.[(((((((((((triple9) -> rule3)) -> rule1)) -> rule6)) -> rule3)) -> rule1))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple2
The cow chases the cat.
("cow" "chases" "cat" "+")
triple3
The cow is young.
("cow" "is" "young" "+")
triple4
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple5
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple6
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple7
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple8
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple9
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple10
The rabbit is round.
("rabbit" "is" "round" "+")
triple11
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple12
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple13
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple14
The cat needs the cow.
("cat" "needs" "cow" "+")
((triple12 triple9) -> (rule4 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((triple9) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
((((triple9) -> (rule3 % int2))) -> (rule7 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
((((((triple9) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3
The cow sees the cat.
("cow" "sees" "cat" "+")
((((((((triple9) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int3
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int4
The cow needs the cow.
("cow" "needs" "cow" "+")
((((((((((triple9) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int5