Dave is not blue. Dave is not furry. Dave is nice. Dave is rough. Harry is big. Harry is furry. Harry is quiet. All big, blue things are nice. If something is nice and quiet then it is big. If Harry is rough and Harry is blue then Harry is quiet. Rough, big things are quiet. All rough, blue things are not quiet. If Dave is smart then Dave is nice. If Dave is not furry then Dave is big. If Dave is furry then Dave is smart.
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All big, blue things are nice.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is nice and quiet then it is big.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If Harry is rough and Harry is blue then Harry is quiet.
((("Harry" "is" "rough" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "quiet" "+"))
Rough, big things are quiet.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All rough, blue things are not quiet.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "-"))
If Dave is smart then Dave is nice.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "nice" "+"))
If Dave is not furry then Dave is big.
((("Dave" "is" "furry" "~")) -> ("Dave" "is" "big" "+"))
If Dave is furry then Dave is smart.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "smart" "+"))
Dave is nice.
True
1
proof
[(triple3)]
("Dave" "is" "nice" "+")
triple3
Harry is not quiet.
False
1
inv-proof
[(triple7)]
("Harry" "is" "quiet" "-")
triple7
Dave is big.
True
2
proof
[(((triple2) -> rule7))]
("Dave" "is" "big" "+")
((triple2) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple2) -> rule7))]
("Dave" "is" "big" "-")
((triple2) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
True
4
proof
[(((triple4 ((triple2) -> rule7)) -> rule4))]
("Dave" "is" "quiet" "+")
((triple4 ((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not quiet.
False
4
inv-proof
[(((triple4 ((triple2) -> rule7)) -> rule4))]
("Dave" "is" "quiet" "-")
((triple4 ((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "nice" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "smart" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Dave is nice.[(triple3)] Dave is not blue.[(triple1)] Dave is not furry.[(triple2)] Dave is rough.[(triple4)] Harry is big.[(triple5)] Harry is furry.[(triple6)] Harry is quiet.[(triple7)] @1: Dave is big.[(((triple2) -> rule7))] @2: Dave is quiet.[(((triple4 ((triple2) -> rule7)) -> rule4))]
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is not blue.
("Dave" "is" "blue" "-")
triple1
Dave is not furry.
("Dave" "is" "furry" "-")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Harry is big.
("Harry" "is" "big" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple4 ((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2