Bob is blue. Bob is cold. Bob is furry. Bob is nice. Bob is quiet. Bob is smart. Bob is white. Harry is blue. Harry is cold. Harry is furry. Harry is nice. Harry is quiet. Harry is smart. Harry is white. If Bob is smart and Bob is blue then Bob is white.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If Bob is smart and Bob is blue then Bob is white.
((("Bob" "is" "smart" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "white" "+"))
Harry is nice.
True
1
proof
[(triple11)]
("Harry" "is" "nice" "+")
triple11
Bob is not smart.
False
1
inv-proof
[(triple6)]
("Bob" "is" "smart" "-")
triple6
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is furry.[(triple3)] Bob is nice.[(triple4)] Bob is quiet.[(triple5)] Bob is smart.[(triple6)] Bob is white.[(triple7 OR ((triple6 triple1) -> rule1))] Harry is blue.[(triple8)] Harry is cold.[(triple9)] Harry is furry.[(triple10)] Harry is nice.[(triple11)] Harry is quiet.[(triple12)] Harry is smart.[(triple13)] Harry is white.[(triple14)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple6 triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Harry is smart.
("Harry" "is" "smart" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple14