Anne is kind. Anne is white. Charlie is not kind. All furry, nice things are white. If Anne is green then Anne is kind. All nice, green things are blue. If something is round and nice then it is not blue. All round, furry things are green. All white things are green. If something is green then it is nice. If something is round and not nice then it is kind.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
All furry, nice things are white.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If Anne is green then Anne is kind.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "kind" "+"))
All nice, green things are blue.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something is round and nice then it is not blue.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "-"))
All round, furry things are green.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All white things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is green then it is nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is round and not nice then it is kind.
((("something" "is" "round" "+") ("something" "is" "nice" "~")) -> ("something" "is" "kind" "+"))
Anne is white.
True
1
proof
[(triple2)]
("Anne" "is" "white" "+")
triple2
Anne is not white.
False
1
inv-proof
[(triple2)]
("Anne" "is" "white" "-")
triple2
Anne is green.
True
2
proof
[(((triple2) -> rule6))]
("Anne" "is" "green" "+")
((triple2) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple2) -> rule6))]
("Anne" "is" "green" "-")
((triple2) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
True
3
proof
[(((((triple2) -> rule6)) -> rule7))]
("Anne" "is" "nice" "+")
((((triple2) -> (rule6 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not nice.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule7))]
("Anne" "is" "nice" "-")
((((triple2) -> (rule6 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is blue.
True
6
proof
[(((((((triple2) -> rule6)) -> rule7) ((triple2) -> rule6)) -> rule3))]
("Anne" "is" "blue" "+")
((((((triple2) -> (rule6 % int3))) -> (rule7 % int2)) ((triple2) -> (rule6 % int3))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not blue.
False
6
inv-proof
[(((((((triple2) -> rule6)) -> rule7) ((triple2) -> rule6)) -> rule3))]
("Anne" "is" "blue" "-")
((((((triple2) -> (rule6 % int3))) -> (rule7 % int2)) ((triple2) -> (rule6 % int3))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Charlie is not blue.
Unknown
inv-rconc
[@3: Charlie is blue.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not nice.
Unknown
inv-rconc
[@3: Charlie is nice.[CWA. Example of deepest failure = (rule7 <- rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is green.
Unknown
rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "green" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Anne is kind.[(triple1 OR ((((triple2) -> rule6)) -> rule2))] Anne is white.[(triple2)] Charlie is not kind.[(triple3)] @1: Anne is green.[(((triple2) -> rule6))] @2: Anne is nice.[(((((triple2) -> rule6)) -> rule7))] @3: Anne is blue.[(((((((triple2) -> rule6)) -> rule7) ((triple2) -> rule6)) -> rule3))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple2
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple3
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2) -> (rule6 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((((triple2) -> (rule6 % int3))) -> (rule7 % int2)) ((triple2) -> (rule6 % int3))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3