The bear is big. If something is young and round then it is big. If something is red then it is not young. Big things are cold. If the bear is young then the bear is cold. If the bear is big and the bear is young then the bear is not cold. If the bear is cold then the bear is red.
The bear is big.
("bear" "is" "big" "+")
If something is young and round then it is big.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something is red then it is not young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "-"))
Big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If the bear is young then the bear is cold.
((("bear" "is" "young" "+")) -> ("bear" "is" "cold" "+"))
If the bear is big and the bear is young then the bear is not cold.
((("bear" "is" "big" "+") ("bear" "is" "young" "+")) -> ("bear" "is" "cold" "-"))
If the bear is cold then the bear is red.
((("bear" "is" "cold" "+")) -> ("bear" "is" "red" "+"))
The bear is big.
True
1
proof
[(triple1)]
("bear" "is" "big" "+")
triple1
The bear is not big.
False
1
inv-proof
[(triple1)]
("bear" "is" "big" "-")
triple1
The bear is cold.
True
2
proof
[(((triple1) -> rule3))]
("bear" "is" "cold" "+")
((triple1) -> (rule3 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "is" "cold" "-")
((triple1) -> (rule3 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is red.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("bear" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is not red.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("bear" "is" "red" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is not young.
True
4
proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule2))]
("bear" "is" "young" "-")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bear is not young.
("bear" "is" "young" "-")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The bear is young.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule2))]
("bear" "is" "young" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bear is not young.
("bear" "is" "young" "-")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
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 is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear is big.[(triple1)] @1: The bear is cold.[(((triple1) -> rule3))] @2: The bear is red.[(((((triple1) -> rule3)) -> rule6))] @3: The bear is not young.[(((((((triple1) -> rule3)) -> rule6)) -> rule2))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
((triple1) -> (rule3 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is red.
("bear" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is not young.
("bear" "is" "young" "-")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bear is not young.
("bear" "is" "young" "-")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3