Bob is big. Bob is blue. Bob is not cold. Bob is not nice. Bob is red. Bob is rough. Bob is white. If someone is blue then they are rough. Nice, rough people are not red. All nice people are red. If someone is nice then they are blue. If someone is cold and not red then they are big. Blue, nice people are not big. All red people are white. If someone is big then they are white.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
If someone is blue then they are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Nice, rough people are not red.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "-"))
All nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is nice then they are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold and not red then they are big.
((("someone" "is" "cold" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "big" "+"))
Blue, nice people are not big.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "-"))
All red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Bob is red.
True
1
proof
[(triple5)]
("Bob" "is" "red" "+")
triple5
Bob is not white.
False
1
inv-proof
[(triple7 OR ((triple1) -> rule8) OR ((triple5) -> rule7))]
("Bob" "is" "white" "-")
triple7
((triple1) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple5) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is not cold.[(triple3)] Bob is not nice.[(triple4)] Bob is red.[(triple5)] Bob is rough.[(triple6 OR ((triple2) -> rule1))] Bob is white.[(triple7 OR ((triple1) -> rule8) OR ((triple5) -> rule7))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is not cold.
("Bob" "is" "cold" "-")
triple3
Bob is not nice.
("Bob" "is" "nice" "-")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is rough.
("Bob" "is" "rough" "+")
triple6
((triple2) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple1) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple5) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1