The bear is cold. Cold people are nice. All big people are nice. Nice, young people are not big. Cold people are not big. If someone is cold and nice then they are young. If someone is young and not big then they are rough.
The bear is cold.
("bear" "is" "cold" "+")
Cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
All big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Nice, young people are not big.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "-"))
Cold people are not big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "-"))
If someone is cold and nice then they are young.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone is young and not big then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "rough" "+"))
The bear is cold.
True
1
proof
[(triple1)]
("bear" "is" "cold" "+")
triple1
The bear is not cold.
False
1
inv-proof
[(triple1)]
("bear" "is" "cold" "-")
triple1
The bear is nice.
True
2
proof
[(((triple1) -> rule1))]
("bear" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is big.
False
2
inv-proof
[(((triple1) -> rule4) OR ((((triple1) -> rule1) ((triple1 ((triple1) -> rule1)) -> rule5)) -> rule3))]
("bear" "is" "big" "+")
((triple1) -> (rule4 % int1))
The bear is not big.
("bear" "is" "big" "-")
int1
((((triple1) -> (rule1 % int3)) ((triple1 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The bear is not big.
("bear" "is" "big" "-")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear is young.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule5))]
("bear" "is" "young" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is not young.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule5))]
("bear" "is" "young" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is rough.
True
7
proof
[(((((triple1 ((triple1) -> rule1)) -> rule5) ((triple1) -> rule4)) -> rule6) OR ((((triple1 ((triple1) -> rule1)) -> rule5) ((((triple1) -> rule1) ((triple1 ((triple1) -> rule1)) -> rule5)) -> rule3)) -> rule6))]
("bear" "is" "rough" "+")
((((triple1 ((triple1) -> (rule1 % int4))) -> (rule5 % int3)) ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is not big.
("bear" "is" "big" "-")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
((((triple1 ((triple1) -> (rule1 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule1 % int4)) ((triple1 ((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is not big.
("bear" "is" "big" "-")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
The bear is not rough.
False
7
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule5) ((triple1) -> rule4)) -> rule6) OR ((((triple1 ((triple1) -> rule1)) -> rule5) ((((triple1) -> rule1) ((triple1 ((triple1) -> rule1)) -> rule5)) -> rule3)) -> rule6))]
("bear" "is" "rough" "-")
((((triple1 ((triple1) -> (rule1 % int4))) -> (rule5 % int3)) ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is not big.
("bear" "is" "big" "-")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
((((triple1 ((triple1) -> (rule1 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule1 % int4)) ((triple1 ((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is not big.
("bear" "is" "big" "-")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
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 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 cold.[(triple1)] @1: The bear is nice.[(((triple1) -> rule1))] The bear is not big.[(((triple1) -> rule4) OR ((((triple1) -> rule1) ((triple1 ((triple1) -> rule1)) -> rule5)) -> rule3))] @2: The bear is young.[(((triple1 ((triple1) -> rule1)) -> rule5))] @3: The bear is rough.[(((((triple1 ((triple1) -> rule1)) -> rule5) ((triple1) -> rule4)) -> rule6) OR ((((triple1 ((triple1) -> rule1)) -> rule5) ((((triple1) -> rule1) ((triple1 ((triple1) -> rule1)) -> rule5)) -> rule3)) -> rule6))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is not big.
("bear" "is" "big" "-")
((triple1) -> (rule4 % int1))
The bear is not big.
("bear" "is" "big" "-")
int1
((((triple1) -> (rule1 % int3)) ((triple1 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The bear is not big.
("bear" "is" "big" "-")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear is young.
("bear" "is" "young" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
((((triple1 ((triple1) -> (rule1 % int4))) -> (rule5 % int3)) ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is not big.
("bear" "is" "big" "-")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
((((triple1 ((triple1) -> (rule1 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule1 % int4)) ((triple1 ((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is not big.
("bear" "is" "big" "-")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4