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