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