Bob is not big. Bob is blue. Bob is furry. Bob is green. Bob is kind. Bob is red. Bob is white. Harry is big. Harry is blue. Harry is furry. Harry is green. Harry is kind. Harry is red. Harry is white. If Harry is green and Harry is white then Harry is big. All furry things are red.
Bob is not big.
("Bob" "is" "big" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
If Harry is green and Harry is white then Harry is big.
((("Harry" "is" "green" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "big" "+"))
All furry things are red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Harry is red.
True
1
proof
[(triple13 OR ((triple10) -> rule2))]
("Harry" "is" "red" "+")
triple13
((triple10) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Bob is big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
@0: Bob is blue.[(triple2)] Bob is furry.[(triple3)] Bob is green.[(triple4)] Bob is kind.[(triple5)] Bob is not big.[(triple1)] Bob is red.[(triple6 OR ((triple3) -> rule2))] Bob is white.[(triple7)] Harry is big.[(triple8 OR ((triple11 triple14) -> rule1))] Harry is blue.[(triple9)] Harry is furry.[(triple10)] Harry is green.[(triple11)] Harry is kind.[(triple12)] Harry is red.[(triple13 OR ((triple10) -> rule2))] Harry is white.[(triple14)]
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple6
((triple3) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple11 triple14) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is kind.
("Harry" "is" "kind" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
((triple10) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple14