The bear visits the rabbit. The cat chases the bear. The rabbit chases the bear. The tiger is red. If something chases the rabbit and the rabbit is blue then the rabbit visits the cat. If something is big and it visits the bear then it visits the rabbit. If something is big and it visits the cat then it visits the bear. If something chases the bear and the bear sees the cat then the cat is big. If something chases the bear then the bear visits the tiger. If the rabbit sees the cat and the cat is green then the rabbit visits the cat. If something chases the cat then the cat visits the bear. If something chases the cat then it is blue.
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The tiger is red.
("tiger" "is" "red" "+")
If something chases the rabbit and the rabbit is blue then the rabbit visits the cat.
((("something" "chases" "rabbit" "+") ("rabbit" "is" "blue" "+")) -> ("rabbit" "visits" "cat" "+"))
If something is big and it visits the bear then it visits the rabbit.
((("something" "is" "big" "+") ("something" "visits" "bear" "+")) -> ("something" "visits" "rabbit" "+"))
If something is big and it visits the cat then it visits the bear.
((("something" "is" "big" "+") ("something" "visits" "cat" "+")) -> ("something" "visits" "bear" "+"))
If something chases the bear and the bear sees the cat then the cat is big.
((("something" "chases" "bear" "+") ("bear" "sees" "cat" "+")) -> ("cat" "is" "big" "+"))
If something chases the bear then the bear visits the tiger.
((("something" "chases" "bear" "+")) -> ("bear" "visits" "tiger" "+"))
If the rabbit sees the cat and the cat is green then the rabbit visits the cat.
((("rabbit" "sees" "cat" "+") ("cat" "is" "green" "+")) -> ("rabbit" "visits" "cat" "+"))
If something chases the cat then the cat visits the bear.
((("something" "chases" "cat" "+")) -> ("cat" "visits" "bear" "+"))
If something chases the cat then it is blue.
((("something" "chases" "cat" "+")) -> ("something" "is" "blue" "+"))
The cat chases the bear.
True
1
proof
[(triple2)]
("cat" "chases" "bear" "+")
triple2
The rabbit does not chase the bear.
False
1
inv-proof
[(triple3)]
("rabbit" "chases" "bear" "-")
triple3
The bear visits the tiger.
True
2
proof
[(((triple2) -> rule5) OR ((triple3) -> rule5))]
("bear" "visits" "tiger" "+")
((triple2) -> (rule5 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
((triple3) -> (rule5 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The bear does not visit the tiger.
False
2
inv-proof
[(((triple2) -> rule5) OR ((triple3) -> rule5))]
("bear" "visits" "tiger" "-")
((triple2) -> (rule5 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
((triple3) -> (rule5 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "visits" "bear" "-")
The tiger visits the bear.
Unknown
rconc
[@1: The tiger visits the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "bear" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear visits the rabbit.[(triple1)] The cat chases the bear.[(triple2)] The rabbit chases the bear.[(triple3)] The tiger is red.[(triple4)] @1: The bear visits the tiger.[(((triple2) -> rule5) OR ((triple3) -> rule5))]
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple1
The cat chases the bear.
("cat" "chases" "bear" "+")
triple2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple3
The tiger is red.
("tiger" "is" "red" "+")
triple4
The bear visits the tiger.
("bear" "visits" "tiger" "+")
((triple2) -> (rule5 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
((triple3) -> (rule5 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1