Anne is white. Dave is smart. Gary is blue. All young people are blue. Blue people are cold. Furry, white people are smart. All white people are green. All smart people are young. If someone is young and blue then they are furry.
Anne is white.
("Anne" "is" "white" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
All young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Furry, white people are smart.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
All white people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
All smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
If someone is young and blue then they are furry.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Dave is smart.
True
1
proof
[(triple2)]
("Dave" "is" "smart" "+")
triple2
Gary is not blue.
False
1
inv-proof
[(triple3)]
("Gary" "is" "blue" "-")
triple3
Anne is green.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "green" "+")
((triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "green" "-")
((triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is blue.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("Dave" "is" "blue" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("Dave" "is" "blue" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is furry.
True
6
proof
[(((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule1)) -> rule6))]
("Dave" "is" "furry" "+")
((((triple2) -> (rule5 % int3)) ((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not furry.
False
6
inv-proof
[(((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule1)) -> rule6))]
("Dave" "is" "furry" "-")
((((triple2) -> (rule5 % int3)) ((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Anne is not young.
Unknown
inv-rconc
[@3: Anne is young.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule6 <- FAIL)]]
("Anne" "is" "young" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "green" "+")
Anne is not cold.
Unknown
inv-rconc
[@5: Anne is cold.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule5 <- rule3 <- rule6 <- FAIL)]]
("Anne" "is" "cold" "-")
Gary is furry.
Unknown
rconc
[@3: Gary is furry.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule3 <- FAIL)]]
("Gary" "is" "furry" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Anne is white.[(triple1)] Dave is smart.[(triple2)] Gary is blue.[(triple3)] @1: Anne is green.[(((triple1) -> rule4))] Dave is young.[(((triple2) -> rule5))] Gary is cold.[(((triple3) -> rule2))] @2: Dave is blue.[(((((triple2) -> rule5)) -> rule1))] @3: Dave is cold.[(((((((triple2) -> rule5)) -> rule1)) -> rule2))] Dave is furry.[(((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule1)) -> rule6))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple3) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((((triple2) -> (rule5 % int3)) ((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3