Anne is quiet. Charlie is furry. Fiona is cold. Harry is not quiet. All quiet people are not young. All quiet, cold people are not furry. Furry people are quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
All quiet people are not young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "-"))
All quiet, cold people are not furry.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "-"))
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Harry is not quiet.
True
1
proof
[(triple4)]
("Harry" "is" "quiet" "-")
triple4
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Charlie is quiet.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Anne is young.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Charlie is not young.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("Charlie" "is" "young" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("Charlie" "is" "young" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Anne is quiet.[(triple1)] Charlie is furry.[(triple2)] Fiona is cold.[(triple3)] Harry is not quiet.[(triple4)] @1: Anne is not young.[(((triple1) -> rule1))] Charlie is quiet.[(((triple2) -> rule3))] @2: Charlie is not young.[(((((triple2) -> rule3)) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple4
Anne is not young.
("Anne" "is" "young" "-")
((triple1) -> (rule1 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2