Anne is furry. Anne is kind. Anne is red. Anne is rough. Bob is furry. Bob is green. Bob is kind. Bob is nice. Bob is red. Bob is rough. Bob is young. Harry is furry. Harry is green. Harry is kind. Harry is nice. Harry is young. If someone is nice and furry then they are red. If someone is furry and nice then they are young. If someone is nice then they are kind. If someone is red then they are green. Green people are nice. If Harry is not kind then Harry is young.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
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 red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is nice and furry then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If someone is furry and nice then they are young.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone is nice then they are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is red then they are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If Harry is not kind then Harry is young.
((("Harry" "is" "kind" "~")) -> ("Harry" "is" "young" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Bob is not kind.
False
1
inv-proof
[(triple7 OR ((triple8) -> rule3) OR ((((triple6) -> rule5)) -> rule3) OR ((((((triple9) -> rule4)) -> rule5)) -> rule3))]
("Bob" "is" "kind" "-")
triple7
((triple8) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Anne is green.
True
2
proof
[(((triple3) -> rule4))]
("Anne" "is" "green" "+")
((triple3) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Harry is not red.
False
3
inv-proof
[(((triple15 triple12) -> rule1) OR ((((triple13) -> rule5) triple12) -> rule1))]
("Harry" "is" "red" "-")
((triple15 triple12) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple13) -> (rule5 % int2)) triple12) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Anne is nice.
True
3
proof
[(((((triple3) -> rule4)) -> rule5))]
("Anne" "is" "nice" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not nice.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule5))]
("Anne" "is" "nice" "-")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
True
5
proof
[(((triple1 ((((triple3) -> rule4)) -> rule5)) -> rule2))]
("Anne" "is" "young" "+")
((triple1 ((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not young.
False
5
inv-proof
[(((triple1 ((((triple3) -> rule4)) -> rule5)) -> rule2))]
("Anne" "is" "young" "-")
((triple1 ((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2 OR ((((((triple3) -> rule4)) -> rule5)) -> rule3))] Anne is red.[(triple3)] Anne is rough.[(triple4)] Bob is furry.[(triple5)] Bob is green.[(triple6 OR ((triple9) -> rule4) OR ((((triple8 triple5) -> rule1)) -> rule4))] Bob is kind.[(triple7 OR ((triple8) -> rule3) OR ((((triple6) -> rule5)) -> rule3) OR ((((((triple9) -> rule4)) -> rule5)) -> rule3))] Bob is nice.[(triple8 OR ((triple6) -> rule5) OR ((((triple9) -> rule4)) -> rule5))] Bob is red.[(triple9 OR ((triple8 triple5) -> rule1) OR ((((triple6) -> rule5) triple5) -> rule1))] Bob is rough.[(triple10)] Bob is young.[(triple11 OR ((triple5 triple8) -> rule2) OR ((triple5 ((triple6) -> rule5)) -> rule2) OR ((triple5 ((((triple9) -> rule4)) -> rule5)) -> rule2))] Harry is furry.[(triple12)] Harry is green.[(triple13 OR ((((triple15 triple12) -> rule1)) -> rule4))] Harry is kind.[(triple14 OR ((triple15) -> rule3) OR ((((triple13) -> rule5)) -> rule3))] Harry is nice.[(triple15 OR ((triple13) -> rule5))] Harry is young.[(triple16 OR ((triple12 triple15) -> rule2) OR ((triple12 ((triple13) -> rule5)) -> rule2))] @1: Anne is green.[(((triple3) -> rule4))] Harry is red.[(((triple15 triple12) -> rule1) OR ((((triple13) -> rule5) triple12) -> rule1))] @2: Anne is nice.[(((((triple3) -> rule4)) -> rule5))] @3: Anne is young.[(((triple1 ((((triple3) -> rule4)) -> rule5)) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Bob is furry.
("Bob" "is" "furry" "+")
triple5
Bob is green.
("Bob" "is" "green" "+")
triple6
((triple9) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple8 triple5) -> (rule1 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple7
((triple8) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
triple8
((triple6) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple9
((triple8 triple5) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple6) -> (rule5 % int2)) triple5) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple10
Bob is young.
("Bob" "is" "young" "+")
triple11
((triple5 triple8) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple5 ((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((triple5 ((((triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
triple13
((((triple15 triple12) -> (rule1 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple14
((triple15) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple13) -> (rule5 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple15
((triple13) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple12 triple15) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple12 ((triple13) -> (rule5 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((triple3) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple15 triple12) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple13) -> (rule5 % int2)) triple12) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((triple1 ((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3