Anne is red. Fiona is not cold. Harry is cold. Blue people are nice. If someone is cold and not furry then they are nice. Cold people are nice. Nice, blue people are not green. All nice people are green. Cold people are kind. If someone is blue then they are red. All nice, green people are red.
Anne is red.
("Anne" "is" "red" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold and not furry then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "nice" "+"))
Cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
Nice, blue people are not green.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "-"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue then they are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
All nice, green people are red.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Harry is cold.
True
1
proof
[(triple3)]
("Harry" "is" "cold" "+")
triple3
Fiona is cold.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "cold" "+")
triple2
Harry is kind.
True
2
proof
[(((triple3) -> rule6))]
("Harry" "is" "kind" "+")
((triple3) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple3) -> rule6))]
("Harry" "is" "kind" "-")
((triple3) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
True
3
proof
[(((((triple3) -> rule3)) -> rule5))]
("Harry" "is" "green" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule5))]
("Harry" "is" "green" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is red.
True
6
proof
[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule5)) -> rule8))]
("Harry" "is" "red" "+")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is not red.
False
6
inv-proof
[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule5)) -> rule8))]
("Harry" "is" "red" "-")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Anne is not green.
Unknown
inv-rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Anne" "is" "green" "-")
Fiona is nice.
Unknown
rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "nice" "+")
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "kind" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "kind" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is red.[(triple1)] Fiona is not cold.[(triple2)] Harry is cold.[(triple3)] @1: Harry is kind.[(((triple3) -> rule6))] Harry is nice.[(((triple3) -> rule3))] @2: Harry is green.[(((((triple3) -> rule3)) -> rule5))] @3: Harry is red.[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule5)) -> rule8))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple2
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
((triple3) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3