Bob is blue. Bob is green. Bob is kind. Bob is nice. Bob is not round. Bob is not smart. Bob is young. Green, round things are smart. Young things are not smart. If Bob is smart then Bob is kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not round.
("Bob" "is" "round" "-")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is young.
("Bob" "is" "young" "+")
Green, round things are smart.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Young things are not smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "-"))
If Bob is smart then Bob is kind.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "kind" "+"))
Bob is green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "+")
triple2
Bob is not young.
False
1
inv-proof
[(triple7)]
("Bob" "is" "young" "-")
triple7
@0: Bob is blue.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3)] Bob is nice.[(triple4)] Bob is not round.[(triple5)] Bob is not smart.[(triple6 OR ((triple7) -> rule2))] Bob is young.[(triple7)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is not round.
("Bob" "is" "round" "-")
triple5
Bob is not smart.
("Bob" "is" "smart" "-")
triple6
((triple7) -> (rule2 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
triple7