Anne is white. Dave is red. Fiona is white. All young people are red. All white people are young. If Dave is blue then Dave is young. All furry, red people are blue. If Dave is furry and Dave is white then Dave is red. Blue, white people are furry.
Anne is white.
("Anne" "is" "white" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is white.
("Fiona" "is" "white" "+")
All young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
All white people are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If Dave is blue then Dave is young.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "young" "+"))
All furry, red people are blue.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If Dave is furry and Dave is white then Dave is red.
((("Dave" "is" "furry" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "red" "+"))
Blue, white people are furry.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Fiona is not white.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "white" "-")
triple3
Fiona is young.
True
2
proof
[(((triple3) -> rule2))]
("Fiona" "is" "young" "+")
((triple3) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "young" "-")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Fiona is not red.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("Fiona" "is" "red" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is blue.
Unknown
rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Dave" "is" "blue" "+")
Fiona is not furry.
Unknown
inv-rconc
[@2: Fiona is furry.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Anne is white.[(triple1)] Dave is red.[(triple2)] Fiona is white.[(triple3)] @1: Anne is young.[(((triple1) -> rule2))] Fiona is young.[(((triple3) -> rule2))] @2: Anne is red.[(((((triple1) -> rule2)) -> rule1))] Fiona is red.[(((((triple3) -> rule2)) -> rule1))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple3) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2