Dave is blue. Dave is furry. Dave is green. Dave is kind. Dave is quiet. Dave is red. Dave is smart. Harry is blue. Harry is furry. Harry is green. Harry is quiet. Harry is smart. All smart people are furry. If someone is smart and red then they are furry. If Harry is green then Harry is red. Green, red people are furry. If Harry is furry and Harry is quiet then Harry is red. If someone is red then they are kind.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart and red then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If Harry is green then Harry is red.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "red" "+"))
Green, red people are furry.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If Harry is furry and Harry is quiet then Harry is red.
((("Harry" "is" "furry" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "red" "+"))
If someone is red then they are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Dave is smart.
True
1
proof
[(triple7)]
("Dave" "is" "smart" "+")
triple7
Harry is not quiet.
False
1
inv-proof
[(triple11)]
("Harry" "is" "quiet" "-")
triple11
Harry is red.
True
2
proof
[(((triple10) -> rule3) OR ((triple9 triple11) -> rule5) OR ((((triple12) -> rule1) triple11) -> rule5))]
("Harry" "is" "red" "+")
((triple10) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple9 triple11) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple12) -> (rule1 % int2)) triple11) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not red.
False
2
inv-proof
[(((triple10) -> rule3) OR ((triple9 triple11) -> rule5) OR ((((triple12) -> rule1) triple11) -> rule5))]
("Harry" "is" "red" "-")
((triple10) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple9 triple11) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple12) -> (rule1 % int2)) triple11) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
True
3
proof
[(((((triple10) -> rule3)) -> rule6) OR ((((triple9 triple11) -> rule5)) -> rule6) OR ((((((triple12) -> rule1) triple11) -> rule5)) -> rule6))]
("Harry" "is" "kind" "+")
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple9 triple11) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((((triple12) -> (rule1 % int3)) triple11) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is not kind.
False
3
inv-proof
[(((((triple10) -> rule3)) -> rule6) OR ((((triple9 triple11) -> rule5)) -> rule6) OR ((((((triple12) -> rule1) triple11) -> rule5)) -> rule6))]
("Harry" "is" "kind" "-")
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple9 triple11) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((((triple12) -> (rule1 % int3)) triple11) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
@0: Dave is blue.[(triple1)] Dave is furry.[(triple2 OR ((triple7) -> rule1) OR ((triple3 triple6) -> rule4) OR ((triple7 triple6) -> rule2))] Dave is green.[(triple3)] Dave is kind.[(triple4 OR ((triple6) -> rule6))] Dave is quiet.[(triple5)] Dave is red.[(triple6)] Dave is smart.[(triple7)] Harry is blue.[(triple8)] Harry is furry.[(triple9 OR ((triple12) -> rule1) OR ((triple10 ((triple10) -> rule3)) -> rule4) OR ((triple12 ((triple10) -> rule3)) -> rule2))] Harry is green.[(triple10)] Harry is quiet.[(triple11)] Harry is smart.[(triple12)] @1: Harry is red.[(((triple10) -> rule3) OR ((triple9 triple11) -> rule5) OR ((((triple12) -> rule1) triple11) -> rule5))] @2: Harry is kind.[(((((triple10) -> rule3)) -> rule6) OR ((((triple9 triple11) -> rule5)) -> rule6) OR ((((((triple12) -> rule1) triple11) -> rule5)) -> rule6))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple7) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple3 triple6) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple7 triple6) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
((triple6) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
((triple12) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple10 ((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((triple12 ((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
((triple10) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple9 triple11) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple12) -> (rule1 % int2)) triple11) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple9 triple11) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((((triple12) -> (rule1 % int3)) triple11) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3