Bob is big. Bob is blue. Bob is cold. Bob is furry. Bob is smart. Bob is white. Bob is young. Furry, blue people are big. If Bob is cold then Bob is blue.
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 smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Furry, blue people are big.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If Bob is cold then Bob is blue.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "blue" "+"))
Bob is white.
True
1
proof
[(triple6)]
("Bob" "is" "white" "+")
triple6
Bob is not blue.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule2))]
("Bob" "is" "blue" "-")
triple2
((triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
@0: Bob is big.[(triple1 OR ((triple4 triple2) -> rule1) OR ((triple4 ((triple3) -> rule2)) -> rule1))] Bob is blue.[(triple2 OR ((triple3) -> rule2))] Bob is cold.[(triple3)] Bob is furry.[(triple4)] Bob is smart.[(triple5)] Bob is white.[(triple6)] Bob is young.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple4 triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple4 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7