Anne is blue. Anne is cold. Anne is furry. Anne is kind. Anne is nice. Anne is quiet. Anne is white. All kind, quiet things are furry. Quiet things are white. All furry, quiet things are blue. All quiet, furry things are cold. Cold, nice things are quiet. White, blue things are cold.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
All kind, quiet things are furry.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
All furry, quiet things are blue.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
All quiet, furry things are cold.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Cold, nice things are quiet.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
White, blue things are cold.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Anne is furry.
True
1
proof
[(triple3 OR ((triple4 triple6) -> rule1) OR ((triple4 ((triple2 triple5) -> rule5)) -> rule1) OR ((triple4 ((((triple7 triple1) -> rule6) triple5) -> rule5)) -> rule1))]
("Anne" "is" "furry" "+")
triple3
((triple4 triple6) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple4 ((triple2 triple5) -> (rule5 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((triple4 ((((triple7 triple1) -> (rule6 % int3)) triple5) -> (rule5 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not blue.
False
1
inv-proof
[(triple1 OR ((triple3 triple6) -> rule3) OR ((triple3 ((triple2 triple5) -> rule5)) -> rule3) OR ((((triple4 triple6) -> rule1) triple6) -> rule3) OR ((((triple4 triple6) -> rule1) ((triple2 triple5) -> rule5)) -> rule3) OR ((((triple4 ((triple2 triple5) -> rule5)) -> rule1) triple6) -> rule3) OR ((((triple4 ((triple2 triple5) -> rule5)) -> rule1) ((triple2 triple5) -> rule5)) -> rule3))]
("Anne" "is" "blue" "-")
triple1
((triple3 triple6) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple3 ((triple2 triple5) -> (rule5 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((triple4 triple6) -> (rule1 % int2)) triple6) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple4 triple6) -> (rule1 % int3)) ((triple2 triple5) -> (rule5 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((triple4 ((triple2 triple5) -> (rule5 % int3))) -> (rule1 % int2)) triple6) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((((triple4 ((triple2 triple5) -> (rule5 % int3))) -> (rule1 % int2)) ((triple2 triple5) -> (rule5 % int3))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
@0: Anne is blue.[(triple1 OR ((triple3 triple6) -> rule3) OR ((triple3 ((triple2 triple5) -> rule5)) -> rule3) OR ((((triple4 triple6) -> rule1) triple6) -> rule3) OR ((((triple4 triple6) -> rule1) ((triple2 triple5) -> rule5)) -> rule3) OR ((((triple4 ((triple2 triple5) -> rule5)) -> rule1) triple6) -> rule3) OR ((((triple4 ((triple2 triple5) -> rule5)) -> rule1) ((triple2 triple5) -> rule5)) -> rule3))] Anne is cold.[(triple2 OR ((triple6 triple3) -> rule4) OR ((triple7 triple1) -> rule6) OR ((triple6 ((triple4 triple6) -> rule1)) -> rule4) OR ((triple7 ((triple3 triple6) -> rule3)) -> rule6) OR ((((triple6) -> rule2) triple1) -> rule6) OR ((((triple6) -> rule2) ((triple3 triple6) -> rule3)) -> rule6) OR ((triple7 ((((triple4 triple6) -> rule1) triple6) -> rule3)) -> rule6) OR ((((triple6) -> rule2) ((((triple4 triple6) -> rule1) triple6) -> rule3)) -> rule6))] Anne is furry.[(triple3 OR ((triple4 triple6) -> rule1) OR ((triple4 ((triple2 triple5) -> rule5)) -> rule1) OR ((triple4 ((((triple7 triple1) -> rule6) triple5) -> rule5)) -> rule1))] Anne is kind.[(triple4)] Anne is nice.[(triple5)] Anne is quiet.[(triple6 OR ((triple2 triple5) -> rule5) OR ((((triple7 triple1) -> rule6) triple5) -> rule5))] Anne is white.[(triple7 OR ((triple6) -> rule2) OR ((((triple2 triple5) -> rule5)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple3 triple6) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple3 ((triple2 triple5) -> (rule5 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((triple4 triple6) -> (rule1 % int2)) triple6) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple4 triple6) -> (rule1 % int3)) ((triple2 triple5) -> (rule5 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((triple4 ((triple2 triple5) -> (rule5 % int3))) -> (rule1 % int2)) triple6) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((((triple4 ((triple2 triple5) -> (rule5 % int3))) -> (rule1 % int2)) ((triple2 triple5) -> (rule5 % int3))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple6 triple3) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple7 triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple6 ((triple4 triple6) -> (rule1 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((triple7 ((triple3 triple6) -> (rule3 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple6) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple3 triple6) -> (rule3 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((triple7 ((((triple4 triple6) -> (rule1 % int3)) triple6) -> (rule3 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((triple6) -> (rule2 % int4)) ((((triple4 triple6) -> (rule1 % int3)) triple6) -> (rule3 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
triple3
((triple4 triple6) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple4 ((triple2 triple5) -> (rule5 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((triple4 ((((triple7 triple1) -> (rule6 % int3)) triple5) -> (rule5 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
triple5
Anne is quiet.
("Anne" "is" "quiet" "+")
triple6
((triple2 triple5) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple7 triple1) -> (rule6 % int2)) triple5) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple7
((triple6) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple2 triple5) -> (rule5 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2