The bear is kind. If something is kind and big then it is round. If something is cold then it is big. Nice things are big. If something is big then it is kind. All cold, nice things are round. Cold things are kind. If the bear is cold then the bear is round. If something is kind then it is cold.
The bear is kind.
("bear" "is" "kind" "+")
If something is kind and big then it is round.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
All cold, nice things are round.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If the bear is cold then the bear is round.
((("bear" "is" "cold" "+")) -> ("bear" "is" "round" "+"))
If something is kind then it is cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
The bear is kind.
True
1
proof
[(triple1)]
("bear" "is" "kind" "+")
triple1
The bear is not kind.
False
1
inv-proof
[(triple1)]
("bear" "is" "kind" "-")
triple1
The bear is cold.
True
2
proof
[(((triple1) -> rule8))]
("bear" "is" "cold" "+")
((triple1) -> (rule8 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is not cold.
False
2
inv-proof
[(((triple1) -> rule8))]
("bear" "is" "cold" "-")
((triple1) -> (rule8 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is big.
True
3
proof
[(((((triple1) -> rule8)) -> rule2))]
("bear" "is" "big" "+")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is not big.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule2))]
("bear" "is" "big" "-")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
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 likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear is kind.[(triple1)] @1: The bear is cold.[(((triple1) -> rule8))] @2: The bear is big.[(((((triple1) -> rule8)) -> rule2))] The bear is round.[(((((triple1) -> rule8)) -> rule7) OR ((triple1 ((((triple1) -> rule8)) -> rule2)) -> rule1))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
((triple1) -> (rule8 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is big.
("bear" "is" "big" "+")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is round.
("bear" "is" "round" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
((triple1 ((((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3