The cat chases the lion. The cat chases the rabbit. The cat eats the rabbit. The lion is rough. The lion visits the rabbit. The rabbit visits the cat. The rabbit visits the lion. If someone is rough then they chase the cat. If someone is blue then they chase the rabbit. If the lion chases the rabbit and the rabbit is big then the lion visits the cat. If someone is green then they chase the lion. If someone visits the rabbit and they visit the cat then the rabbit is big. If someone chases the cat then the cat is rough. If someone eats the lion and the lion is big then they are blue. If the rabbit eats the cat and the cat visits the lion then the lion is blue.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If someone is rough then they chase the cat.
((("someone" "is" "rough" "+")) -> ("someone" "chases" "cat" "+"))
If someone is blue then they chase the rabbit.
((("someone" "is" "blue" "+")) -> ("someone" "chases" "rabbit" "+"))
If the lion chases the rabbit and the rabbit is big then the lion visits the cat.
((("lion" "chases" "rabbit" "+") ("rabbit" "is" "big" "+")) -> ("lion" "visits" "cat" "+"))
If someone is green then they chase the lion.
((("someone" "is" "green" "+")) -> ("someone" "chases" "lion" "+"))
If someone visits the rabbit and they visit the cat then the rabbit is big.
((("someone" "visits" "rabbit" "+") ("someone" "visits" "cat" "+")) -> ("rabbit" "is" "big" "+"))
If someone chases the cat then the cat is rough.
((("someone" "chases" "cat" "+")) -> ("cat" "is" "rough" "+"))
If someone eats the lion and the lion is big then they are blue.
((("someone" "eats" "lion" "+") ("lion" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If the rabbit eats the cat and the cat visits the lion then the lion is blue.
((("rabbit" "eats" "cat" "+") ("cat" "visits" "lion" "+")) -> ("lion" "is" "blue" "+"))
The cat eats the rabbit.
True
1
proof
[(triple3)]
("cat" "eats" "rabbit" "+")
triple3
The cat does not chase the rabbit.
False
1
inv-proof
[(triple2)]
("cat" "chases" "rabbit" "-")
triple2
The lion chases the cat.
True
2
proof
[(((triple4) -> rule1))]
("lion" "chases" "cat" "+")
((triple4) -> (rule1 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion does not chase the cat.
False
2
inv-proof
[(((triple4) -> rule1))]
("lion" "chases" "cat" "-")
((triple4) -> (rule1 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The cat is rough.
True
3
proof
[(((((triple4) -> rule1)) -> rule6))]
("cat" "is" "rough" "+")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The cat is not rough.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule6))]
("cat" "is" "rough" "-")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The cat chases the cat.
True
4
proof
[(((((((triple4) -> rule1)) -> rule6)) -> rule1))]
("cat" "chases" "cat" "+")
((((((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
int3
The cat does not chase the cat.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule6)) -> rule1))]
("cat" "chases" "cat" "-")
((((((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
int3
The lion is not blue.
Unknown
inv-rconc
[@1: The lion is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "is" "blue" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@2: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The rabbit is not blue.
Unknown
inv-rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit is big.
Unknown
rconc
[@2: The rabbit is big.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("rabbit" "is" "big" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The rabbit eats the lion.
Unknown
random
[@0: The rabbit eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "lion" "+")
The lion does not eat the rabbit.
Unknown
inv-random
[@0: The lion eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "rabbit" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The cat chases the lion.[(triple1)] The cat chases the rabbit.[(triple2)] The cat eats the rabbit.[(triple3)] The lion is rough.[(triple4)] The lion visits the rabbit.[(triple5)] The rabbit visits the cat.[(triple6)] The rabbit visits the lion.[(triple7)] @1: The lion chases the cat.[(((triple4) -> rule1))] @2: The cat is rough.[(((((triple4) -> rule1)) -> rule6))] @3: The cat chases the cat.[(((((((triple4) -> rule1)) -> rule6)) -> rule1))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple2
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple5
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple6
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple7
The lion chases the cat.
("lion" "chases" "cat" "+")
((triple4) -> (rule1 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
((((((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
int3