The cow chases the lion. The cow is kind. The cow likes the lion. The cow sees the lion. The lion likes the cow. The lion does not like the rabbit. The lion sees the cow. The rabbit chases the cow. The rabbit chases the lion. The rabbit is kind. The rabbit sees the cow. The rabbit sees the lion. If someone is red then they do not like the cow. If someone is nice and red then they like the lion. If someone likes the lion then they are red. If someone chases the lion and they are rough then the lion likes the cow. If someone is big then they do not see the rabbit. If someone likes the lion and they do not like the cow then they are big.
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The lion does not like the rabbit.
("lion" "likes" "rabbit" "-")
The lion sees the cow.
("lion" "sees" "cow" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone is red then they do not like the cow.
((("someone" "is" "red" "+")) -> ("someone" "likes" "cow" "-"))
If someone is nice and red then they like the lion.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "likes" "lion" "+"))
If someone likes the lion then they are red.
((("someone" "likes" "lion" "+")) -> ("someone" "is" "red" "+"))
If someone chases the lion and they are rough then the lion likes the cow.
((("someone" "chases" "lion" "+") ("someone" "is" "rough" "+")) -> ("lion" "likes" "cow" "+"))
If someone is big then they do not see the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "sees" "rabbit" "-"))
If someone likes the lion and they do not like the cow then they are big.
((("someone" "likes" "lion" "+") ("someone" "likes" "cow" "~")) -> ("someone" "is" "big" "+"))
The rabbit chases the lion.
True
1
proof
[(triple9)]
("rabbit" "chases" "lion" "+")
triple9
The cow does not like the lion.
False
1
inv-proof
[(triple3)]
("cow" "likes" "lion" "-")
triple3
The cow is red.
True
2
proof
[(((triple3) -> rule3))]
("cow" "is" "red" "+")
((triple3) -> (rule3 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is not red.
False
2
inv-proof
[(((triple3) -> rule3))]
("cow" "is" "red" "-")
((triple3) -> (rule3 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow does not like the cow.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("cow" "likes" "cow" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cow does not like the cow.
("cow" "likes" "cow" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow likes the cow.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("cow" "likes" "cow" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cow does not like the cow.
("cow" "likes" "cow" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is big.
True
5
proof
[(((triple3 ((((triple3) -> rule3)) -> rule1)) -> rule6))]
("cow" "is" "big" "+")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow does not like the cow.
("cow" "likes" "cow" "-")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is not big.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule3)) -> rule1)) -> rule6))]
("cow" "is" "big" "-")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow does not like the cow.
("cow" "likes" "cow" "-")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The rabbit does not like the lion.
Unknown
inv-rconc
[@1: The rabbit likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "likes" "lion" "-")
The lion likes the lion.
Unknown
rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "likes" "lion" "+")
The lion is not big.
Unknown
inv-rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "big" "-")
The rabbit is big.
Unknown
rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "big" "+")
The lion does not chase the rabbit.
Unknown
inv-random
[@0: The lion chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "rabbit" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The cow chases the lion.[(triple1)] The cow is kind.[(triple2)] The cow likes the lion.[(triple3)] The cow sees the lion.[(triple4)] The lion does not like the rabbit.[(triple6)] The lion likes the cow.[(triple5)] The lion sees the cow.[(triple7)] The rabbit chases the cow.[(triple8)] The rabbit chases the lion.[(triple9)] The rabbit is kind.[(triple10)] The rabbit sees the cow.[(triple11)] The rabbit sees the lion.[(triple12)] @1: The cow is red.[(((triple3) -> rule3))] @2: The cow does not like the cow.[(((((triple3) -> rule3)) -> rule1))] @3: The cow is big.[(((triple3 ((((triple3) -> rule3)) -> rule1)) -> rule6))] @4: The cow does not see the rabbit.[(((((triple3 ((((triple3) -> rule3)) -> rule1)) -> rule6)) -> rule5))]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
The cow likes the lion.
("cow" "likes" "lion" "+")
triple3
The cow sees the lion.
("cow" "sees" "lion" "+")
triple4
The lion does not like the rabbit.
("lion" "likes" "rabbit" "-")
triple6
The lion likes the cow.
("lion" "likes" "cow" "+")
triple5
The lion sees the cow.
("lion" "sees" "cow" "+")
triple7
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple8
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple9
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple11
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple12
The cow is red.
("cow" "is" "red" "+")
((triple3) -> (rule3 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow does not like the cow.
("cow" "likes" "cow" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cow does not like the cow.
("cow" "likes" "cow" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is big.
("cow" "is" "big" "+")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow does not like the cow.
("cow" "likes" "cow" "-")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow does not see the rabbit.
("cow" "sees" "rabbit" "-")
((((triple3 ((((triple3) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow does not see the rabbit.
("cow" "sees" "rabbit" "-")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow does not like the cow.
("cow" "likes" "cow" "-")
int3
The cow is red.
("cow" "is" "red" "+")
int4