Anne is furry. Charlie is red. Dave is smart. Harry is big. All furry people are red. If someone is red then they are not young.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
All furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If someone is red then they are not young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "-"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Anne is red.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "red" "+")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Charlie is young.
False
2
inv-proof
[(((triple2) -> rule2))]
("Charlie" "is" "young" "+")
((triple2) -> (rule2 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Anne is not young.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Anne" "is" "young" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is young.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Anne" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "red" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "red" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Anne is furry.[(triple1)] Charlie is red.[(triple2)] Dave is smart.[(triple3)] Harry is big.[(triple4)] @1: Anne is red.[(((triple1) -> rule1))] Charlie is not young.[(((triple2) -> rule2))] @2: Anne is not young.[(((((triple1) -> rule1)) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
((triple2) -> (rule2 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Anne is not young.
("Anne" "is" "young" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2