Bob is big. Bob is cold. Bob is furry. Bob is kind. Bob is quiet. Bob is rough. Bob is young. Gary is big. Gary is cold. Gary is furry. Gary is kind. Gary is quiet. Gary is rough. Gary is young. Cold people are rough. If someone is cold then they are kind.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
Cold people are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold then they are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Gary is not cold.
False
1
inv-proof
[(triple9)]
("Gary" "is" "cold" "-")
triple9
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is furry.[(triple3)] Bob is kind.[(triple4 OR ((triple2) -> rule2))] Bob is quiet.[(triple5)] Bob is rough.[(triple6 OR ((triple2) -> rule1))] Bob is young.[(triple7)] Gary is big.[(triple8)] Gary is cold.[(triple9)] Gary is furry.[(triple10)] Gary is kind.[(triple11 OR ((triple9) -> rule2))] Gary is quiet.[(triple12)] Gary is rough.[(triple13 OR ((triple9) -> rule1))] Gary is young.[(triple14)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple2) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is rough.
("Bob" "is" "rough" "+")
triple6
((triple2) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is furry.
("Gary" "is" "furry" "+")
triple10
Gary is kind.
("Gary" "is" "kind" "+")
triple11
((triple9) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
Gary is rough.
("Gary" "is" "rough" "+")
triple13
((triple9) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple14