Bob is big. Bob is furry. Bob is green. Bob is nice. Bob is rough. Harry is big. Harry is furry. Harry is green. Harry is nice. Harry is quiet. Harry is rough. Harry is round. If someone is quiet and big then they are rough. If Bob is green and Bob is nice then Bob is big. Round, furry people are quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is quiet and big then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If Bob is green and Bob is nice then Bob is big.
((("Bob" "is" "green" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "big" "+"))
Round, furry people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Bob is furry.
True
1
proof
[(triple2)]
("Bob" "is" "furry" "+")
triple2
Harry is not rough.
False
1
inv-proof
[(triple11 OR ((triple10 triple6) -> rule1) OR ((((triple12 triple7) -> rule3) triple6) -> rule1))]
("Harry" "is" "rough" "-")
triple11
((triple10 triple6) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple12 triple7) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is big.[(triple1 OR ((triple3 triple4) -> rule2))] Bob is furry.[(triple2)] Bob is green.[(triple3)] Bob is nice.[(triple4)] Bob is rough.[(triple5)] Harry is big.[(triple6)] Harry is furry.[(triple7)] Harry is green.[(triple8)] Harry is nice.[(triple9)] Harry is quiet.[(triple10 OR ((triple12 triple7) -> rule3))] Harry is rough.[(triple11 OR ((triple10 triple6) -> rule1) OR ((((triple12 triple7) -> rule3) triple6) -> rule1))] Harry is round.[(triple12)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3 triple4) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
((triple12 triple7) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple11
((triple10 triple6) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple12 triple7) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple12