Anne is cold. Anne is kind. Anne is quiet. Charlie is blue. Charlie is cold. Charlie is furry. Charlie is green. Charlie is kind. Charlie is smart. Harry is blue. Harry is cold. Harry is furry. Harry is green. Harry is kind. Harry is quiet. Harry is smart. Furry people are quiet. If someone is quiet then they are furry. All furry people are smart. Cold, quiet people are blue. If Anne is blue and Anne is green then Anne is smart. Kind, blue people are cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet then they are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
All furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Cold, quiet people are blue.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If Anne is blue and Anne is green then Anne is smart.
((("Anne" "is" "blue" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "smart" "+"))
Kind, blue people are cold.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Charlie is green.
True
1
proof
[(triple7)]
("Charlie" "is" "green" "+")
triple7
Charlie is not blue.
False
1
inv-proof
[(triple4 OR ((triple5 ((triple6) -> rule1)) -> rule4))]
("Charlie" "is" "blue" "-")
triple4
((triple5 ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is quiet.
True
2
proof
[(((triple6) -> rule1))]
("Charlie" "is" "quiet" "+")
((triple6) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Anne is not blue.
False
3
inv-proof
[(((triple1 triple3) -> rule4))]
("Anne" "is" "blue" "-")
((triple1 triple3) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Anne" "is" "smart" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not smart.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Anne" "is" "smart" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
@0: Anne is cold.[(triple1)] Anne is kind.[(triple2)] Anne is quiet.[(triple3)] Charlie is blue.[(triple4 OR ((triple5 ((triple6) -> rule1)) -> rule4))] Charlie is cold.[(triple5 OR ((triple8 triple4) -> rule6))] Charlie is furry.[(triple6)] Charlie is green.[(triple7)] Charlie is kind.[(triple8)] Charlie is smart.[(triple9 OR ((triple6) -> rule3))] Harry is blue.[(triple10 OR ((triple11 triple15) -> rule4) OR ((triple11 ((triple12) -> rule1)) -> rule4))] Harry is cold.[(triple11 OR ((triple14 triple10) -> rule6))] Harry is furry.[(triple12 OR ((triple15) -> rule2))] Harry is green.[(triple13)] Harry is kind.[(triple14)] Harry is quiet.[(triple15 OR ((triple12) -> rule1))] Harry is smart.[(triple16 OR ((triple12) -> rule3) OR ((((triple15) -> rule2)) -> rule3))] @1: Anne is blue.[(((triple1 triple3) -> rule4))] Anne is furry.[(((triple3) -> rule2))] Charlie is quiet.[(((triple6) -> rule1))] @2: Anne is smart.[(((((triple3) -> rule2)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
((triple5 ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
((triple8 triple4) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
triple8
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
((triple6) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple10
((triple11 triple15) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple11 ((triple12) -> (rule1 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple11
((triple14 triple10) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple12
((triple15) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple13
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
((triple12) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple16
((triple12) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple15) -> (rule2 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((triple1 triple3) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple3) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple6) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2