Anne is young. Charlie is furry. Harry is blue. All blue people are young. All furry, white people are kind. If someone is white then they are furry. If Harry is quiet then Harry is white. All blue, kind people are nice. All young people are kind.
Anne is young.
("Anne" "is" "young" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Harry is blue.
("Harry" "is" "blue" "+")
All blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
All furry, white people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If someone is white then they are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If Harry is quiet then Harry is white.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "white" "+"))
All blue, kind people are nice.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
All young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Charlie is furry.
True
1
proof
[(triple2)]
("Charlie" "is" "furry" "+")
triple2
Harry is not blue.
False
1
inv-proof
[(triple3)]
("Harry" "is" "blue" "-")
triple3
Anne is kind.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "young" "-")
((triple3) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is kind.
True
3
proof
[(((((triple3) -> rule1)) -> rule6))]
("Harry" "is" "kind" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not kind.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule6))]
("Harry" "is" "kind" "-")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is nice.
True
5
proof
[(((triple3 ((((triple3) -> rule1)) -> rule6)) -> rule5))]
("Harry" "is" "nice" "+")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not nice.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule1)) -> rule6)) -> rule5))]
("Harry" "is" "nice" "-")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is kind.
Unknown
rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "kind" "+")
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "white" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Anne is young.[(triple1)] Charlie is furry.[(triple2)] Harry is blue.[(triple3)] @1: Anne is kind.[(((triple1) -> rule6))] Harry is young.[(((triple3) -> rule1))] @2: Harry is kind.[(((((triple3) -> rule1)) -> rule6))] @3: Harry is nice.[(((triple3 ((((triple3) -> rule1)) -> rule6)) -> rule5))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple3) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3