Bob is big. Bob is blue. Bob is cold. Bob is green. Bob is kind. Bob is quiet. Bob is white. If something is cold then it is big. All quiet things are cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Bob is green.
True
1
proof
[(triple4)]
("Bob" "is" "green" "+")
triple4
Bob is not big.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule1) OR ((((triple6) -> rule2)) -> rule1))]
("Bob" "is" "big" "-")
triple1
((triple3) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
@0: Bob is big.[(triple1 OR ((triple3) -> rule1) OR ((((triple6) -> rule2)) -> rule1))] Bob is blue.[(triple2)] Bob is cold.[(triple3 OR ((triple6) -> rule2))] Bob is green.[(triple4)] Bob is kind.[(triple5)] Bob is quiet.[(triple6)] Bob is white.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
((triple6) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7