Anne is not nice. Anne is red. Anne is smart. Smart people are cold. All smart, red people are cold. If someone is cold and nice then they are rough. If Anne is big and Anne is not nice then Anne is green. If Anne is green then Anne is smart. Smart people are big.
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
All smart, red people are cold.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and nice then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If Anne is big and Anne is not nice then Anne is green.
((("Anne" "is" "big" "+") ("Anne" "is" "nice" "~")) -> ("Anne" "is" "green" "+"))
If Anne is green then Anne is smart.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "smart" "+"))
Smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Anne is smart.
True
1
proof
[(triple3)]
("Anne" "is" "smart" "+")
triple3
Anne is nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Anne is big.
True
2
proof
[(((triple3) -> rule6))]
("Anne" "is" "big" "+")
((triple3) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple3) -> rule6))]
("Anne" "is" "big" "-")
((triple3) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
True
4
proof
[(((((triple3) -> rule6) triple1) -> rule4))]
("Anne" "is" "green" "+")
((((triple3) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not green.
False
4
inv-proof
[(((((triple3) -> rule6) triple1) -> rule4))]
("Anne" "is" "green" "-")
((((triple3) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
@0: Anne is not nice.[(triple1)] Anne is red.[(triple2)] Anne is smart.[(triple3)] @1: Anne is big.[(((triple3) -> rule6))] Anne is cold.[(((triple3) -> rule1) OR ((triple3 triple2) -> rule2))] @2: Anne is green.[(((((triple3) -> rule6) triple1) -> rule4))]
Anne is not nice.
("Anne" "is" "nice" "-")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple3) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple3 triple2) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple3) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2