Bob is big. Bob is blue. Bob is quiet. Bob is red. Dave is furry. Dave is nice. Dave is quiet. Dave is smart. Gary is not big. Gary is not blue. Gary is not furry. Gary is red. Gary is smart. Harry is blue. Harry is nice. Harry is red. If Dave is big then Dave is not smart. If someone is big then they are furry. If Harry is blue and Harry is not nice then Harry is furry. All big people are quiet. If Gary is smart then Gary is red. If someone is red and blue then they are smart.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
If Dave is big then Dave is not smart.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "smart" "-"))
If someone is big then they are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
If Harry is blue and Harry is not nice then Harry is furry.
((("Harry" "is" "blue" "+") ("Harry" "is" "nice" "~")) -> ("Harry" "is" "furry" "+"))
All big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is smart then Gary is red.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "red" "+"))
If someone is red and blue then they are smart.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Dave is not furry.
False
1
inv-proof
[(triple5)]
("Dave" "is" "furry" "-")
triple5
Bob is furry.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Harry is not smart.
False
3
inv-proof
[(((triple16 triple14) -> rule6))]
("Harry" "is" "smart" "-")
((triple16 triple14) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "furry" "-")
Gary is quiet.
Unknown
rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "quiet" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is quiet.[(triple3 OR ((triple1) -> rule4))] Bob is red.[(triple4)] Dave is furry.[(triple5)] Dave is nice.[(triple6)] Dave is quiet.[(triple7)] Dave is smart.[(triple8)] Gary is not big.[(triple9)] Gary is not blue.[(triple10)] Gary is not furry.[(triple11)] Gary is red.[(triple12 OR ((triple13) -> rule5))] Gary is smart.[(triple13)] Harry is blue.[(triple14)] Harry is nice.[(triple15)] Harry is red.[(triple16)] @1: Bob is furry.[(((triple1) -> rule2))] Bob is smart.[(((triple4 triple2) -> rule6))] Harry is smart.[(((triple16 triple14) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple1) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
triple8
Gary is not big.
("Gary" "is" "big" "-")
triple9
Gary is not blue.
("Gary" "is" "blue" "-")
triple10
Gary is not furry.
("Gary" "is" "furry" "-")
triple11
Gary is red.
("Gary" "is" "red" "+")
triple12
((triple13) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple13
Harry is blue.
("Harry" "is" "blue" "+")
triple14
Harry is nice.
("Harry" "is" "nice" "+")
triple15
Harry is red.
("Harry" "is" "red" "+")
triple16
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple4 triple2) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple16 triple14) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1