Anne is big. Anne is cold. Anne is furry. Anne is green. Anne is rough. Anne is white. Anne is young. Green people are cold. If someone is white then they are green. Cold, big people are green.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is white then they are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Cold, big people are green.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Anne is cold.
True
1
proof
[(triple2 OR ((triple4) -> rule1) OR ((((triple6) -> rule2)) -> rule1))]
("Anne" "is" "cold" "+")
triple2
((triple4) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not green.
False
1
inv-proof
[(triple4 OR ((triple6) -> rule2) OR ((triple2 triple1) -> rule3))]
("Anne" "is" "green" "-")
triple4
((triple6) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple2 triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
@0: Anne is big.[(triple1)] Anne is cold.[(triple2 OR ((triple4) -> rule1) OR ((((triple6) -> rule2)) -> rule1))] Anne is furry.[(triple3)] Anne is green.[(triple4 OR ((triple6) -> rule2) OR ((triple2 triple1) -> rule3))] Anne is rough.[(triple5)] Anne is white.[(triple6)] Anne is young.[(triple7)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple4) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is green.
("Anne" "is" "green" "+")
triple4
((triple6) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple2 triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7