Anne is rough. Bob is kind. Fiona is smart. All cold, round people are smart. Rough, young people are kind. All kind people are white. If Anne is smart and Anne is kind then Anne is cold. All smart people are cold. All white people are smart.
Anne is rough.
("Anne" "is" "rough" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
All cold, round people are smart.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Rough, young people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
All kind people are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If Anne is smart and Anne is kind then Anne is cold.
((("Anne" "is" "smart" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "cold" "+"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
All white people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Fiona is not smart.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "smart" "-")
triple3
Fiona is cold.
True
2
proof
[(((triple3) -> rule5))]
("Fiona" "is" "cold" "+")
((triple3) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "white" "-")
((triple2) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
True
3
proof
[(((((triple2) -> rule3)) -> rule6))]
("Bob" "is" "smart" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule6))]
("Bob" "is" "smart" "-")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Anne is not smart.
Unknown
inv-rconc
[@3: Anne is smart.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule2 <- FAIL)]]
("Anne" "is" "smart" "-")
Fiona is white.
Unknown
rconc
[@2: Fiona is white.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Anne is rough.[(triple1)] Bob is kind.[(triple2)] Fiona is smart.[(triple3)] @1: Bob is white.[(((triple2) -> rule3))] Fiona is cold.[(((triple3) -> rule5))] @2: Bob is smart.[(((((triple2) -> rule3)) -> rule6))] @3: Bob is cold.[(((((((triple2) -> rule3)) -> rule6)) -> rule5))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
((triple2) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple3) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3