Anne is big. Anne is green. Anne is kind. Anne is rough. Anne is round. Anne is smart. Anne is young. Fiona is green. Fiona is kind. Fiona is round. Fiona is smart. Fiona is young. If someone is kind and round then they are green. If Fiona is kind and Fiona is smart then Fiona is rough. If someone is round then they are green.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If someone is kind and round then they are green.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If Fiona is kind and Fiona is smart then Fiona is rough.
((("Fiona" "is" "kind" "+") ("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "rough" "+"))
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Fiona is round.
True
1
proof
[(triple10)]
("Fiona" "is" "round" "+")
triple10
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
@0: Anne is big.[(triple1)] Anne is green.[(triple2 OR ((triple5) -> rule3) OR ((triple3 triple5) -> rule1))] Anne is kind.[(triple3)] Anne is rough.[(triple4)] Anne is round.[(triple5)] Anne is smart.[(triple6)] Anne is young.[(triple7)] Fiona is green.[(triple8 OR ((triple10) -> rule3) OR ((triple9 triple10) -> rule1))] Fiona is kind.[(triple9)] Fiona is round.[(triple10)] Fiona is smart.[(triple11)] Fiona is young.[(triple12)] @1: Fiona is rough.[(((triple9 triple11) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple5) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple3 triple5) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
Fiona is green.
("Fiona" "is" "green" "+")
triple8
((triple10) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple9 triple10) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
Fiona is young.
("Fiona" "is" "young" "+")
triple12
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple9 triple11) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1