Anne is blue. Dave is blue. Harry is round. All smart people are furry. If someone is green and round then they are smart. If someone is round then they are green.
Anne is blue.
("Anne" "is" "blue" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Harry is round.
("Harry" "is" "round" "+")
All smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is green and round then they are smart.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Harry is green.
True
2
proof
[(((triple3) -> rule3))]
("Harry" "is" "green" "+")
((triple3) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "green" "-")
((triple3) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
True
4
proof
[(((((triple3) -> rule3) triple3) -> rule2))]
("Harry" "is" "smart" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not smart.
False
4
inv-proof
[(((((triple3) -> rule3) triple3) -> rule2))]
("Harry" "is" "smart" "-")
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Dave is not furry.
Unknown
inv-rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "furry" "-")
Anne is furry.
Unknown
rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "green" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is blue.[(triple1)] Dave is blue.[(triple2)] Harry is round.[(triple3)] @1: Harry is green.[(((triple3) -> rule3))] @2: Harry is smart.[(((((triple3) -> rule3) triple3) -> rule2))] @3: Harry is furry.[(((((((triple3) -> rule3) triple3) -> rule2)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
((triple3) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3