Anne is blue. Anne is furry. Anne is green. Anne is white. Fiona is blue. Fiona is cold. Fiona is furry. Fiona is kind. Harry is blue. Harry is cold. Harry is furry. Harry is green. Harry is kind. Harry is red. Harry is white. If something is white and blue then it is red. All furry, red things are kind. Kind, blue things are white. If something is blue then it is kind. If Fiona is furry and Fiona is white then Fiona is green. If Harry is blue and Harry is white then Harry is kind. If something is blue and white then it is red. All red, white things are kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is white.
("Anne" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
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 red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is white and blue then it is red.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
All furry, red things are kind.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Kind, blue things are white.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If something is blue then it is kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If Fiona is furry and Fiona is white then Fiona is green.
((("Fiona" "is" "furry" "+") ("Fiona" "is" "white" "+")) -> ("Fiona" "is" "green" "+"))
If Harry is blue and Harry is white then Harry is kind.
((("Harry" "is" "blue" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "kind" "+"))
If something is blue and white then it is red.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All red, white things are kind.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Harry is cold.
True
1
proof
[(triple10)]
("Harry" "is" "cold" "+")
triple10
Fiona is not blue.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "blue" "-")
triple5
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2)] Anne is green.[(triple3)] Anne is white.[(triple4 OR ((((triple1) -> rule4) triple1) -> rule3))] Fiona is blue.[(triple5)] Fiona is cold.[(triple6)] Fiona is furry.[(triple7)] Fiona is kind.[(triple8 OR ((triple5) -> rule4))] Harry is blue.[(triple9)] Harry is cold.[(triple10)] Harry is furry.[(triple11)] Harry is green.[(triple12)] Harry is kind.[(triple13 OR ((triple9) -> rule4) OR ((triple11 triple14) -> rule2) OR ((triple14 triple15) -> rule8) OR ((triple9 triple15) -> rule6) OR ((triple11 ((triple15 triple9) -> rule1)) -> rule2) OR ((triple11 ((triple9 triple15) -> rule7)) -> rule2) OR ((((triple15 triple9) -> rule1) triple15) -> rule8) OR ((((triple9 triple15) -> rule7) triple15) -> rule8))] Harry is red.[(triple14 OR ((triple15 triple9) -> rule1) OR ((triple9 triple15) -> rule7) OR ((triple9 ((triple13 triple9) -> rule3)) -> rule7) OR ((((triple13 triple9) -> rule3) triple9) -> rule1) OR ((triple9 ((((triple9) -> rule4) triple9) -> rule3)) -> rule7) OR ((((((triple9) -> rule4) triple9) -> rule3) triple9) -> rule1))] Harry is white.[(triple15 OR ((triple13 triple9) -> rule3) OR ((((triple9) -> rule4) triple9) -> rule3) OR ((((triple11 triple14) -> rule2) triple9) -> rule3))] @1: Anne is kind.[(((triple1) -> rule4) OR ((triple2 ((triple1 triple4) -> rule7)) -> rule2) OR ((triple2 ((triple4 triple1) -> rule1)) -> rule2) OR ((((triple1 triple4) -> rule7) triple4) -> rule8) OR ((((triple4 triple1) -> rule1) triple4) -> rule8))] Anne is red.[(((triple1 triple4) -> rule7) OR ((triple4 triple1) -> rule1) OR ((triple1 ((((triple1) -> rule4) triple1) -> rule3)) -> rule7) OR ((((((triple1) -> rule4) triple1) -> rule3) triple1) -> rule1))] Fiona is white.[(((triple8 triple5) -> rule3) OR ((((triple5) -> rule4) triple5) -> rule3))] @2: Fiona is green.[(((triple7 ((triple8 triple5) -> rule3)) -> rule5) OR ((triple7 ((((triple5) -> rule4) triple5) -> rule3)) -> rule5))] Fiona is red.[(((triple5 ((triple8 triple5) -> rule3)) -> rule7) OR ((((triple8 triple5) -> rule3) triple5) -> rule1) OR ((triple5 ((((triple5) -> rule4) triple5) -> rule3)) -> rule7) OR ((((((triple5) -> rule4) triple5) -> rule3) triple5) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
((((triple1) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
Fiona is kind.
("Fiona" "is" "kind" "+")
triple8
((triple5) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
triple13
((triple9) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple11 triple14) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple14 triple15) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple9 triple15) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple11 ((triple15 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((triple11 ((triple9 triple15) -> (rule7 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple15 triple9) -> (rule1 % int2)) triple15) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple9 triple15) -> (rule7 % int2)) triple15) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple14
((triple15 triple9) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple9 triple15) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple9 ((triple13 triple9) -> (rule3 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple13 triple9) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((triple9 ((((triple9) -> (rule4 % int3)) triple9) -> (rule3 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((triple9) -> (rule4 % int3)) triple9) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
triple15
((triple13 triple9) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple9) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple11 triple14) -> (rule2 % int2)) triple9) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple2 ((triple1 triple4) -> (rule7 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((triple2 ((triple4 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple1 triple4) -> (rule7 % int2)) triple4) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple4 triple1) -> (rule1 % int2)) triple4) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((triple1 triple4) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple4 triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple1 ((((triple1) -> (rule4 % int3)) triple1) -> (rule3 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((((triple1) -> (rule4 % int3)) triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
((triple8 triple5) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple5) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((triple7 ((triple8 triple5) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((triple7 ((((triple5) -> (rule4 % int3)) triple5) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((triple5 ((triple8 triple5) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((triple8 triple5) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((triple5 ((((triple5) -> (rule4 % int3)) triple5) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((((triple5) -> (rule4 % int3)) triple5) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3