Bob is blue. Bob is rough. Bob is round. If Bob is blue and Bob is round then Bob is red. All blue things are big. If something is rough then it is big. If Bob is blue then Bob is kind. All kind things are furry. Round, kind things are big.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
If Bob is blue and Bob is round then Bob is red.
((("Bob" "is" "blue" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "red" "+"))
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If Bob is blue then Bob is kind.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "kind" "+"))
All kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Round, kind things are big.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not rough.
False
1
inv-proof
[(triple2)]
("Bob" "is" "rough" "-")
triple2
@0: Bob is blue.[(triple1)] Bob is rough.[(triple2)] Bob is round.[(triple3)] @1: Bob is big.[(((triple1) -> rule2) OR ((triple2) -> rule3) OR ((triple3 ((triple1) -> rule4)) -> rule6))] Bob is kind.[(((triple1) -> rule4))] Bob is red.[(((triple1 triple3) -> rule1))] @2: Bob is furry.[(((((triple1) -> rule4)) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple3 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple1 triple3) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2