Anne is big. Anne is blue. Anne is cold. Anne is green. Anne is kind. Anne is nice. Anne is rough. Harry is big. Harry is cold. Harry is green. Harry is nice. Harry is rough. If someone is kind then they are blue. Rough, cold people are kind. If someone is big and kind then they are nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is kind then they are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Rough, cold people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is big and kind then they are nice.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Anne is kind.
True
1
proof
[(triple5 OR ((triple7 triple3) -> rule2))]
("Anne" "is" "kind" "+")
triple5
((triple7 triple3) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Harry is not rough.
False
1
inv-proof
[(triple12)]
("Harry" "is" "rough" "-")
triple12
Harry is kind.
True
3
proof
[(((triple12 triple9) -> rule2))]
("Harry" "is" "kind" "+")
((triple12 triple9) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
3
inv-proof
[(((triple12 triple9) -> rule2))]
("Harry" "is" "kind" "-")
((triple12 triple9) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
True
4
proof
[(((((triple12 triple9) -> rule2)) -> rule1))]
("Harry" "is" "blue" "+")
((((triple12 triple9) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not blue.
False
4
inv-proof
[(((((triple12 triple9) -> rule2)) -> rule1))]
("Harry" "is" "blue" "-")
((((triple12 triple9) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple5) -> rule1) OR ((((triple7 triple3) -> rule2)) -> rule1))] Anne is cold.[(triple3)] Anne is green.[(triple4)] Anne is kind.[(triple5 OR ((triple7 triple3) -> rule2))] Anne is nice.[(triple6 OR ((triple1 triple5) -> rule3) OR ((triple1 ((triple7 triple3) -> rule2)) -> rule3))] Anne is rough.[(triple7)] Harry is big.[(triple8)] Harry is cold.[(triple9)] Harry is green.[(triple10)] Harry is nice.[(triple11 OR ((triple8 ((triple12 triple9) -> rule2)) -> rule3))] Harry is rough.[(triple12)] @1: Harry is kind.[(((triple12 triple9) -> rule2))] @2: Harry is blue.[(((((triple12 triple9) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple5) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple7 triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
Anne is green.
("Anne" "is" "green" "+")
triple4
Anne is kind.
("Anne" "is" "kind" "+")
triple5
((triple7 triple3) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple6
((triple1 triple5) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((triple1 ((triple7 triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple11
((triple8 ((triple12 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
((triple12 triple9) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple12 triple9) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2