Anne is cold. Charlie is blue. Fiona is cold. Cold people are nice. If someone is kind and blue then they are white. If someone is white and blue then they are smart. If someone is kind then they are blue. All cold people are kind. If Charlie is white then Charlie is smart.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is kind and blue then they are white.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If someone is white and blue then they are smart.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If someone is kind then they are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
All cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is white then Charlie is smart.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "smart" "+"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is kind.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "kind" "-")
((triple1) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is smart.
Unknown
rconc
[@3: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule5 <- FAIL)]]
("Charlie" "is" "smart" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is cold.[(triple1)] Charlie is blue.[(triple2)] Fiona is cold.[(triple3)] @1: Anne is kind.[(((triple1) -> rule5))] Anne is nice.[(((triple1) -> rule1))] Fiona is kind.[(((triple3) -> rule5))] Fiona is nice.[(((triple3) -> rule1))] @2: Anne is blue.[(((((triple1) -> rule5)) -> rule4))] Fiona is blue.[(((((triple3) -> rule5)) -> rule4))] @3: Anne is white.[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule4)) -> rule2))] Fiona is white.[(((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule4)) -> rule2))] @4: Anne is smart.[(((((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule4)) -> rule2) ((((triple1) -> rule5)) -> rule4)) -> rule3))] Fiona is smart.[(((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule4)) -> rule2) ((((triple3) -> rule5)) -> rule4)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple3) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple1) -> (rule5 % int4)) ((((triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2)) ((((triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
((((((triple3) -> (rule5 % int4)) ((((triple3) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2)) ((((triple3) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4