Bob is big. Bob is kind. Bob is not nice. Bob is red. Bob is rough. Bob is round. Bob is white. Rough, kind things are round. If something is white and not red then it is not round. If Bob is nice and Bob is kind then Bob is big.
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Rough, kind things are round.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something is white and not red then it is not round.
((("something" "is" "white" "+") ("something" "is" "red" "~")) -> ("something" "is" "round" "-"))
If Bob is nice and Bob is kind then Bob is big.
((("Bob" "is" "nice" "+") ("Bob" "is" "kind" "+")) -> ("Bob" "is" "big" "+"))
Bob is kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "+")
triple2
Bob is not kind.
False
1
inv-proof
[(triple2)]
("Bob" "is" "kind" "-")
triple2
@0: Bob is big.[(triple1)] Bob is kind.[(triple2)] Bob is not nice.[(triple3)] Bob is red.[(triple4)] Bob is rough.[(triple5)] Bob is round.[(triple6 OR ((triple5 triple2) -> rule1))] Bob is white.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is not nice.
("Bob" "is" "nice" "-")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple5 triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple7