Dave is blue. Dave is cold. Dave is furry. Dave is green. Dave is not nice. Dave is round. Dave is smart. Erin is not blue. Erin is cold. Erin is furry. Erin is not green. Erin is smart. Harry is furry. Harry is green. Harry is round. Blue, cold things are green. If something is furry and not nice then it is blue. If Harry is cold and Harry is furry then Harry is green. If Dave is not blue then Dave is smart. If something is furry and not green then it is smart. Cold things are smart. Round things are smart. If something is round and nice then it is not smart.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not green.
("Erin" "is" "green" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is round.
("Harry" "is" "round" "+")
Blue, cold things are green.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is furry and not nice then it is blue.
((("something" "is" "furry" "+") ("something" "is" "nice" "~")) -> ("something" "is" "blue" "+"))
If Harry is cold and Harry is furry then Harry is green.
((("Harry" "is" "cold" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "green" "+"))
If Dave is not blue then Dave is smart.
((("Dave" "is" "blue" "~")) -> ("Dave" "is" "smart" "+"))
If something is furry and not green then it is smart.
((("something" "is" "furry" "+") ("something" "is" "green" "~")) -> ("something" "is" "smart" "+"))
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If something is round and nice then it is not smart.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "-"))
Dave is smart.
True
1
proof
[(triple7 OR ((triple2) -> rule6) OR ((triple6) -> rule7))]
("Dave" "is" "smart" "+")
triple7
((triple2) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple6) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Harry is not furry.
False
1
inv-proof
[(triple13)]
("Harry" "is" "furry" "-")
triple13
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "blue" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Dave is blue.[(triple1 OR ((triple3 triple5) -> rule2))] Dave is cold.[(triple2)] Dave is furry.[(triple3)] Dave is green.[(triple4 OR ((triple1 triple2) -> rule1) OR ((((triple3 triple5) -> rule2) triple2) -> rule1))] Dave is not nice.[(triple5)] Dave is round.[(triple6)] Dave is smart.[(triple7 OR ((triple2) -> rule6) OR ((triple6) -> rule7))] Erin is cold.[(triple9)] Erin is furry.[(triple10)] Erin is not blue.[(triple8)] Erin is not green.[(triple11)] Erin is smart.[(triple12 OR ((triple9) -> rule6) OR ((triple10 triple11) -> rule5))] Harry is furry.[(triple13)] Harry is green.[(triple14)] Harry is round.[(triple15)] @1: Harry is smart.[(((triple15) -> rule7))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple3 triple5) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
((triple1 triple2) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple3 triple5) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
((triple2) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple6) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple9
Erin is furry.
("Erin" "is" "furry" "+")
triple10
Erin is not blue.
("Erin" "is" "blue" "-")
triple8
Erin is not green.
("Erin" "is" "green" "-")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
((triple9) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple10 triple11) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is green.
("Harry" "is" "green" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
((triple15) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1