The bear chases the rabbit. The bear is cold. The bear is red. The bear is round. The bear sees the rabbit. The bear visits the rabbit. The rabbit chases the bear. The rabbit is cold. The rabbit is red. The rabbit is round. If someone is big then they see the rabbit. If someone chases the rabbit and the rabbit chases the bear then the rabbit is big.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is round.
("bear" "is" "round" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
If someone is big then they see the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone chases the rabbit and the rabbit chases the bear then the rabbit is big.
((("someone" "chases" "rabbit" "+") ("rabbit" "chases" "bear" "+")) -> ("rabbit" "is" "big" "+"))
The bear sees the rabbit.
True
1
proof
[(triple5)]
("bear" "sees" "rabbit" "+")
triple5
The bear is not red.
False
1
inv-proof
[(triple3)]
("bear" "is" "red" "-")
triple3
The rabbit is big.
True
3
proof
[(((triple1 triple7) -> rule2))]
("rabbit" "is" "big" "+")
((triple1 triple7) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is not big.
False
3
inv-proof
[(((triple1 triple7) -> rule2))]
("rabbit" "is" "big" "-")
((triple1 triple7) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit sees the rabbit.
True
4
proof
[(((((triple1 triple7) -> rule2)) -> rule1))]
("rabbit" "sees" "rabbit" "+")
((((triple1 triple7) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit does not see the rabbit.
False
4
inv-proof
[(((((triple1 triple7) -> rule2)) -> rule1))]
("rabbit" "sees" "rabbit" "-")
((((triple1 triple7) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The bear is nice.
Unknown
random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "+")
@0: The bear chases the rabbit.[(triple1)] The bear is cold.[(triple2)] The bear is red.[(triple3)] The bear is round.[(triple4)] The bear sees the rabbit.[(triple5)] The bear visits the rabbit.[(triple6)] The rabbit chases the bear.[(triple7)] The rabbit is cold.[(triple8)] The rabbit is red.[(triple9)] The rabbit is round.[(triple10)] @1: The rabbit is big.[(((triple1 triple7) -> rule2))] @2: The rabbit sees the rabbit.[(((((triple1 triple7) -> rule2)) -> rule1))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is red.
("bear" "is" "red" "+")
triple3
The bear is round.
("bear" "is" "round" "+")
triple4
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple5
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple6
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple8
The rabbit is red.
("rabbit" "is" "red" "+")
triple9
The rabbit is round.
("rabbit" "is" "round" "+")
triple10
The rabbit is big.
("rabbit" "is" "big" "+")
((triple1 triple7) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((triple1 triple7) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2