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