Dave is smart. Harry is rough. All kind, furry things are smart. If something is blue then it is rough. If something is smart then it is not furry. All smart things are blue. If something is blue and round then it is green. Smart, furry things are not green. If something is green and not furry then it is round. Blue, smart things are round.
Dave is smart.
("Dave" "is" "smart" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All kind, furry things are smart.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is smart then it is not furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "-"))
All smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If something is blue and round then it is green.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Smart, furry things are not green.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "-"))
If something is green and not furry then it is round.
((("something" "is" "green" "+") ("something" "is" "furry" "~")) -> ("something" "is" "round" "+"))
Blue, smart things are round.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Harry is rough.
True
1
proof
[(triple2)]
("Harry" "is" "rough" "+")
triple2
Dave is not smart.
False
1
inv-proof
[(triple1)]
("Dave" "is" "smart" "-")
triple1
Dave is not furry.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "furry" "-")
((triple1) -> (rule3 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is not blue.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "blue" "-")
((triple1) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("Dave" "is" "rough" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("Dave" "is" "rough" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is green.
True
7
proof
[(((((triple1) -> rule4) ((((triple1) -> rule4) triple1) -> rule8)) -> rule5))]
("Dave" "is" "green" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3)) triple1) -> (rule8 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not green.
False
7
inv-proof
[(((((triple1) -> rule4) ((((triple1) -> rule4) triple1) -> rule8)) -> rule5))]
("Dave" "is" "green" "-")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3)) triple1) -> (rule8 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Harry is not round.
Unknown
inv-rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Harry" "is" "round" "-")
Harry is blue.
Unknown
rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Harry" "is" "blue" "+")
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is green.
Unknown
rconc
[@3: Harry is green.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule1 <- FAIL)]]
("Harry" "is" "green" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Dave is smart.[(triple1)] Harry is rough.[(triple2)] @1: Dave is blue.[(((triple1) -> rule4))] Dave is not furry.[(((triple1) -> rule3))] @2: Dave is rough.[(((((triple1) -> rule4)) -> rule2))] Dave is round.[(((((triple1) -> rule4) triple1) -> rule8))] @3: Dave is green.[(((((triple1) -> rule4) ((((triple1) -> rule4) triple1) -> rule8)) -> rule5))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Harry is rough.
("Harry" "is" "rough" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
((triple1) -> (rule3 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3)) triple1) -> (rule8 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3