Anne is nice. Dave is furry. Dave is nice. Dave is young. Harry is blue. Harry is kind. Harry is nice. If someone is young then they are blue. Blue people are white. Nice, furry people are young.
Anne is nice.
("Anne" "is" "nice" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If someone is young then they are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Nice, furry people are young.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Harry is nice.
True
1
proof
[(triple7)]
("Harry" "is" "nice" "+")
triple7
Harry is not blue.
False
1
inv-proof
[(triple5)]
("Harry" "is" "blue" "-")
triple5
Dave is blue.
True
2
proof
[(((triple4) -> rule1) OR ((((triple3 triple2) -> rule3)) -> rule1))]
("Dave" "is" "blue" "+")
((triple4) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not blue.
False
2
inv-proof
[(((triple4) -> rule1) OR ((((triple3 triple2) -> rule3)) -> rule1))]
("Dave" "is" "blue" "-")
((triple4) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is white.
True
3
proof
[(((((triple4) -> rule1)) -> rule2) OR ((((((triple3 triple2) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "white" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((((triple3 triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not white.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2) OR ((((((triple3 triple2) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "white" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((((triple3 triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Anne is not white.
Unknown
inv-rconc
[@3: Anne is white.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule3 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is blue.
Unknown
rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Anne" "is" "blue" "+")
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Anne is nice.[(triple1)] Dave is furry.[(triple2)] Dave is nice.[(triple3)] Dave is young.[(triple4 OR ((triple3 triple2) -> rule3))] Harry is blue.[(triple5)] Harry is kind.[(triple6)] Harry is nice.[(triple7)] @1: Dave is blue.[(((triple4) -> rule1) OR ((((triple3 triple2) -> rule3)) -> rule1))] Harry is white.[(((triple5) -> rule2))] @2: Dave is white.[(((((triple4) -> rule1)) -> rule2) OR ((((((triple3 triple2) -> rule3)) -> rule1)) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
((triple3 triple2) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
((triple4) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((triple5) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((((triple3 triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3