Anne is cold. Bob is furry. Fiona is young. Gary is smart. All red people are nice. All kind, smart people are not nice. If someone is young then they are red. All cold people are not red. If Anne is cold and Anne is kind then Anne is young. If someone is cold and not nice then they are furry.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
All kind, smart people are not nice.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "-"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
All cold people are not red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "-"))
If Anne is cold and Anne is kind then Anne is young.
((("Anne" "is" "cold" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "young" "+"))
If someone is cold and not nice then they are furry.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "furry" "+"))
Fiona is young.
True
1
proof
[(triple3)]
("Fiona" "is" "young" "+")
triple3
Fiona is not young.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "young" "-")
triple3
Anne is not red.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "red" "-")
((triple1) -> (rule4 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is red.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "red" "+")
((triple1) -> (rule4 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Fiona is nice.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("Fiona" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not nice.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("Fiona" "is" "nice" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "young" "+")
Gary is not nice.
Unknown
inv-rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is cold.[(triple1)] Bob is furry.[(triple2)] Fiona is young.[(triple3)] Gary is smart.[(triple4)] @1: Anne is not red.[(((triple1) -> rule4))] Fiona is red.[(((triple3) -> rule3))] @2: Fiona is nice.[(((((triple3) -> rule3)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Fiona is young.
("Fiona" "is" "young" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
triple4
Anne is not red.
("Anne" "is" "red" "-")
((triple1) -> (rule4 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple3) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2