Anne is big. Kind, nice things are round. All big things are round. Round things are not nice. If something is big then it is kind. If something is kind and not round then it is smart. If something is smart and big then it is white. All round things are not white. If something is round and not nice then it is red.
Anne is big.
("Anne" "is" "big" "+")
Kind, nice things are round.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
All big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Round things are not nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "-"))
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is kind and not round then it is smart.
((("something" "is" "kind" "+") ("something" "is" "round" "~")) -> ("something" "is" "smart" "+"))
If something is smart and big then it is white.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
All round things are not white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "-"))
If something is round and not nice then it is red.
((("something" "is" "round" "+") ("something" "is" "nice" "~")) -> ("something" "is" "red" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is round.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "round" "+")
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "round" "-")
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not nice.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "nice" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is nice.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is red.
True
6
proof
[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule3)) -> rule8))]
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not red.
False
6
inv-proof
[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule3)) -> rule8))]
("Anne" "is" "red" "-")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
@0: Anne is big.[(triple1)] @1: Anne is kind.[(((triple1) -> rule4))] Anne is round.[(((triple1) -> rule2))] @2: Anne is not nice.[(((((triple1) -> rule2)) -> rule3))] Anne is not white.[(((((triple1) -> rule2)) -> rule7))] @3: Anne is red.[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule3)) -> rule8))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not white.
("Anne" "is" "white" "-")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
int2
Anne is round.
("Anne" "is" "round" "+")
int3