Anne is blue. Bob is furry. Harry is not blue. If Anne is blue then Anne is quiet. Big, blue people are quiet. Blue people are not young. If Anne is young then Anne is not furry. If someone is quiet then they are white. If someone is furry and not big then they are not blue. If someone is young and not furry then they are smart. White people are smart.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
If Anne is blue then Anne is quiet.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "quiet" "+"))
Big, blue people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
Blue people are not young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "-"))
If Anne is young then Anne is not furry.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "furry" "-"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is furry and not big then they are not blue.
((("someone" "is" "furry" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "blue" "-"))
If someone is young and not furry then they are smart.
((("someone" "is" "young" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "smart" "+"))
White people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
Bob is furry.
True
1
proof
[(triple2)]
("Bob" "is" "furry" "+")
triple2
Harry is blue.
False
1
inv-proof
[(triple3)]
("Harry" "is" "blue" "+")
triple3
Anne is quiet.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "white" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
True
4
proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule8))]
("Anne" "is" "smart" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not smart.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule8))]
("Anne" "is" "smart" "-")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Harry is not white.
Unknown
inv-rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Harry" "is" "white" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "quiet" "+")
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "quiet" "-")
Bob is white.
Unknown
rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Bob" "is" "white" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Anne is blue.[(triple1)] Bob is furry.[(triple2)] Harry is not blue.[(triple3)] @1: Anne is not young.[(((triple1) -> rule3))] Anne is quiet.[(((triple1) -> rule1))] @2: Anne is white.[(((((triple1) -> rule1)) -> rule5))] @3: Anne is smart.[(((((((triple1) -> rule1)) -> rule5)) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Harry is not blue.
("Harry" "is" "blue" "-")
triple3
Anne is not young.
("Anne" "is" "young" "-")
((triple1) -> (rule3 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3