The bear is red. If something is red then it is round. If something is green then it is round. If something is cold and not green then it is not round. If something is cold and round then it is red. Round things are nice. Round, nice things are not cold.
The bear is red.
("bear" "is" "red" "+")
If something is red then it is round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If something is green then it is round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something is cold and not green then it is not round.
((("something" "is" "cold" "+") ("something" "is" "green" "~")) -> ("something" "is" "round" "-"))
If something is cold and round then it is red.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Round, nice things are not cold.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "-"))
The bear is red.
True
1
proof
[(triple1)]
("bear" "is" "red" "+")
triple1
The bear is not red.
False
1
inv-proof
[(triple1)]
("bear" "is" "red" "-")
triple1
The bear is round.
True
2
proof
[(((triple1) -> rule1))]
("bear" "is" "round" "+")
((triple1) -> (rule1 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "is" "round" "-")
((triple1) -> (rule1 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is nice.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("bear" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is not nice.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("bear" "is" "nice" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is round.
("bear" "is" "round" "+")
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 visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The bear is not green.
Unknown
inv-random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "-")
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 red.[(triple1)] @1: The bear is round.[(((triple1) -> rule1))] @2: The bear is nice.[(((((triple1) -> rule1)) -> rule5))] @3: The bear is not cold.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule5)) -> rule6))]
The bear is red.
("bear" "is" "red" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
((triple1) -> (rule1 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is not cold.
("bear" "is" "cold" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The bear is not cold.
("bear" "is" "cold" "-")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3