The bear is rough. Red things are big. If something is rough and red then it is big. All young things are red. Big, cold things are red. If something is young and not rough then it is cold. If something is young then it is cold. If the bear is big and the bear is young then the bear is red. All rough things are young.
The bear is rough.
("bear" "is" "rough" "+")
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is rough and red then it is big.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
All young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Big, cold things are red.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is young and not rough then it is cold.
((("something" "is" "young" "+") ("something" "is" "rough" "~")) -> ("something" "is" "cold" "+"))
If something is young then it is cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If the bear is big and the bear is young then the bear is red.
((("bear" "is" "big" "+") ("bear" "is" "young" "+")) -> ("bear" "is" "red" "+"))
All rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
The bear is rough.
True
1
proof
[(triple1)]
("bear" "is" "rough" "+")
triple1
The bear is not rough.
False
1
inv-proof
[(triple1)]
("bear" "is" "rough" "-")
triple1
The bear is young.
True
2
proof
[(((triple1) -> rule8))]
("bear" "is" "young" "+")
((triple1) -> (rule8 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is not young.
False
2
inv-proof
[(((triple1) -> rule8))]
("bear" "is" "young" "-")
((triple1) -> (rule8 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is red.
True
3
proof
[(((((triple1) -> rule8)) -> rule3))]
("bear" "is" "red" "+")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is not red.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule3))]
("bear" "is" "red" "-")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is big.
True
4
proof
[(((((((triple1) -> rule8)) -> rule3)) -> rule1) OR ((triple1 ((((triple1) -> rule8)) -> rule3)) -> rule2))]
("bear" "is" "big" "+")
((((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
((triple1 ((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear is not big.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule3)) -> rule1) OR ((triple1 ((((triple1) -> rule8)) -> rule3)) -> rule2))]
("bear" "is" "big" "-")
((((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
((triple1 ((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
@0: The bear is rough.[(triple1)] @1: The bear is young.[(((triple1) -> rule8))] @2: The bear is cold.[(((((triple1) -> rule8)) -> rule6))] The bear is red.[(((((triple1) -> rule8)) -> rule3))] @3: The bear is big.[(((((((triple1) -> rule8)) -> rule3)) -> rule1) OR ((triple1 ((((triple1) -> rule8)) -> rule3)) -> rule2))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
((triple1) -> (rule8 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is red.
("bear" "is" "red" "+")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is big.
("bear" "is" "big" "+")
((((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
((triple1 ((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3