Anne is not big. Anne is cold. Anne is furry. Anne is not green. Anne is kind. Anne is not quiet. Anne is not red. Harry is big. Harry is cold. Harry is quiet. If Anne is green and Anne is cold then Anne is furry. If Harry is cold and Harry is red then Harry is furry. All green people are not kind. Red, furry people are kind. Green people are not quiet. Quiet people are red. All red people are furry. All big, green people are furry.
Anne is not big.
("Anne" "is" "big" "-")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not green.
("Anne" "is" "green" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is not red.
("Anne" "is" "red" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Anne is green and Anne is cold then Anne is furry.
((("Anne" "is" "green" "+") ("Anne" "is" "cold" "+")) -> ("Anne" "is" "furry" "+"))
If Harry is cold and Harry is red then Harry is furry.
((("Harry" "is" "cold" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "furry" "+"))
All green people are not kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "-"))
Red, furry people are kind.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Green people are not quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "-"))
Quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
All red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All big, green people are furry.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Anne is not quiet.
True
1
proof
[(triple6)]
("Anne" "is" "quiet" "-")
triple6
Harry is not quiet.
False
1
inv-proof
[(triple10)]
("Harry" "is" "quiet" "-")
triple10
Harry is red.
True
2
proof
[(((triple10) -> rule6))]
("Harry" "is" "red" "+")
((triple10) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple10) -> rule6))]
("Harry" "is" "red" "-")
((triple10) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
True
3
proof
[(((((triple10) -> rule6)) -> rule7) OR ((triple9 ((triple10) -> rule6)) -> rule2))]
("Harry" "is" "furry" "+")
((((triple10) -> (rule6 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((triple9 ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((((triple10) -> rule6)) -> rule7) OR ((triple9 ((triple10) -> rule6)) -> rule2))]
("Harry" "is" "furry" "-")
((((triple10) -> (rule6 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((triple9 ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
True
6
proof
[(((((triple10) -> rule6) ((((triple10) -> rule6)) -> rule7)) -> rule4) OR ((((triple10) -> rule6) ((triple9 ((triple10) -> rule6)) -> rule2)) -> rule4))]
("Harry" "is" "kind" "+")
((((triple10) -> (rule6 % int3)) ((((triple10) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((triple10) -> (rule6 % int3)) ((triple9 ((triple10) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not kind.
False
6
inv-proof
[(((((triple10) -> rule6) ((((triple10) -> rule6)) -> rule7)) -> rule4) OR ((((triple10) -> rule6) ((triple9 ((triple10) -> rule6)) -> rule2)) -> rule4))]
("Harry" "is" "kind" "-")
((((triple10) -> (rule6 % int3)) ((((triple10) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((triple10) -> (rule6 % int3)) ((triple9 ((triple10) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
@0: Anne is cold.[(triple2)] Anne is furry.[(triple3)] Anne is kind.[(triple5)] Anne is not big.[(triple1)] Anne is not green.[(triple4)] Anne is not quiet.[(triple6)] Anne is not red.[(triple7)] Harry is big.[(triple8)] Harry is cold.[(triple9)] Harry is quiet.[(triple10)] @1: Harry is red.[(((triple10) -> rule6))] @2: Harry is furry.[(((((triple10) -> rule6)) -> rule7) OR ((triple9 ((triple10) -> rule6)) -> rule2))] @3: Harry is kind.[(((((triple10) -> rule6) ((((triple10) -> rule6)) -> rule7)) -> rule4) OR ((((triple10) -> rule6) ((triple9 ((triple10) -> rule6)) -> rule2)) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple5
Anne is not big.
("Anne" "is" "big" "-")
triple1
Anne is not green.
("Anne" "is" "green" "-")
triple4
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple6
Anne is not red.
("Anne" "is" "red" "-")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
((triple10) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple10) -> (rule6 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((triple9 ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple10) -> (rule6 % int3)) ((((triple10) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((triple10) -> (rule6 % int3)) ((triple9 ((triple10) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3