Bob is furry. Bob is green. Bob is kind. Bob is nice. Bob is quiet. Bob is red. Bob is young. Gary is furry. Gary is nice. Gary is quiet. Gary is red. Harry is green. Harry is nice. Harry is quiet. Harry is red. Harry is young. If something is red and nice then it is young. Young, furry things are kind. If Harry is young and Harry is nice then Harry is kind. All furry, kind things are young. If Bob is young and Bob is kind then Bob is red. If Harry is furry and Harry is green then Harry is young. If something is furry then it is green. All kind things are quiet.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is red and nice then it is young.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Young, furry things are kind.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If Harry is young and Harry is nice then Harry is kind.
((("Harry" "is" "young" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "kind" "+"))
All furry, kind things are young.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If Bob is young and Bob is kind then Bob is red.
((("Bob" "is" "young" "+") ("Bob" "is" "kind" "+")) -> ("Bob" "is" "red" "+"))
If Harry is furry and Harry is green then Harry is young.
((("Harry" "is" "furry" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "young" "+"))
If something is furry then it is green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
Bob is nice.
True
1
proof
[(triple4)]
("Bob" "is" "nice" "+")
triple4
Harry is not nice.
False
1
inv-proof
[(triple13)]
("Harry" "is" "nice" "-")
triple13
Gary is green.
True
2
proof
[(((triple8) -> rule7))]
("Gary" "is" "green" "+")
((triple8) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple8) -> rule7))]
("Gary" "is" "green" "-")
((triple8) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
True
5
proof
[(((((triple11 triple9) -> rule1) triple8) -> rule2))]
("Gary" "is" "kind" "+")
((((triple11 triple9) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not kind.
False
5
inv-proof
[(((((triple11 triple9) -> rule1) triple8) -> rule2))]
("Gary" "is" "kind" "-")
((((triple11 triple9) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
@0: Bob is furry.[(triple1)] Bob is green.[(triple2 OR ((triple1) -> rule7))] Bob is kind.[(triple3 OR ((triple7 triple1) -> rule2) OR ((((triple6 triple4) -> rule1) triple1) -> rule2))] Bob is nice.[(triple4)] Bob is quiet.[(triple5 OR ((triple3) -> rule8) OR ((((triple7 triple1) -> rule2)) -> rule8) OR ((((((triple6 triple4) -> rule1) triple1) -> rule2)) -> rule8))] Bob is red.[(triple6 OR ((triple7 triple3) -> rule5) OR ((triple7 ((triple7 triple1) -> rule2)) -> rule5) OR ((((triple1 triple3) -> rule4) triple3) -> rule5) OR ((((triple1 triple3) -> rule4) ((triple7 triple1) -> rule2)) -> rule5))] Bob is young.[(triple7 OR ((triple1 triple3) -> rule4) OR ((triple6 triple4) -> rule1))] Gary is furry.[(triple8)] Gary is nice.[(triple9)] Gary is quiet.[(triple10 OR ((((((triple11 triple9) -> rule1) triple8) -> rule2)) -> rule8))] Gary is red.[(triple11)] Harry is green.[(triple12)] Harry is nice.[(triple13)] Harry is quiet.[(triple14 OR ((((triple16 triple13) -> rule3)) -> rule8) OR ((((((triple15 triple13) -> rule1) triple13) -> rule3)) -> rule8))] Harry is red.[(triple15)] Harry is young.[(triple16 OR ((triple15 triple13) -> rule1))] @1: Gary is green.[(((triple8) -> rule7))] Gary is young.[(((triple11 triple9) -> rule1))] Harry is kind.[(((triple16 triple13) -> rule3) OR ((((triple15 triple13) -> rule1) triple13) -> rule3))] @2: Gary is kind.[(((((triple11 triple9) -> rule1) triple8) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple1) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple7 triple1) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple6 triple4) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple3) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple7 triple1) -> (rule2 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((((triple6 triple4) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
triple6
((triple7 triple3) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple7 ((triple7 triple1) -> (rule2 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple1 triple3) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple1 triple3) -> (rule4 % int3)) ((triple7 triple1) -> (rule2 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple1 triple3) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple6 triple4) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
((((((triple11 triple9) -> (rule1 % int3)) triple8) -> (rule2 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
((((triple16 triple13) -> (rule3 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((((triple15 triple13) -> (rule1 % int3)) triple13) -> (rule3 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple15 triple13) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple8) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple11 triple9) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple16 triple13) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple15 triple13) -> (rule1 % int2)) triple13) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple11 triple9) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2