Charlie is white. Erin is green. If Charlie is white then Charlie is blue. All kind things are blue. All rough things are quiet. If Charlie is white and Charlie is quiet then Charlie is green. Cold, quiet things are white. If Charlie is blue then Charlie is rough. All rough, white things are green. If Erin is blue then Erin is cold.
Charlie is white.
("Charlie" "is" "white" "+")
Erin is green.
("Erin" "is" "green" "+")
If Charlie is white then Charlie is blue.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "blue" "+"))
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
All rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is white and Charlie is quiet then Charlie is green.
((("Charlie" "is" "white" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "green" "+"))
Cold, quiet things are white.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If Charlie is blue then Charlie is rough.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "rough" "+"))
All rough, white things are green.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If Erin is blue then Erin is cold.
((("Erin" "is" "blue" "+")) -> ("Erin" "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 blue.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "blue" "-")
((triple1) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("Charlie" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not rough.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("Charlie" "is" "rough" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Erin is not cold.
Unknown
inv-rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule8 <- rule2 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is white.
Unknown
rconc
[@2: Erin is white.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Erin" "is" "white" "+")
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Charlie is white.[(triple1)] Erin is green.[(triple2)] @1: Charlie is blue.[(((triple1) -> rule1))] @2: Charlie is rough.[(((((triple1) -> rule1)) -> rule6))] @3: Charlie is green.[(((((((triple1) -> rule1)) -> rule6) triple1) -> rule7) OR ((triple1 ((((((triple1) -> rule1)) -> rule6)) -> rule3)) -> rule4))] Charlie is quiet.[(((((((triple1) -> rule1)) -> rule6)) -> rule3))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((triple1 ((((((triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3