Bob is blue. Bob is nice. Bob is smart. Harry is big. Harry is blue. Harry is cold. Harry is furry. If something is nice then it is smart. Nice things are smart.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Bob is smart.
True
1
proof
[(triple3 OR ((triple2) -> rule1) OR ((triple2) -> rule2))]
("Bob" "is" "smart" "+")
triple3
((triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Harry is not blue.
False
1
inv-proof
[(triple5)]
("Harry" "is" "blue" "-")
triple5
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "smart" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is blue.[(triple1)] Bob is nice.[(triple2)] Bob is smart.[(triple3 OR ((triple2) -> rule1) OR ((triple2) -> rule2))] Harry is big.[(triple4)] Harry is blue.[(triple5)] Harry is cold.[(triple6)] Harry is furry.[(triple7)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
((triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7