Anne is big. Harry is blue. All blue people are kind. Blue, white people are not kind. All big people are white. All smart people are not blue. If someone is blue and white then they are young. All kind people are not cold.
Anne is big.
("Anne" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Blue, white people are not kind.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "-"))
All big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
All smart people are not blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "-"))
If someone is blue and white then they are young.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
All kind people are not cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "-"))
Harry is blue.
True
1
proof
[(triple2)]
("Harry" "is" "blue" "+")
triple2
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is white.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "white" "+")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "white" "-")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Harry is not cold.
True
3
proof
[(((((triple2) -> rule1)) -> rule6))]
("Harry" "is" "cold" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("Harry" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "kind" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "white" "+")
Harry is not young.
Unknown
inv-rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Harry" "is" "young" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is big.[(triple1)] Harry is blue.[(triple2)] @1: Anne is white.[(((triple1) -> rule3))] Harry is kind.[(((triple2) -> rule1))] @2: Harry is not cold.[(((((triple2) -> rule1)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple2) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2