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