Bob is cold. Bob is not kind. Bob is quiet. Bob is not red. Bob is rough. Bob is not smart. Bob is white. If someone is red then they are smart. Red, white people are smart. If someone is smart then they are red. Kind people are not cold. If someone is smart and not white then they are not rough. If Bob is not red then Bob is rough. If someone is rough then they are quiet. All kind people are not quiet.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is white.
("Bob" "is" "white" "+")
If someone is red then they are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Red, white people are smart.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart then they are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Kind people are not cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "-"))
If someone is smart and not white then they are not rough.
((("someone" "is" "smart" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "rough" "-"))
If Bob is not red then Bob is rough.
((("Bob" "is" "red" "~")) -> ("Bob" "is" "rough" "+"))
If someone is rough then they are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
All kind people are not quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "-"))
Bob is rough.
True
1
proof
[(triple5 OR ((triple4) -> rule6))]
("Bob" "is" "rough" "+")
triple5
((triple4) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
False
1
inv-proof
[(triple6)]
("Bob" "is" "smart" "+")
triple6
@0: Bob is cold.[(triple1)] Bob is not kind.[(triple2)] Bob is not red.[(triple4)] Bob is not smart.[(triple6)] Bob is quiet.[(triple3 OR ((triple5) -> rule7) OR ((((triple4) -> rule6)) -> rule7))] Bob is rough.[(triple5 OR ((triple4) -> rule6))] Bob is white.[(triple7)]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is not kind.
("Bob" "is" "kind" "-")
triple2
Bob is not red.
("Bob" "is" "red" "-")
triple4
Bob is not smart.
("Bob" "is" "smart" "-")
triple6
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple5) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple4) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple7