The bear is not big. The bear is blue. The bear is red. The bear is not round. The bear likes the rabbit. The bear does not see the rabbit. The bear visits the rabbit. The rabbit is not blue. The rabbit is cold. The rabbit likes the bear. The rabbit does not see the bear. The rabbit visits the bear. If something sees the bear then the bear does not see the rabbit. If the bear sees the rabbit and the rabbit sees the bear then the rabbit is not cold. If something is red and not big then it does not see the bear. If something visits the bear and the bear sees the rabbit then it does not see the bear. If something likes the bear then it is cold. If something visits the rabbit then the rabbit visits the bear. If something visits the rabbit then the rabbit does not see the bear. If something visits the bear then it likes the rabbit.
The bear is not big.
("bear" "is" "big" "-")
The bear is blue.
("bear" "is" "blue" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is not round.
("bear" "is" "round" "-")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear does not see the rabbit.
("bear" "sees" "rabbit" "-")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The rabbit is not blue.
("rabbit" "is" "blue" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
If something sees the bear then the bear does not see the rabbit.
((("something" "sees" "bear" "+")) -> ("bear" "sees" "rabbit" "-"))
If the bear sees the rabbit and the rabbit sees the bear then the rabbit is not cold.
((("bear" "sees" "rabbit" "+") ("rabbit" "sees" "bear" "+")) -> ("rabbit" "is" "cold" "-"))
If something is red and not big then it does not see the bear.
((("something" "is" "red" "+") ("something" "is" "big" "~")) -> ("something" "sees" "bear" "-"))
If something visits the bear and the bear sees the rabbit then it does not see the bear.
((("something" "visits" "bear" "+") ("bear" "sees" "rabbit" "+")) -> ("something" "sees" "bear" "-"))
If something likes the bear then it is cold.
((("something" "likes" "bear" "+")) -> ("something" "is" "cold" "+"))
If something visits the rabbit then the rabbit visits the bear.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "visits" "bear" "+"))
If something visits the rabbit then the rabbit does not see the bear.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "sees" "bear" "-"))
If something visits the bear then it likes the rabbit.
((("something" "visits" "bear" "+")) -> ("something" "likes" "rabbit" "+"))
The rabbit visits the bear.
True
1
proof
[(triple12 OR ((triple7) -> rule6))]
("rabbit" "visits" "bear" "+")
triple12
((triple7) -> (rule6 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is blue.
False
1
inv-proof
[(triple8)]
("rabbit" "is" "blue" "+")
triple8
The bear is not cold.
Unknown
inv-rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "cold" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear does not see the rabbit.[(triple6)] The bear is blue.[(triple2)] The bear is not big.[(triple1)] The bear is not round.[(triple4)] The bear is red.[(triple3)] The bear likes the rabbit.[(triple5)] The bear visits the rabbit.[(triple7)] The rabbit does not see the bear.[(triple11 OR ((triple7) -> rule7))] The rabbit is cold.[(triple9 OR ((triple10) -> rule5))] The rabbit is not blue.[(triple8)] The rabbit likes the bear.[(triple10)] The rabbit visits the bear.[(triple12 OR ((triple7) -> rule6))] @1: The bear does not see the bear.[(((triple3 triple1) -> rule3))] The rabbit likes the rabbit.[(((triple12) -> rule8) OR ((((triple7) -> rule6)) -> rule8))]
The bear does not see the rabbit.
("bear" "sees" "rabbit" "-")
triple6
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is not big.
("bear" "is" "big" "-")
triple1
The bear is not round.
("bear" "is" "round" "-")
triple4
The bear is red.
("bear" "is" "red" "+")
triple3
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple5
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple7
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
triple11
((triple7) -> (rule7 % int1))
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple9
((triple10) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is not blue.
("rabbit" "is" "blue" "-")
triple8
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple10
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple12
((triple7) -> (rule6 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The bear does not see the bear.
("bear" "sees" "bear" "-")
((triple3 triple1) -> (rule3 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple12) -> (rule8 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2