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