Dave is furry. Dave is red. Dave is young. Harry is blue. Harry is green. Harry is round. Harry is smart. Blue things are smart. Red things are green. If something is blue and red then it is round. All smart things are green. All red, round things are furry. If something is furry then it is red. If something is blue and smart then it is green. If Dave is red then Dave is green.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is blue and red then it is round.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All red, round things are furry.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is blue and smart then it is green.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If Dave is red then Dave is green.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "green" "+"))
Dave is furry.
True
1
proof
[(triple1)]
("Dave" "is" "furry" "+")
triple1
Dave is not red.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule6))]
("Dave" "is" "red" "-")
triple2
((triple1) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Dave is furry.[(triple1)] Dave is red.[(triple2 OR ((triple1) -> rule6))] Dave is young.[(triple3)] Harry is blue.[(triple4)] Harry is green.[(triple5 OR ((triple7) -> rule4) OR ((triple4 triple7) -> rule7) OR ((((triple4) -> rule1)) -> rule4) OR ((triple4 ((triple4) -> rule1)) -> rule7))] Harry is round.[(triple6)] Harry is smart.[(triple7 OR ((triple4) -> rule1))] @1: Dave is green.[(((triple2) -> rule2) OR ((triple2) -> rule8) OR ((((triple1) -> rule6)) -> rule2) OR ((((triple1) -> rule6)) -> rule8))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
((triple1) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Harry is green.
("Harry" "is" "green" "+")
triple5
((triple7) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple4 triple7) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple4 ((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
((triple4) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple2) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2