Charlie is white. All blue, red things are cold. Rough, white things are blue. If something is cold then it is rough. If something is rough then it is blue. All young things are cold. All rough, green things are cold. If something is white then it is rough. If something is young and white then it is cold.
Charlie is white.
("Charlie" "is" "white" "+")
All blue, red things are cold.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Rough, white things are blue.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If something is cold then it is rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it is blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All rough, green things are cold.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is white then it is rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If something is young and white then it is cold.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Charlie is white.
True
1
proof
[(triple1)]
("Charlie" "is" "white" "+")
triple1
Charlie is not white.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "white" "-")
triple1
Charlie is rough.
True
2
proof
[(((triple1) -> rule7))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple1) -> rule7))]
("Charlie" "is" "rough" "-")
((triple1) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
True
3
proof
[(((((triple1) -> rule7)) -> rule4) OR ((((triple1) -> rule7) triple1) -> rule2))]
("Charlie" "is" "blue" "+")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple1) -> (rule7 % int2)) triple1) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not blue.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule4) OR ((((triple1) -> rule7) triple1) -> rule2))]
("Charlie" "is" "blue" "-")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple1) -> (rule7 % int2)) triple1) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is white.[(triple1)] @1: Charlie is rough.[(((triple1) -> rule7))] @2: Charlie is blue.[(((((triple1) -> rule7)) -> rule4) OR ((((triple1) -> rule7) triple1) -> rule2))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple1) -> (rule7 % int2)) triple1) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2