Charlie is young. If someone is young then they are cold. If someone is cold then they are red. If someone is nice and not white then they are quiet.
Charlie is young.
("Charlie" "is" "young" "+")
If someone is young then they are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold then they are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is nice and not white then they are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "quiet" "+"))
Charlie is young.
True
1
proof
[(triple1)]
("Charlie" "is" "young" "+")
triple1
Charlie is not young.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "young" "-")
triple1
Charlie is cold.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not red.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "red" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is young.[(triple1)] @1: Charlie is cold.[(((triple1) -> rule1))] @2: Charlie is red.[(((((triple1) -> rule1)) -> rule2))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2