Anne is big. Anne is green. Anne is not quiet. All big people are nice. If someone is blue then they are not nice. If Anne is nice and Anne is green then Anne is rough. Rough, nice people are not round. All green, round people are blue. If someone is round and not blue then they are quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
All big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue then they are not nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "-"))
If Anne is nice and Anne is green then Anne is rough.
((("Anne" "is" "nice" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "rough" "+"))
Rough, nice people are not round.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "-"))
All green, round people are blue.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is round and not blue then they are quiet.
((("someone" "is" "round" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "quiet" "+"))
Anne is not quiet.
True
1
proof
[(triple3)]
("Anne" "is" "quiet" "-")
triple3
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is nice.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "nice" "-")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
True
4
proof
[(((((triple1) -> rule1) triple2) -> rule3))]
("Anne" "is" "rough" "+")
((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not rough.
False
4
inv-proof
[(((((triple1) -> rule1) triple2) -> rule3))]
("Anne" "is" "rough" "-")
((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not round.
True
7
proof
[(((((((triple1) -> rule1) triple2) -> rule3) ((triple1) -> rule1)) -> rule4))]
("Anne" "is" "round" "-")
((((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int2)) ((triple1) -> (rule1 % int3))) -> (rule4 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is round.
False
7
inv-proof
[(((((((triple1) -> rule1) triple2) -> rule3) ((triple1) -> rule1)) -> rule4))]
("Anne" "is" "round" "+")
((((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int2)) ((triple1) -> (rule1 % int3))) -> (rule4 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
@0: Anne is big.[(triple1)] Anne is green.[(triple2)] Anne is not quiet.[(triple3)] @1: Anne is nice.[(((triple1) -> rule1))] @2: Anne is rough.[(((((triple1) -> rule1) triple2) -> rule3))] @3: Anne is not round.[(((((((triple1) -> rule1) triple2) -> rule3) ((triple1) -> rule1)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not round.
("Anne" "is" "round" "-")
((((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int2)) ((triple1) -> (rule1 % int3))) -> (rule4 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3