Anne is furry. Anne is kind. Anne is rough. Anne is young. Bob is furry. Bob is not green. Bob is not kind. Charlie is furry. Charlie is round. Charlie is smart. If someone is furry and green then they are young. If someone is smart then they are green. If someone is young and furry then they are kind.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is not kind.
("Bob" "is" "kind" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
If someone is furry and green then they are young.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is smart then they are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is young and furry then they are kind.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Charlie is not furry.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "furry" "-")
triple8
Charlie is green.
True
2
proof
[(((triple10) -> rule2))]
("Charlie" "is" "green" "+")
((triple10) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple10) -> rule2))]
("Charlie" "is" "green" "-")
((triple10) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
True
4
proof
[(((triple8 ((triple10) -> rule2)) -> rule1))]
("Charlie" "is" "young" "+")
((triple8 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not young.
False
4
inv-proof
[(((triple8 ((triple10) -> rule2)) -> rule1))]
("Charlie" "is" "young" "-")
((triple8 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is kind.
True
6
proof
[(((((triple8 ((triple10) -> rule2)) -> rule1) triple8) -> rule3))]
("Charlie" "is" "kind" "+")
((((triple8 ((triple10) -> (rule2 % int3))) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is not kind.
False
6
inv-proof
[(((((triple8 ((triple10) -> rule2)) -> rule1) triple8) -> rule3))]
("Charlie" "is" "kind" "-")
((((triple8 ((triple10) -> (rule2 % int3))) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "young" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2 OR ((triple4 triple1) -> rule3))] Anne is rough.[(triple3)] Anne is young.[(triple4)] Bob is furry.[(triple5)] Bob is not green.[(triple6)] Bob is not kind.[(triple7)] Charlie is furry.[(triple8)] Charlie is round.[(triple9)] Charlie is smart.[(triple10)] @1: Charlie is green.[(((triple10) -> rule2))] @2: Charlie is young.[(((triple8 ((triple10) -> rule2)) -> rule1))] @3: Charlie is kind.[(((((triple8 ((triple10) -> rule2)) -> rule1) triple8) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple4 triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Bob is furry.
("Bob" "is" "furry" "+")
triple5
Bob is not green.
("Bob" "is" "green" "-")
triple6
Bob is not kind.
("Bob" "is" "kind" "-")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
Charlie is round.
("Charlie" "is" "round" "+")
triple9
Charlie is smart.
("Charlie" "is" "smart" "+")
triple10
Charlie is green.
("Charlie" "is" "green" "+")
((triple10) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple8 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple8 ((triple10) -> (rule2 % int3))) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3