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