Anne is big. Nice people are green. Big people are young. If someone is young then they are big. All blue people are big. All blue people are kind. All young people are blue. If Anne is green and Anne is not young then Anne is cold. If Anne is nice and Anne is not big then Anne is kind.
Anne is big.
("Anne" "is" "big" "+")
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
All blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
All young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If Anne is green and Anne is not young then Anne is cold.
((("Anne" "is" "green" "+") ("Anne" "is" "young" "~")) -> ("Anne" "is" "cold" "+"))
If Anne is nice and Anne is not big then Anne is kind.
((("Anne" "is" "nice" "+") ("Anne" "is" "big" "~")) -> ("Anne" "is" "kind" "+"))
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 young.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "young" "+")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "young" "-")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not blue.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is kind.
True
4
proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule5))]
("Anne" "is" "kind" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not kind.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule5))]
("Anne" "is" "kind" "-")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is big.[(triple1)] @1: Anne is young.[(((triple1) -> rule2))] @2: Anne is blue.[(((((triple1) -> rule2)) -> rule6))] @3: Anne is kind.[(((((((triple1) -> rule2)) -> rule6)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3