Anne is big. Anne is blue. Anne is furry. Anne is green. Anne is kind. Anne is rough. Anne is white. Furry things are blue. Furry things are rough. If something is kind and green then it is white. All green things are furry. All rough things are big. If something is blue then it is kind.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If something is kind and green then it is white.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
All green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is blue then it is kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Anne is white.
True
1
proof
[(triple7 OR ((triple5 triple4) -> rule3) OR ((((triple2) -> rule6) triple4) -> rule3) OR ((((((triple3) -> rule1)) -> rule6) triple4) -> rule3) OR ((((((((triple4) -> rule4)) -> rule1)) -> rule6) triple4) -> rule3))]
("Anne" "is" "white" "+")
triple7
((triple5 triple4) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple2) -> (rule6 % int2)) triple4) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2)) triple4) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((((triple4) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule6 % int2)) triple4) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is not kind.
False
1
inv-proof
[(triple5 OR ((triple2) -> rule6) OR ((((triple3) -> rule1)) -> rule6) OR ((((((triple4) -> rule4)) -> rule1)) -> rule6))]
("Anne" "is" "kind" "-")
triple5
((triple2) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
@0: Anne is big.[(triple1 OR ((triple6) -> rule5) OR ((((triple3) -> rule2)) -> rule5) OR ((((((triple4) -> rule4)) -> rule2)) -> rule5))] Anne is blue.[(triple2 OR ((triple3) -> rule1) OR ((((triple4) -> rule4)) -> rule1))] Anne is furry.[(triple3 OR ((triple4) -> rule4))] Anne is green.[(triple4)] Anne is kind.[(triple5 OR ((triple2) -> rule6) OR ((((triple3) -> rule1)) -> rule6) OR ((((((triple4) -> rule4)) -> rule1)) -> rule6))] Anne is rough.[(triple6 OR ((triple3) -> rule2) OR ((((triple4) -> rule4)) -> rule2))] Anne is white.[(triple7 OR ((triple5 triple4) -> rule3) OR ((((triple2) -> rule6) triple4) -> rule3) OR ((((((triple3) -> rule1)) -> rule6) triple4) -> rule3) OR ((((((((triple4) -> rule4)) -> rule1)) -> rule6) triple4) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple6) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple3) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
((triple4) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple4
Anne is kind.
("Anne" "is" "kind" "+")
triple5
((triple2) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
triple6
((triple3) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple7
((triple5 triple4) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple2) -> (rule6 % int2)) triple4) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2)) triple4) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((((triple4) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule6 % int2)) triple4) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4