Anne is blue. Blue people are green. Cold, blue people are kind. If someone is rough and cold then they are blue. All green people are white. If Anne is white then Anne is round. Green, rough people are kind.
Anne is blue.
("Anne" "is" "blue" "+")
Blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Cold, blue people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is rough and cold then they are blue.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
All green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If Anne is white then Anne is round.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "round" "+"))
Green, rough people are kind.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Anne is green.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "green" "+")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "green" "-")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Anne" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Anne" "is" "white" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is round.
True
4
proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule5))]
("Anne" "is" "round" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not round.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule5))]
("Anne" "is" "round" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is blue.[(triple1)] @1: Anne is green.[(((triple1) -> rule1))] @2: Anne is white.[(((((triple1) -> rule1)) -> rule4))] @3: Anne is round.[(((((((triple1) -> rule1)) -> rule4)) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3