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