Anne is kind. Charlie is young. Quiet people are smart. Smart, rough people are nice. If someone is smart then they are not rough. If Charlie is kind and Charlie is smart then Charlie is not rough. All kind people are not young. All rough people are not young. All young people are red. If someone is smart and not nice then they are red.
Anne is kind.
("Anne" "is" "kind" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Smart, rough people are nice.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is smart then they are not rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "-"))
If Charlie is kind and Charlie is smart then Charlie is not rough.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "rough" "-"))
All kind people are not young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "-"))
All rough people are not young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "-"))
All young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is smart and not nice then they are red.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "red" "+"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Charlie is not young.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "young" "-")
triple2
Anne is not young.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "young" "-")
((triple1) -> (rule5 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Charlie is not red.
False
2
inv-proof
[(((triple2) -> rule7))]
("Charlie" "is" "red" "-")
((triple2) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "red" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "nice" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is kind.[(triple1)] Charlie is young.[(triple2)] @1: Anne is not young.[(((triple1) -> rule5))] Charlie is red.[(((triple2) -> rule7))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Anne is not young.
("Anne" "is" "young" "-")
((triple1) -> (rule5 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple2) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1