Anne is nice. Charlie is nice. Furry people are rough. All smart people are rough. If someone is nice then they are smart. If someone is furry then they are nice. All nice, cold people are rough. If someone is nice and white then they are smart.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Furry people are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
All smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If someone is nice then they are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is furry then they are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All nice, cold people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone is nice and white then they are smart.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Charlie is smart.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "smart" "-")
((triple2) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is nice.[(triple1)] Charlie is nice.[(triple2)] @1: Anne is smart.[(((triple1) -> rule3))] Charlie is smart.[(((triple2) -> rule3))] @2: Anne is rough.[(((((triple1) -> rule3)) -> rule2))] Charlie is rough.[(((((triple2) -> rule3)) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2