Anne is big. Anne is blue. Anne is nice. Anne is red. Anne is rough. Anne is round. Anne is smart. Nice, rough people are red. Big, rough people are red. If someone is smart and red then they are rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Nice, rough people are red.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
Big, rough people are red.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is smart and red then they are rough.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Anne is rough.
True
1
proof
[(triple5 OR ((triple7 triple4) -> rule3))]
("Anne" "is" "rough" "+")
triple5
((triple7 triple4) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not nice.
False
1
inv-proof
[(triple3)]
("Anne" "is" "nice" "-")
triple3
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is nice.[(triple3)] Anne is red.[(triple4 OR ((triple1 triple5) -> rule2) OR ((triple3 triple5) -> rule1))] Anne is rough.[(triple5 OR ((triple7 triple4) -> rule3))] Anne is round.[(triple6)] Anne is smart.[(triple7)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple1 triple5) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple3 triple5) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple7 triple4) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple6
Anne is smart.
("Anne" "is" "smart" "+")
triple7