Anne is white. White, smart things are nice. Nice, round things are white. White things are smart. If Anne is nice and Anne is white then Anne is blue. All round, furry things are white. Rough things are round. If something is furry then it is smart. All furry, smart things are nice.
Anne is white.
("Anne" "is" "white" "+")
White, smart things are nice.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Nice, round things are white.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
White things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If Anne is nice and Anne is white then Anne is blue.
((("Anne" "is" "nice" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "blue" "+"))
All round, furry things are white.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
All furry, smart things are nice.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
triple1
Anne is smart.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "smart" "-")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule1))]
("Anne" "is" "nice" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not nice.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule1))]
("Anne" "is" "nice" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is blue.
True
6
proof
[(((((triple1 ((triple1) -> rule3)) -> rule1) triple1) -> rule4))]
("Anne" "is" "blue" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not blue.
False
6
inv-proof
[(((((triple1 ((triple1) -> rule3)) -> rule1) triple1) -> rule4))]
("Anne" "is" "blue" "-")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is white.[(triple1)] @1: Anne is smart.[(((triple1) -> rule3))] @2: Anne is nice.[(((triple1 ((triple1) -> rule3)) -> rule1))] @3: Anne is blue.[(((((triple1 ((triple1) -> rule3)) -> rule1) triple1) -> rule4))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3