Dave is furry. Dave is nice. Dave is round. Harry is blue. Harry is cold. Harry is furry. Harry is green. Harry is nice. Harry is rough. Harry is round. Blue, furry things are rough. All furry things are nice. If something is cold then it is rough. Cold things are round. If something is nice and rough then it is furry. Round, nice things are green.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Blue, furry things are rough.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
All furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is cold then it is rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is nice and rough then it is furry.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
Round, nice things are green.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Harry is furry.
True
1
proof
[(triple6 OR ((triple8 triple9) -> rule5) OR ((triple8 ((triple5) -> rule3)) -> rule5))]
("Harry" "is" "furry" "+")
triple6
((triple8 triple9) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple8 ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Dave is not furry.
False
1
inv-proof
[(triple1)]
("Dave" "is" "furry" "-")
triple1
Dave is green.
True
3
proof
[(((triple3 triple2) -> rule6) OR ((triple3 ((triple1) -> rule2)) -> rule6))]
("Dave" "is" "green" "+")
((triple3 triple2) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple3 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not green.
False
3
inv-proof
[(((triple3 triple2) -> rule6) OR ((triple3 ((triple1) -> rule2)) -> rule6))]
("Dave" "is" "green" "-")
((triple3 triple2) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple3 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "-")
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 nice.[(triple2 OR ((triple1) -> rule2))] Dave is round.[(triple3)] Harry is blue.[(triple4)] Harry is cold.[(triple5)] Harry is furry.[(triple6 OR ((triple8 triple9) -> rule5) OR ((triple8 ((triple5) -> rule3)) -> rule5))] Harry is green.[(triple7 OR ((triple10 triple8) -> rule6) OR ((triple10 ((triple6) -> rule2)) -> rule6) OR ((((triple5) -> rule4) triple8) -> rule6) OR ((((triple5) -> rule4) ((triple6) -> rule2)) -> rule6))] Harry is nice.[(triple8 OR ((triple6) -> rule2))] Harry is rough.[(triple9 OR ((triple5) -> rule3) OR ((triple4 triple6) -> rule1))] Harry is round.[(triple10 OR ((triple5) -> rule4))] @1: Dave is green.[(((triple3 triple2) -> rule6) OR ((triple3 ((triple1) -> rule2)) -> rule6))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
((triple1) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
((triple8 triple9) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple8 ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple7
((triple10 triple8) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple10 ((triple6) -> (rule2 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple5) -> (rule4 % int2)) triple8) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((triple5) -> (rule4 % int3)) ((triple6) -> (rule2 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple6) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple9
((triple5) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple4 triple6) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple10
((triple5) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple3 triple2) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple3 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2