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