The cat chases the lion. The cat is cold. The cat likes the lion. The cat likes the rabbit. The cat sees the lion. The lion chases the cat. The lion sees the cat. The lion sees the rabbit. The rabbit chases the cat. The rabbit chases the lion. The rabbit is cold. The rabbit sees the cat. If the cat sees the lion and the lion sees the rabbit then the lion is kind. If something chases the lion and it likes the cat then the lion chases the rabbit. If something sees the rabbit and the rabbit is big then it is red. If the rabbit sees the lion then the rabbit chases the lion. If something likes the lion and the lion is red then it is round. If something is red then it chases the cat. If something sees the cat then it is big. If something is red and it chases the rabbit then the rabbit chases the lion.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If the cat sees the lion and the lion sees the rabbit then the lion is kind.
((("cat" "sees" "lion" "+") ("lion" "sees" "rabbit" "+")) -> ("lion" "is" "kind" "+"))
If something chases the lion and it likes the cat then the lion chases the rabbit.
((("something" "chases" "lion" "+") ("something" "likes" "cat" "+")) -> ("lion" "chases" "rabbit" "+"))
If something sees the rabbit and the rabbit is big then it is red.
((("something" "sees" "rabbit" "+") ("rabbit" "is" "big" "+")) -> ("something" "is" "red" "+"))
If the rabbit sees the lion then the rabbit chases the lion.
((("rabbit" "sees" "lion" "+")) -> ("rabbit" "chases" "lion" "+"))
If something likes the lion and the lion is red then it is round.
((("something" "likes" "lion" "+") ("lion" "is" "red" "+")) -> ("something" "is" "round" "+"))
If something is red then it chases the cat.
((("something" "is" "red" "+")) -> ("something" "chases" "cat" "+"))
If something sees the cat then it is big.
((("something" "sees" "cat" "+")) -> ("something" "is" "big" "+"))
If something is red and it chases the rabbit then the rabbit chases the lion.
((("something" "is" "red" "+") ("something" "chases" "rabbit" "+")) -> ("rabbit" "chases" "lion" "+"))
The cat likes the rabbit.
True
1
proof
[(triple4)]
("cat" "likes" "rabbit" "+")
triple4
The lion does not see the rabbit.
False
1
inv-proof
[(triple8)]
("lion" "sees" "rabbit" "-")
triple8
The lion is kind.
True
3
proof
[(((triple5 triple8) -> rule1))]
("lion" "is" "kind" "+")
((triple5 triple8) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is not big.
False
2
inv-proof
[(((triple7) -> rule7))]
("lion" "is" "big" "-")
((triple7) -> (rule7 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is red.
True
4
proof
[(((triple8 ((triple12) -> rule7)) -> rule3))]
("lion" "is" "red" "+")
((triple8 ((triple12) -> (rule7 % int2))) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The lion is not red.
False
4
inv-proof
[(((triple8 ((triple12) -> rule7)) -> rule3))]
("lion" "is" "red" "-")
((triple8 ((triple12) -> (rule7 % int2))) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The cat is round.
True
6
proof
[(((triple3 ((triple8 ((triple12) -> rule7)) -> rule3)) -> rule5))]
("cat" "is" "round" "+")
((triple3 ((triple8 ((triple12) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The cat is not round.
False
6
inv-proof
[(((triple3 ((triple8 ((triple12) -> rule7)) -> rule3)) -> rule5))]
("cat" "is" "round" "-")
((triple3 ((triple8 ((triple12) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "red" "-")
The cat chases the cat.
Unknown
rconc
[@2: The cat chases the cat.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("cat" "chases" "cat" "+")
The lion is not round.
Unknown
inv-rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "round" "-")
The lion chases the rabbit.
Unknown
rconc
[@1: The lion chases the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "chases" "rabbit" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The lion likes the cat.
Unknown
random
[@0: The lion likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cat" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The cat chases the rabbit.
Unknown
random
[@0: The cat chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "rabbit" "+")
@0: The cat chases the lion.[(triple1)] The cat is cold.[(triple2)] The cat likes the lion.[(triple3)] The cat likes the rabbit.[(triple4)] The cat sees the lion.[(triple5)] The lion chases the cat.[(triple6 OR ((((triple8 ((triple12) -> rule7)) -> rule3)) -> rule6))] The lion sees the cat.[(triple7)] The lion sees the rabbit.[(triple8)] The rabbit chases the cat.[(triple9)] The rabbit chases the lion.[(triple10)] The rabbit is cold.[(triple11)] The rabbit sees the cat.[(triple12)] @1: The lion is big.[(((triple7) -> rule7))] The lion is kind.[(((triple5 triple8) -> rule1))] The rabbit is big.[(((triple12) -> rule7))] @2: The lion is red.[(((triple8 ((triple12) -> rule7)) -> rule3))] @3: The cat is round.[(((triple3 ((triple8 ((triple12) -> rule7)) -> rule3)) -> rule5))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat likes the lion.
("cat" "likes" "lion" "+")
triple3
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple4
The cat sees the lion.
("cat" "sees" "lion" "+")
triple5
The lion chases the cat.
("lion" "chases" "cat" "+")
triple6
((((triple8 ((triple12) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The lion sees the cat.
("lion" "sees" "cat" "+")
triple7
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple8
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple9
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple10
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple11
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple12
The lion is big.
("lion" "is" "big" "+")
((triple7) -> (rule7 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((triple5 triple8) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((triple12) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((triple8 ((triple12) -> (rule7 % int2))) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The cat is round.
("cat" "is" "round" "+")
((triple3 ((triple8 ((triple12) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3