Anne is nice. Anne is round. Charlie is kind. Charlie is red. Charlie is round. Erin is not red. Erin is round. If someone is cold and furry then they are round. Kind, round people are big. Cold people are big. If someone is red and not kind then they are big. Kind people are cold. If Charlie is round then Charlie is red. All cold people are not nice. If someone is kind and not red then they are nice.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is not red.
("Erin" "is" "red" "-")
Erin is round.
("Erin" "is" "round" "+")
If someone is cold and furry then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Kind, round people are big.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
Cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is red and not kind then they are big.
((("someone" "is" "red" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "big" "+"))
Kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is round then Charlie is red.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "red" "+"))
All cold people are not nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "-"))
If someone is kind and not red then they are nice.
((("someone" "is" "kind" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "nice" "+"))
Erin is not red.
True
1
proof
[(triple6)]
("Erin" "is" "red" "-")
triple6
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Charlie is big.
True
3
proof
[(((triple3 triple5) -> rule2) OR ((((triple3) -> rule5)) -> rule3))]
("Charlie" "is" "big" "+")
((triple3 triple5) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not cold.
False
2
inv-proof
[(((triple3) -> rule5))]
("Charlie" "is" "cold" "-")
((triple3) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not nice.
True
3
proof
[(((((triple3) -> rule5)) -> rule7))]
("Charlie" "is" "nice" "-")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule7))]
("Charlie" "is" "nice" "+")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "cold" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "nice" "+")
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is nice.[(triple1)] Anne is round.[(triple2)] Charlie is kind.[(triple3)] Charlie is red.[(triple4 OR ((triple5) -> rule6))] Charlie is round.[(triple5)] Erin is not red.[(triple6)] Erin is round.[(triple7)] @1: Charlie is big.[(((triple3 triple5) -> rule2) OR ((((triple3) -> rule5)) -> rule3))] Charlie is cold.[(((triple3) -> rule5))] @2: Charlie is not nice.[(((((triple3) -> rule5)) -> rule7))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
((triple5) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Erin is not red.
("Erin" "is" "red" "-")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
Charlie is big.
("Charlie" "is" "big" "+")
((triple3 triple5) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not nice.
("Charlie" "is" "nice" "-")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2