Charlie is cold. Erin is young. Harry is red. If Erin is nice then Erin is red. Kind, red people are not nice. If Erin is kind then Erin is not cold. Cold people are young. All cold people are kind. If someone is young and not white then they are not kind. All kind, cold people are red. If someone is young and not kind then they are round.
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is red.
("Harry" "is" "red" "+")
If Erin is nice then Erin is red.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "red" "+"))
Kind, red people are not nice.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "-"))
If Erin is kind then Erin is not cold.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "cold" "-"))
Cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is young and not white then they are not kind.
((("someone" "is" "young" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "kind" "-"))
All kind, cold people are red.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is young and not kind then they are round.
((("someone" "is" "young" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "round" "+"))
Charlie is cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Harry is not red.
False
1
inv-proof
[(triple3)]
("Harry" "is" "red" "-")
triple3
Charlie is kind.
True
2
proof
[(((triple1) -> rule5))]
("Charlie" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple1) -> rule4))]
("Charlie" "is" "young" "-")
((triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
True
4
proof
[(((((triple1) -> rule5) triple1) -> rule7))]
("Charlie" "is" "red" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not red.
False
4
inv-proof
[(((((triple1) -> rule5) triple1) -> rule7))]
("Charlie" "is" "red" "-")
((((triple1) -> (rule5 % int2)) triple1) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not nice.
True
7
proof
[(((((triple1) -> rule5) ((((triple1) -> rule5) triple1) -> rule7)) -> rule2))]
("Charlie" "is" "nice" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3)) triple1) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is nice.
False
7
inv-proof
[(((((triple1) -> rule5) ((((triple1) -> rule5) triple1) -> rule7)) -> rule2))]
("Charlie" "is" "nice" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3)) triple1) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "round" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "round" "+")
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "red" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "kind" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Charlie is cold.[(triple1)] Erin is young.[(triple2)] Harry is red.[(triple3)] @1: Charlie is kind.[(((triple1) -> rule5))] Charlie is young.[(((triple1) -> rule4))] @2: Charlie is red.[(((((triple1) -> rule5) triple1) -> rule7))] @3: Charlie is not nice.[(((((triple1) -> rule5) ((((triple1) -> rule5) triple1) -> rule7)) -> rule2))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Erin is young.
("Erin" "is" "young" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not nice.
("Charlie" "is" "nice" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3)) triple1) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3