Anne is red. All green, smart things are quiet. If Anne is red then Anne is white. All cold, kind things are green. All red, white things are quiet. All white things are smart. Red, smart things are cold. All smart things are quiet. Smart things are cold.
Anne is red.
("Anne" "is" "red" "+")
All green, smart things are quiet.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If Anne is red then Anne is white.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "white" "+"))
All cold, kind things are green.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All red, white things are quiet.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
All white things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Red, smart things are cold.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Smart things are cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Anne is not red.
False
1
inv-proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Anne is white.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "white" "+")
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "white" "-")
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is red.[(triple1)] @1: Anne is white.[(((triple1) -> rule2))] @2: Anne is quiet.[(((triple1 ((triple1) -> rule2)) -> rule4) OR ((((((triple1) -> rule2)) -> rule5)) -> rule7))] Anne is smart.[(((((triple1) -> rule2)) -> rule5))] @3: Anne is cold.[(((((((triple1) -> rule2)) -> rule5)) -> rule8) OR ((triple1 ((((triple1) -> rule2)) -> rule5)) -> rule6))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3