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