The bear is round. Nice, blue people are cold. All cold people are not round. If someone is cold and not blue then they are round. All blue people are not round. All cold, kind people are not nice. If someone is round and kind then they are not nice. If the bear is round then the bear is kind. If the bear is kind then the bear is not nice.
The bear is round.
("bear" "is" "round" "+")
Nice, blue people are cold.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All cold people are not round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "-"))
If someone is cold and not blue then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "round" "+"))
All blue people are not round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "-"))
All cold, kind people are not nice.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "-"))
If someone is round and kind then they are not nice.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "-"))
If the bear is round then the bear is kind.
((("bear" "is" "round" "+")) -> ("bear" "is" "kind" "+"))
If the bear is kind then the bear is not nice.
((("bear" "is" "kind" "+")) -> ("bear" "is" "nice" "-"))
The bear is round.
True
1
proof
[(triple1)]
("bear" "is" "round" "+")
triple1
The bear is not round.
False
1
inv-proof
[(triple1)]
("bear" "is" "round" "-")
triple1
The bear is kind.
True
2
proof
[(((triple1) -> rule7))]
("bear" "is" "kind" "+")
((triple1) -> (rule7 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is not kind.
False
2
inv-proof
[(((triple1) -> rule7))]
("bear" "is" "kind" "-")
((triple1) -> (rule7 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is not nice.
True
3
proof
[(((((triple1) -> rule7)) -> rule8) OR ((triple1 ((triple1) -> rule7)) -> rule6))]
("bear" "is" "nice" "-")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear is nice.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule8) OR ((triple1 ((triple1) -> rule7)) -> rule6))]
("bear" "is" "nice" "+")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear is not cold.
Unknown
inv-rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "cold" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "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 round.[(triple1)] @1: The bear is kind.[(((triple1) -> rule7))] @2: The bear is not nice.[(((((triple1) -> rule7)) -> rule8) OR ((triple1 ((triple1) -> rule7)) -> rule6))]
The bear is round.
("bear" "is" "round" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
((triple1) -> (rule7 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is not nice.
("bear" "is" "nice" "-")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2