Charlie is cold. All red things are cold. If something is cold then it is round. Quiet, rough things are red. If something is quiet then it is round. Cold, blue things are young. All round, rough things are red. If something is blue then it is round. All round things are blue.
Charlie is cold.
("Charlie" "is" "cold" "+")
All red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Quiet, rough things are red.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is quiet then it is round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
Cold, blue things are young.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All round, rough things are red.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is blue then it is round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
All round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Charlie is cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Charlie is not cold.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "cold" "-")
triple1
Charlie is round.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "round" "+")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "round" "-")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
True
3
proof
[(((((triple1) -> rule2)) -> rule8))]
("Charlie" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not blue.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule8))]
("Charlie" "is" "blue" "-")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
True
5
proof
[(((triple1 ((((triple1) -> rule2)) -> rule8)) -> rule5))]
("Charlie" "is" "young" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is not young.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule2)) -> rule8)) -> rule5))]
("Charlie" "is" "young" "-")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is cold.[(triple1)] @1: Charlie is round.[(((triple1) -> rule2))] @2: Charlie is blue.[(((((triple1) -> rule2)) -> rule8))] @3: Charlie is young.[(((triple1 ((((triple1) -> rule2)) -> rule8)) -> rule5))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3