The bear is cold. The bear is green. The bear needs the rabbit. The bear visits the rabbit. The rabbit eats the bear. The rabbit eats the tiger. The rabbit is not nice. The rabbit needs the tiger. The rabbit visits the bear. The tiger eats the bear. The tiger is round. The tiger needs the bear. If something eats the bear then it is red. If the rabbit eats the tiger then the rabbit needs the tiger. If something is green then it eats the bear.
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is not nice.
("rabbit" "is" "nice" "-")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
If something eats the bear then it is red.
((("something" "eats" "bear" "+")) -> ("something" "is" "red" "+"))
If the rabbit eats the tiger then the rabbit needs the tiger.
((("rabbit" "eats" "tiger" "+")) -> ("rabbit" "needs" "tiger" "+"))
If something is green then it eats the bear.
((("something" "is" "green" "+")) -> ("something" "eats" "bear" "+"))
The rabbit eats the tiger.
True
1
proof
[(triple6)]
("rabbit" "eats" "tiger" "+")
triple6
The bear does not need the rabbit.
False
1
inv-proof
[(triple3)]
("bear" "needs" "rabbit" "-")
triple3
The bear eats the bear.
True
2
proof
[(((triple2) -> rule3))]
("bear" "eats" "bear" "+")
((triple2) -> (rule3 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The rabbit is not red.
False
2
inv-proof
[(((triple5) -> rule1))]
("rabbit" "is" "red" "-")
((triple5) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The bear is red.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("bear" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The bear is not red.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("bear" "is" "red" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The tiger visits the bear.
Unknown
random
[@0: The tiger visits the bear.[CWA. Example of deepest failure = (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 tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
@0: The bear is cold.[(triple1)] The bear is green.[(triple2)] The bear needs the rabbit.[(triple3)] The bear visits the rabbit.[(triple4)] The rabbit eats the bear.[(triple5)] The rabbit eats the tiger.[(triple6)] The rabbit is not nice.[(triple7)] The rabbit needs the tiger.[(triple8 OR ((triple6) -> rule2))] The rabbit visits the bear.[(triple9)] The tiger eats the bear.[(triple10)] The tiger is round.[(triple11)] The tiger needs the bear.[(triple12)] @1: The bear eats the bear.[(((triple2) -> rule3))] The rabbit is red.[(((triple5) -> rule1))] The tiger is red.[(((triple10) -> rule1))] @2: The bear is red.[(((((triple2) -> rule3)) -> rule1))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear is green.
("bear" "is" "green" "+")
triple2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple3
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple4
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple5
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple6
The rabbit is not nice.
("rabbit" "is" "nice" "-")
triple7
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple8
((triple6) -> (rule2 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple9
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple10
The tiger is round.
("tiger" "is" "round" "+")
triple11
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple12
The bear eats the bear.
("bear" "eats" "bear" "+")
((triple2) -> (rule3 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
((triple5) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
((triple10) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The bear is red.
("bear" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2