Anne is blue. Dave is green. Fiona is round. Harry is kind. All furry people are kind. If Dave is white and Dave is blue then Dave is round. If Anne is blue and Anne is round then Anne is not green. All blue people are green. Green people are furry. If Harry is not green then Harry is not big. If someone is furry then they are not big. If someone is green and not round then they are big.
Anne is blue.
("Anne" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If Dave is white and Dave is blue then Dave is round.
((("Dave" "is" "white" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "round" "+"))
If Anne is blue and Anne is round then Anne is not green.
((("Anne" "is" "blue" "+") ("Anne" "is" "round" "+")) -> ("Anne" "is" "green" "-"))
All blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If Harry is not green then Harry is not big.
((("Harry" "is" "green" "~")) -> ("Harry" "is" "big" "-"))
If someone is furry then they are not big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "-"))
If someone is green and not round then they are big.
((("someone" "is" "green" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "big" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Fiona is not round.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "round" "-")
triple3
Anne is green.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "green" "+")
((triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple2) -> rule5))]
("Dave" "is" "furry" "-")
((triple2) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("Dave" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not big.
True
4
proof
[(((((((triple1) -> rule4)) -> rule5)) -> rule7))]
("Anne" "is" "big" "-")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not kind.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule5)) -> rule1))]
("Anne" "is" "kind" "-")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Fiona is not furry.
Unknown
inv-rconc
[@2: Fiona is furry.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Fiona" "is" "furry" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "green" "+")
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "green" "-")
Fiona is kind.
Unknown
rconc
[@3: Fiona is kind.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule4 <- FAIL)]]
("Fiona" "is" "kind" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is blue.[(triple1)] Dave is green.[(triple2)] Fiona is round.[(triple3)] Harry is kind.[(triple4)] @1: Anne is green.[(((triple1) -> rule4))] Dave is furry.[(((triple2) -> rule5))] @2: Anne is furry.[(((((triple1) -> rule4)) -> rule5))] Dave is kind.[(((((triple2) -> rule5)) -> rule1))] Dave is not big.[(((((triple2) -> rule5)) -> rule7))] @3: Anne is kind.[(((((((triple1) -> rule4)) -> rule5)) -> rule1))] Anne is not big.[(((((((triple1) -> rule4)) -> rule5)) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not big.
("Dave" "is" "big" "-")
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not big.
("Anne" "is" "big" "-")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3