Bob is big. Bob is furry. Bob is green. Bob is quiet. Bob is red. Bob is smart. Bob is white. All quiet people are big. All furry people are big. If someone is big and quiet then they are red.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
All quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
All furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If someone is big and quiet then they are red.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
Bob is red.
True
1
proof
[(triple5 OR ((triple1 triple4) -> rule3) OR ((((triple2) -> rule2) triple4) -> rule3) OR ((((triple4) -> rule1) triple4) -> rule3))]
("Bob" "is" "red" "+")
triple5
((triple1 triple4) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple2) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple4) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not white.
False
1
inv-proof
[(triple7)]
("Bob" "is" "white" "-")
triple7
@0: Bob is big.[(triple1 OR ((triple2) -> rule2) OR ((triple4) -> rule1))] Bob is furry.[(triple2)] Bob is green.[(triple3)] Bob is quiet.[(triple4)] Bob is red.[(triple5 OR ((triple1 triple4) -> rule3) OR ((((triple2) -> rule2) triple4) -> rule3) OR ((((triple4) -> rule1) triple4) -> rule3))] Bob is smart.[(triple6)] Bob is white.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple4) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple1 triple4) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple2) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple4) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7