Bob is big. Bob is blue. Bob is cold. Bob is kind. Bob is rough. Bob is not smart. Bob is young. Blue, cold things are young. If something is cold then it is kind.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is young.
("Bob" "is" "young" "+")
Blue, cold things are young.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Bob is young.
True
1
proof
[(triple7 OR ((triple2 triple3) -> rule1))]
("Bob" "is" "young" "+")
triple7
((triple2 triple3) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
False
1
inv-proof
[(triple6)]
("Bob" "is" "smart" "+")
triple6
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is cold.[(triple3)] Bob is kind.[(triple4 OR ((triple3) -> rule2))] Bob is not smart.[(triple6)] Bob is rough.[(triple5)] Bob is young.[(triple7 OR ((triple2 triple3) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple3) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not smart.
("Bob" "is" "smart" "-")
triple6
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple2 triple3) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1