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