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