Anne is cold. Anne is not green. Anne is round. If Anne is not green then Anne is round. Nice, quiet people are not big. If someone is cold then they are nice. If Anne is quiet and Anne is not green then Anne is young. Nice people are quiet. If Anne is quiet and Anne is not round then Anne is not big. If someone is round and big then they are young. Round, green people are young.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is not green.
("Anne" "is" "green" "-")
Anne is round.
("Anne" "is" "round" "+")
If Anne is not green then Anne is round.
((("Anne" "is" "green" "~")) -> ("Anne" "is" "round" "+"))
Nice, quiet people are not big.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "-"))
If someone is cold then they are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If Anne is quiet and Anne is not green then Anne is young.
((("Anne" "is" "quiet" "+") ("Anne" "is" "green" "~")) -> ("Anne" "is" "young" "+"))
Nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is quiet and Anne is not round then Anne is not big.
((("Anne" "is" "quiet" "+") ("Anne" "is" "round" "~")) -> ("Anne" "is" "big" "-"))
If someone is round and big then they are young.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Round, green people are young.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Anne is not green.
True
1
proof
[(triple2)]
("Anne" "is" "green" "-")
triple2
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is nice.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
True
3
proof
[(((((triple1) -> rule3)) -> rule5))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not quiet.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not big.
True
6
proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule2))]
("Anne" "is" "big" "-")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not young.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule5) triple2) -> rule4))]
("Anne" "is" "young" "-")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) triple2) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
@0: Anne is cold.[(triple1)] Anne is not green.[(triple2)] Anne is round.[(triple3 OR ((triple2) -> rule1))] @1: Anne is nice.[(((triple1) -> rule3))] @2: Anne is quiet.[(((((triple1) -> rule3)) -> rule5))] @3: Anne is not big.[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule2))] Anne is young.[(((((((triple1) -> rule3)) -> rule5) triple2) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is not green.
("Anne" "is" "green" "-")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
((triple2) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not big.
("Anne" "is" "big" "-")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) triple2) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3