Dave is big. Dave is not blue. Dave is kind. Dave is nice. Dave is quiet. Dave is white. Gary is big. Gary is furry. Gary is kind. Gary is nice. Gary is quiet. Gary is white. Harry is furry. Harry is kind. Harry is quiet. Harry is white. If something is furry and not kind then it is not big. All big, furry things are white. If something is quiet then it is furry. If Gary is big and Gary is white then Gary is blue. If Dave is nice and Dave is furry then Dave is quiet. All big, blue things are nice.
Dave is big.
("Dave" "is" "big" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is furry and not kind then it is not big.
((("something" "is" "furry" "+") ("something" "is" "kind" "~")) -> ("something" "is" "big" "-"))
All big, furry things are white.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If something is quiet then it is furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If Gary is big and Gary is white then Gary is blue.
((("Gary" "is" "big" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "blue" "+"))
If Dave is nice and Dave is furry then Dave is quiet.
((("Dave" "is" "nice" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "quiet" "+"))
All big, blue things are nice.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Harry is furry.
True
1
proof
[(triple13 OR ((triple15) -> rule3))]
("Harry" "is" "furry" "+")
triple13
((triple15) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Gary is not nice.
False
1
inv-proof
[(triple10 OR ((triple7 ((triple7 triple12) -> rule4)) -> rule6) OR ((triple7 ((triple7 ((triple7 triple8) -> rule2)) -> rule4)) -> rule6) OR ((triple7 ((triple7 ((triple7 ((triple11) -> rule3)) -> rule2)) -> rule4)) -> rule6))]
("Gary" "is" "nice" "-")
triple10
((triple7 ((triple7 triple12) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple7 ((triple7 ((triple7 triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((triple7 ((triple7 ((triple7 ((triple11) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Dave is furry.
True
2
proof
[(((triple5) -> rule3))]
("Dave" "is" "furry" "+")
((triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple5) -> rule3))]
("Dave" "is" "furry" "-")
((triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Dave is big.[(triple1)] Dave is kind.[(triple3)] Dave is nice.[(triple4)] Dave is not blue.[(triple2)] Dave is quiet.[(triple5)] Dave is white.[(triple6 OR ((triple1 ((triple5) -> rule3)) -> rule2))] Gary is big.[(triple7)] Gary is furry.[(triple8 OR ((triple11) -> rule3))] Gary is kind.[(triple9)] Gary is nice.[(triple10 OR ((triple7 ((triple7 triple12) -> rule4)) -> rule6) OR ((triple7 ((triple7 ((triple7 triple8) -> rule2)) -> rule4)) -> rule6) OR ((triple7 ((triple7 ((triple7 ((triple11) -> rule3)) -> rule2)) -> rule4)) -> rule6))] Gary is quiet.[(triple11)] Gary is white.[(triple12 OR ((triple7 triple8) -> rule2) OR ((triple7 ((triple11) -> rule3)) -> rule2))] Harry is furry.[(triple13 OR ((triple15) -> rule3))] Harry is kind.[(triple14)] Harry is quiet.[(triple15)] Harry is white.[(triple16)] @1: Dave is furry.[(((triple5) -> rule3))] Gary is blue.[(((triple7 triple12) -> rule4) OR ((triple7 ((triple7 triple8) -> rule2)) -> rule4) OR ((triple7 ((triple7 ((triple11) -> rule3)) -> rule2)) -> rule4))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is not blue.
("Dave" "is" "blue" "-")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple1 ((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
((triple11) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple10
((triple7 ((triple7 triple12) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple7 ((triple7 ((triple7 triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((triple7 ((triple7 ((triple7 ((triple11) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
((triple7 triple8) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple7 ((triple11) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple13
((triple15) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
Dave is furry.
("Dave" "is" "furry" "+")
((triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple7 triple12) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple7 ((triple7 triple8) -> (rule2 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((triple7 ((triple7 ((triple11) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3