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