The bear eats the rabbit. The bear is big. The bear is round. The bear does not need the rabbit. The bear sees the rabbit. The rabbit eats the bear. The rabbit is big. The rabbit is cold. The rabbit needs the bear. The rabbit sees the bear. If the rabbit is red and the rabbit sees the bear then the rabbit eats the bear. If something is big then it eats the bear.
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is round.
("bear" "is" "round" "+")
The bear does not need the rabbit.
("bear" "needs" "rabbit" "-")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
If the rabbit is red and the rabbit sees the bear then the rabbit eats the bear.
((("rabbit" "is" "red" "+") ("rabbit" "sees" "bear" "+")) -> ("rabbit" "eats" "bear" "+"))
If something is big then it eats the bear.
((("something" "is" "big" "+")) -> ("something" "eats" "bear" "+"))
The bear does not need the rabbit.
True
1
proof
[(triple4)]
("bear" "needs" "rabbit" "-")
triple4
The rabbit does not eat the bear.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule2))]
("rabbit" "eats" "bear" "-")
triple6
((triple7) -> (rule2 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The bear eats the bear.
True
2
proof
[(((triple2) -> rule2))]
("bear" "eats" "bear" "+")
((triple2) -> (rule2 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear does not eat the bear.
False
2
inv-proof
[(((triple2) -> rule2))]
("bear" "eats" "bear" "-")
((triple2) -> (rule2 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
@0: The bear does not need the rabbit.[(triple4)] The bear eats the rabbit.[(triple1)] The bear is big.[(triple2)] The bear is round.[(triple3)] The bear sees the rabbit.[(triple5)] The rabbit eats the bear.[(triple6 OR ((triple7) -> rule2))] The rabbit is big.[(triple7)] The rabbit is cold.[(triple8)] The rabbit needs the bear.[(triple9)] The rabbit sees the bear.[(triple10)] @1: The bear eats the bear.[(((triple2) -> rule2))]
The bear does not need the rabbit.
("bear" "needs" "rabbit" "-")
triple4
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is round.
("bear" "is" "round" "+")
triple3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple5
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple6
((triple7) -> (rule2 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple8
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple9
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple10
The bear eats the bear.
("bear" "eats" "bear" "+")
((triple2) -> (rule2 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1