Bob is furry. Bob is kind. Bob is smart. Bob is white. Charlie is big. Charlie is furry. Charlie is kind. Charlie is red. Charlie is rough. Charlie is smart. Charlie is white. Harry is red. Red, white things are rough. Smart, big things are furry. If something is big and rough then it is smart.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is red.
("Harry" "is" "red" "+")
Red, white things are rough.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
Smart, big things are furry.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is big and rough then it is smart.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Bob is kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "+")
triple2
Bob is not white.
False
1
inv-proof
[(triple4)]
("Bob" "is" "white" "-")
triple4
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Bob is furry.[(triple1)] Bob is kind.[(triple2)] Bob is smart.[(triple3)] Bob is white.[(triple4)] Charlie is big.[(triple5)] Charlie is furry.[(triple6 OR ((triple10 triple5) -> rule2) OR ((((triple5 triple9) -> rule3) triple5) -> rule2) OR ((((triple5 ((triple8 triple11) -> rule1)) -> rule3) triple5) -> rule2))] Charlie is kind.[(triple7)] Charlie is red.[(triple8)] Charlie is rough.[(triple9 OR ((triple8 triple11) -> rule1))] Charlie is smart.[(triple10 OR ((triple5 triple9) -> rule3) OR ((triple5 ((triple8 triple11) -> rule1)) -> rule3))] Charlie is white.[(triple11)] Harry is red.[(triple12)]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
((triple10 triple5) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple5 triple9) -> (rule3 % int2)) triple5) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((((triple5 ((triple8 triple11) -> (rule1 % int3))) -> (rule3 % int2)) triple5) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
triple8
Charlie is rough.
("Charlie" "is" "rough" "+")
triple9
((triple8 triple11) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple10
((triple5 triple9) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple5 ((triple8 triple11) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12