Anne is big. Anne is blue. Anne is quiet. Anne is round. Anne is smart. Anne is white. Anne is young. Erin is big. Erin is blue. Erin is quiet. Erin is round. Erin is smart. Erin is white. Erin is young. Young people are big. If Erin is quiet then Erin is white.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If Erin is quiet then Erin is white.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "white" "+"))
Erin is big.
True
1
proof
[(triple8 OR ((triple14) -> rule1))]
("Erin" "is" "big" "+")
triple8
((triple14) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not young.
False
1
inv-proof
[(triple14)]
("Erin" "is" "young" "-")
triple14
@0: Anne is big.[(triple1 OR ((triple7) -> rule1))] Anne is blue.[(triple2)] Anne is quiet.[(triple3)] Anne is round.[(triple4)] Anne is smart.[(triple5)] Anne is white.[(triple6)] Anne is young.[(triple7)] Erin is big.[(triple8 OR ((triple14) -> rule1))] Erin is blue.[(triple9)] Erin is quiet.[(triple10)] Erin is round.[(triple11)] Erin is smart.[(triple12)] Erin is white.[(triple13 OR ((triple10) -> rule2))] Erin is young.[(triple14)]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple7) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
((triple14) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Erin is white.
("Erin" "is" "white" "+")
triple13
((triple10) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple14