Anne is kind. Anne is nice. Anne is quiet. Anne is smart. Anne is white. Erin is big. Erin is kind. Erin is nice. Erin is quiet. Erin is rough. Erin is smart. Erin is white. If Anne is nice and Anne is rough then Anne is kind. If Erin is rough then Erin is nice. All smart, nice people are big. If someone is rough and smart then they are nice. Big people are rough. If someone is smart and quiet then they are white. Rough people are nice. Kind, rough people are nice.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
If Anne is nice and Anne is rough then Anne is kind.
((("Anne" "is" "nice" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "kind" "+"))
If Erin is rough then Erin is nice.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "nice" "+"))
All smart, nice people are big.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is rough and smart then they are nice.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If someone is smart and quiet then they are white.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Kind, rough people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Anne is smart.
True
1
proof
[(triple4)]
("Anne" "is" "smart" "+")
triple4
Erin is not white.
False
1
inv-proof
[(triple12 OR ((triple11 triple9) -> rule6))]
("Erin" "is" "white" "-")
triple12
((triple11 triple9) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Anne is big.
True
3
proof
[(((triple4 triple2) -> rule3))]
("Anne" "is" "big" "+")
((triple4 triple2) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
3
inv-proof
[(((triple4 triple2) -> rule3))]
("Anne" "is" "big" "-")
((triple4 triple2) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
True
4
proof
[(((((triple4 triple2) -> rule3)) -> rule5))]
("Anne" "is" "rough" "+")
((((triple4 triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not rough.
False
4
inv-proof
[(((((triple4 triple2) -> rule3)) -> rule5))]
("Anne" "is" "rough" "-")
((((triple4 triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
@0: Anne is kind.[(triple1 OR ((triple2 ((((triple4 triple2) -> rule3)) -> rule5)) -> rule1))] Anne is nice.[(triple2)] Anne is quiet.[(triple3)] Anne is smart.[(triple4)] Anne is white.[(triple5 OR ((triple4 triple3) -> rule6))] Erin is big.[(triple6 OR ((triple11 triple8) -> rule3) OR ((triple11 ((triple10) -> rule2)) -> rule3) OR ((triple11 ((triple10) -> rule7)) -> rule3) OR ((triple11 ((triple10 triple11) -> rule4)) -> rule3) OR ((triple11 ((triple7 triple10) -> rule8)) -> rule3))] Erin is kind.[(triple7)] Erin is nice.[(triple8 OR ((triple10) -> rule2) OR ((triple10) -> rule7) OR ((triple10 triple11) -> rule4) OR ((triple7 triple10) -> rule8) OR ((((triple6) -> rule5)) -> rule2) OR ((((triple6) -> rule5)) -> rule7) OR ((triple7 ((triple6) -> rule5)) -> rule8) OR ((((triple6) -> rule5) triple11) -> rule4))] Erin is quiet.[(triple9)] Erin is rough.[(triple10 OR ((triple6) -> rule5) OR ((((triple11 triple8) -> rule3)) -> rule5))] Erin is smart.[(triple11)] Erin is white.[(triple12 OR ((triple11 triple9) -> rule6))] @1: Anne is big.[(((triple4 triple2) -> rule3))] @2: Anne is rough.[(((((triple4 triple2) -> rule3)) -> rule5))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
((triple2 ((((triple4 triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple5
((triple4 triple3) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple6
((triple11 triple8) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple11 ((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple11 ((triple10) -> (rule7 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple11 ((triple10 triple11) -> (rule4 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple11 ((triple7 triple10) -> (rule8 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
triple8
((triple10) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple10) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple10 triple11) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple7 triple10) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple6) -> (rule5 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((triple7 ((triple6) -> (rule5 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple6) -> (rule5 % int2)) triple11) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Erin is rough.
("Erin" "is" "rough" "+")
triple10
((triple6) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple11 triple8) -> (rule3 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Erin is white.
("Erin" "is" "white" "+")
triple12
((triple11 triple9) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((triple4 triple2) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple4 triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2