The dog chases the lion. The dog chases the rabbit. The dog eats the lion. The dog eats the rabbit. The dog is big. The dog sees the lion. The lion chases the dog. The lion eats the dog. The lion is cold. The lion sees the dog. The lion sees the rabbit. The rabbit chases the lion. The rabbit is cold. The rabbit is rough. The rabbit sees the dog. If someone eats the rabbit then the rabbit sees the lion. Nice, cold people are rough. If someone sees the lion then the lion eats the rabbit. If someone is nice and big then they chase the rabbit. If someone chases the lion and they chase the dog then the lion sees the dog. If someone sees the lion and the lion eats the dog then they are nice. If someone sees the lion and the lion is big then the lion is nice. If the lion sees the rabbit and the rabbit eats the lion then the rabbit sees the lion.
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is big.
("dog" "is" "big" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If someone eats the rabbit then the rabbit sees the lion.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "sees" "lion" "+"))
Nice, cold people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone sees the lion then the lion eats the rabbit.
((("someone" "sees" "lion" "+")) -> ("lion" "eats" "rabbit" "+"))
If someone is nice and big then they chase the rabbit.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone chases the lion and they chase the dog then the lion sees the dog.
((("someone" "chases" "lion" "+") ("someone" "chases" "dog" "+")) -> ("lion" "sees" "dog" "+"))
If someone sees the lion and the lion eats the dog then they are nice.
((("someone" "sees" "lion" "+") ("lion" "eats" "dog" "+")) -> ("someone" "is" "nice" "+"))
If someone sees the lion and the lion is big then the lion is nice.
((("someone" "sees" "lion" "+") ("lion" "is" "big" "+")) -> ("lion" "is" "nice" "+"))
If the lion sees the rabbit and the rabbit eats the lion then the rabbit sees the lion.
((("lion" "sees" "rabbit" "+") ("rabbit" "eats" "lion" "+")) -> ("rabbit" "sees" "lion" "+"))
The rabbit is cold.
True
1
proof
[(triple13)]
("rabbit" "is" "cold" "+")
triple13
The rabbit is not rough.
False
1
inv-proof
[(triple14 OR ((((((triple4) -> rule1) triple8) -> rule6) triple13) -> rule2) OR ((((((((triple6) -> rule3)) -> rule1) triple8) -> rule6) triple13) -> rule2))]
("rabbit" "is" "rough" "-")
triple14
((((((triple4) -> (rule1 % int3)) triple8) -> (rule6 % int2)) triple13) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
((((((((triple6) -> (rule3 % int4))) -> (rule1 % int3)) triple8) -> (rule6 % int2)) triple13) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int4
The lion eats the rabbit.
True
2
proof
[(((triple6) -> rule3) OR ((((triple4) -> rule1)) -> rule3))]
("lion" "eats" "rabbit" "+")
((triple6) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The lion does not eat the rabbit.
False
2
inv-proof
[(((triple6) -> rule3) OR ((((triple4) -> rule1)) -> rule3))]
("lion" "eats" "rabbit" "-")
((triple6) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The rabbit is nice.
True
4
proof
[(((((triple4) -> rule1) triple8) -> rule6) OR ((((((triple6) -> rule3)) -> rule1) triple8) -> rule6))]
("rabbit" "is" "nice" "+")
((((triple4) -> (rule1 % int2)) triple8) -> (rule6 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2)) triple8) -> (rule6 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int3
The rabbit is not nice.
False
4
inv-proof
[(((((triple4) -> rule1) triple8) -> rule6) OR ((((((triple6) -> rule3)) -> rule1) triple8) -> rule6))]
("rabbit" "is" "nice" "-")
((((triple4) -> (rule1 % int2)) triple8) -> (rule6 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2)) triple8) -> (rule6 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int3
The rabbit does not chase the rabbit.
Unknown
inv-rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "chases" "rabbit" "-")
The dog is rough.
Unknown
rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "rough" "+")
The lion does not chase the rabbit.
Unknown
inv-rconc
[@1: The lion chases the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "chases" "rabbit" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
@0: The dog chases the lion.[(triple1)] The dog chases the rabbit.[(triple2 OR ((((triple6 triple8) -> rule6) triple5) -> rule4))] The dog eats the lion.[(triple3)] The dog eats the rabbit.[(triple4)] The dog is big.[(triple5)] The dog sees the lion.[(triple6)] The lion chases the dog.[(triple7)] The lion eats the dog.[(triple8)] The lion is cold.[(triple9)] The lion sees the dog.[(triple10)] The lion sees the rabbit.[(triple11)] The rabbit chases the lion.[(triple12)] The rabbit is cold.[(triple13)] The rabbit is rough.[(triple14 OR ((((((triple4) -> rule1) triple8) -> rule6) triple13) -> rule2) OR ((((((((triple6) -> rule3)) -> rule1) triple8) -> rule6) triple13) -> rule2))] The rabbit sees the dog.[(triple15)] @1: The dog is nice.[(((triple6 triple8) -> rule6))] The lion eats the rabbit.[(((triple6) -> rule3) OR ((((triple4) -> rule1)) -> rule3))] The rabbit sees the lion.[(((triple4) -> rule1) OR ((((triple6) -> rule3)) -> rule1))] @2: The rabbit is nice.[(((((triple4) -> rule1) triple8) -> rule6) OR ((((((triple6) -> rule3)) -> rule1) triple8) -> rule6))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple2
((((triple6 triple8) -> (rule6 % int2)) triple5) -> (rule4 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog eats the lion.
("dog" "eats" "lion" "+")
triple3
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple4
The dog is big.
("dog" "is" "big" "+")
triple5
The dog sees the lion.
("dog" "sees" "lion" "+")
triple6
The lion chases the dog.
("lion" "chases" "dog" "+")
triple7
The lion eats the dog.
("lion" "eats" "dog" "+")
triple8
The lion is cold.
("lion" "is" "cold" "+")
triple9
The lion sees the dog.
("lion" "sees" "dog" "+")
triple10
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple11
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple12
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple13
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple14
((((((triple4) -> (rule1 % int3)) triple8) -> (rule6 % int2)) triple13) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
((((((((triple6) -> (rule3 % int4))) -> (rule1 % int3)) triple8) -> (rule6 % int2)) triple13) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int4
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple15
The dog is nice.
("dog" "is" "nice" "+")
((triple6 triple8) -> (rule6 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
((triple6) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
((triple4) -> (rule1 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
((((triple4) -> (rule1 % int2)) triple8) -> (rule6 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2)) triple8) -> (rule6 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int3