Anne is green. Bob is green. Charlie is white. White people are smart. If someone is smart and round then they are cold. If Charlie is not green then Charlie is kind. All smart people are round. If someone is smart and cold then they are white. If someone is cold and not kind then they are nice.
Anne is green.
("Anne" "is" "green" "+")
Bob is green.
("Bob" "is" "green" "+")
Charlie is white.
("Charlie" "is" "white" "+")
White people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and round then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is not green then Charlie is kind.
((("Charlie" "is" "green" "~")) -> ("Charlie" "is" "kind" "+"))
All smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If someone is smart and cold then they are white.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is cold and not kind then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "nice" "+"))
Bob is green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "+")
triple2
Bob is not green.
False
1
inv-proof
[(triple2)]
("Bob" "is" "green" "-")
triple2
Charlie is smart.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
True
3
proof
[(((((triple3) -> rule1)) -> rule4))]
("Charlie" "is" "round" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not round.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule4))]
("Charlie" "is" "round" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
True
6
proof
[(((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule4)) -> rule2))]
("Charlie" "is" "cold" "+")
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not cold.
False
6
inv-proof
[(((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule4)) -> rule2))]
("Charlie" "is" "cold" "-")
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Anne is not cold.
Unknown
inv-rconc
[@3: Anne is cold.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule5 <- FAIL)]]
("Anne" "is" "cold" "-")
Bob is cold.
Unknown
rconc
[@3: Bob is cold.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule5 <- FAIL)]]
("Bob" "is" "cold" "+")
Bob is not smart.
Unknown
inv-rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Bob" "is" "smart" "-")
Anne is round.
Unknown
rconc
[@3: Anne is round.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule5 <- FAIL)]]
("Anne" "is" "round" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Anne is green.[(triple1)] Bob is green.[(triple2)] Charlie is white.[(triple3)] @1: Charlie is smart.[(((triple3) -> rule1))] @2: Charlie is round.[(((((triple3) -> rule1)) -> rule4))] @3: Charlie is cold.[(((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule4)) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3