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