The bear is green. The bear is red. The bear is rough. If the bear is big then the bear is not nice. If something is green and not red then it is big. All green things are big. If something is red then it is big. If the bear is green then the bear is rough. If something is big and not red then it is not nice.
The bear is green.
("bear" "is" "green" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is rough.
("bear" "is" "rough" "+")
If the bear is big then the bear is not nice.
((("bear" "is" "big" "+")) -> ("bear" "is" "nice" "-"))
If something is green and not red then it is big.
((("something" "is" "green" "+") ("something" "is" "red" "~")) -> ("something" "is" "big" "+"))
All green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is red then it is big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If the bear is green then the bear is rough.
((("bear" "is" "green" "+")) -> ("bear" "is" "rough" "+"))
If something is big and not red then it is not nice.
((("something" "is" "big" "+") ("something" "is" "red" "~")) -> ("something" "is" "nice" "-"))
The bear is red.
True
1
proof
[(triple2)]
("bear" "is" "red" "+")
triple2
The bear is not red.
False
1
inv-proof
[(triple2)]
("bear" "is" "red" "-")
triple2
The bear is big.
True
2
proof
[(((triple1) -> rule3) OR ((triple2) -> rule4))]
("bear" "is" "big" "+")
((triple1) -> (rule3 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
((triple2) -> (rule4 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is not big.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple2) -> rule4))]
("bear" "is" "big" "-")
((triple1) -> (rule3 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
((triple2) -> (rule4 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is not nice.
True
3
proof
[(((((triple1) -> rule3)) -> rule1) OR ((((triple2) -> rule4)) -> rule1))]
("bear" "is" "nice" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The bear is big.
("bear" "is" "big" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is nice.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1) OR ((((triple2) -> rule4)) -> rule1))]
("bear" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The bear is big.
("bear" "is" "big" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The bear is big.
("bear" "is" "big" "+")
int2
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 eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
@0: The bear is green.[(triple1)] The bear is red.[(triple2)] The bear is rough.[(triple3 OR ((triple1) -> rule5))] @1: The bear is big.[(((triple1) -> rule3) OR ((triple2) -> rule4))] @2: The bear is not nice.[(((((triple1) -> rule3)) -> rule1) OR ((((triple2) -> rule4)) -> rule1))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear is red.
("bear" "is" "red" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
((triple1) -> (rule5 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is big.
("bear" "is" "big" "+")
((triple1) -> (rule3 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
((triple2) -> (rule4 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is not nice.
("bear" "is" "nice" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The bear is big.
("bear" "is" "big" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The bear is big.
("bear" "is" "big" "+")
int2