The bear eats the lion. The bear is green. The bear is rough. The bear visits the lion. The cat chases the rabbit. The cat eats the bear. The cat eats the rabbit. The cat is kind. The cat visits the bear. The lion chases the bear. The lion does not eat the bear. The lion is not green. The rabbit chases the cat. The rabbit eats the bear. The rabbit visits the cat. If the lion is young then the lion visits the bear. If someone is green and not rough then they eat the lion. If someone visits the rabbit then they visit the lion. If someone eats the bear then they are green. If someone chases the bear then they do not eat the cat. If someone is green then they chase the bear. If the lion visits the rabbit and the rabbit is not young then the lion is not kind. If the bear chases the rabbit and the lion does not visit the bear then the bear does not visit the lion.
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion does not eat the bear.
("lion" "eats" "bear" "-")
The lion is not green.
("lion" "is" "green" "-")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If the lion is young then the lion visits the bear.
((("lion" "is" "young" "+")) -> ("lion" "visits" "bear" "+"))
If someone is green and not rough then they eat the lion.
((("someone" "is" "green" "+") ("someone" "is" "rough" "~")) -> ("someone" "eats" "lion" "+"))
If someone visits the rabbit then they visit the lion.
((("someone" "visits" "rabbit" "+")) -> ("someone" "visits" "lion" "+"))
If someone eats the bear then they are green.
((("someone" "eats" "bear" "+")) -> ("someone" "is" "green" "+"))
If someone chases the bear then they do not eat the cat.
((("someone" "chases" "bear" "+")) -> ("someone" "eats" "cat" "-"))
If someone is green then they chase the bear.
((("someone" "is" "green" "+")) -> ("someone" "chases" "bear" "+"))
If the lion visits the rabbit and the rabbit is not young then the lion is not kind.
((("lion" "visits" "rabbit" "+") ("rabbit" "is" "young" "~")) -> ("lion" "is" "kind" "-"))
If the bear chases the rabbit and the lion does not visit the bear then the bear does not visit the lion.
((("bear" "chases" "rabbit" "+") ("lion" "visits" "bear" "~")) -> ("bear" "visits" "lion" "-"))
The bear is green.
True
1
proof
[(triple2)]
("bear" "is" "green" "+")
triple2
The lion does not chase the bear.
False
1
inv-proof
[(triple10)]
("lion" "chases" "bear" "-")
triple10
The rabbit is green.
True
2
proof
[(((triple14) -> rule4))]
("rabbit" "is" "green" "+")
((triple14) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The lion eats the cat.
False
2
inv-proof
[(((triple10) -> rule5))]
("lion" "eats" "cat" "+")
((triple10) -> (rule5 % int1))
The lion does not eat the cat.
("lion" "eats" "cat" "-")
int1
The cat chases the bear.
True
3
proof
[(((((triple6) -> rule4)) -> rule6))]
("cat" "chases" "bear" "+")
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat does not chase the bear.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule6))]
("cat" "chases" "bear" "-")
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat does not eat the cat.
True
4
proof
[(((((((triple6) -> rule4)) -> rule6)) -> rule5))]
("cat" "eats" "cat" "-")
((((((triple6) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cat does not eat the cat.
("cat" "eats" "cat" "-")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
The rabbit eats the cat.
False
4
inv-proof
[(((((((triple14) -> rule4)) -> rule6)) -> rule5))]
("rabbit" "eats" "cat" "+")
((((((triple14) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit does not visit the lion.
Unknown
inv-rconc
[@1: The rabbit visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "visits" "lion" "-")
The cat eats the lion.
Unknown
rconc
[@1: The cat eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "eats" "lion" "+")
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "eats" "lion" "-")
The lion visits the bear.
Unknown
rconc
[@1: The lion visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "bear" "+")
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The rabbit chases the lion.
Unknown
random
[@0: The rabbit chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "lion" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The lion visits the cat.
Unknown
random
[@0: The lion visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cat" "+")
@0: The bear eats the lion.[(triple1)] The bear is green.[(triple2)] The bear is rough.[(triple3)] The bear visits the lion.[(triple4)] The cat chases the rabbit.[(triple5)] The cat eats the bear.[(triple6)] The cat eats the rabbit.[(triple7)] The cat is kind.[(triple8)] The cat visits the bear.[(triple9)] The lion chases the bear.[(triple10)] The lion does not eat the bear.[(triple11)] The lion is not green.[(triple12)] The rabbit chases the cat.[(triple13)] The rabbit eats the bear.[(triple14)] The rabbit visits the cat.[(triple15)] @1: The bear chases the bear.[(((triple2) -> rule6))] The cat is green.[(((triple6) -> rule4))] The lion does not eat the cat.[(((triple10) -> rule5))] The rabbit is green.[(((triple14) -> rule4))] @2: The bear does not eat the cat.[(((((triple2) -> rule6)) -> rule5))] The cat chases the bear.[(((((triple6) -> rule4)) -> rule6))] The rabbit chases the bear.[(((((triple14) -> rule4)) -> rule6))] @3: The cat does not eat the cat.[(((((((triple6) -> rule4)) -> rule6)) -> rule5))] The rabbit does not eat the cat.[(((((((triple14) -> rule4)) -> rule6)) -> rule5))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The bear is green.
("bear" "is" "green" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear visits the lion.
("bear" "visits" "lion" "+")
triple4
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple5
The cat eats the bear.
("cat" "eats" "bear" "+")
triple6
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple7
The cat is kind.
("cat" "is" "kind" "+")
triple8
The cat visits the bear.
("cat" "visits" "bear" "+")
triple9
The lion chases the bear.
("lion" "chases" "bear" "+")
triple10
The lion does not eat the bear.
("lion" "eats" "bear" "-")
triple11
The lion is not green.
("lion" "is" "green" "-")
triple12
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple13
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple14
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple15
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple2) -> (rule6 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The cat is green.
("cat" "is" "green" "+")
((triple6) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The lion does not eat the cat.
("lion" "eats" "cat" "-")
((triple10) -> (rule5 % int1))
The lion does not eat the cat.
("lion" "eats" "cat" "-")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple14) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The bear does not eat the cat.
("bear" "eats" "cat" "-")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
The bear does not eat the cat.
("bear" "eats" "cat" "-")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The cat chases the bear.
("cat" "chases" "bear" "+")
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((((triple14) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The cat does not eat the cat.
("cat" "eats" "cat" "-")
((((((triple6) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cat does not eat the cat.
("cat" "eats" "cat" "-")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
((((((triple14) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3