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