Charlie is nice. Erin is cold. All young people are smart. If someone is smart and nice then they are kind. If someone is nice then they are kind. All smart, cold people are young. Kind people are cold. Smart people are green. If someone is smart then they are nice. If someone is young and not green then they are quiet.
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is cold.
("Erin" "is" "cold" "+")
All young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and nice then they are kind.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is nice then they are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All smart, cold people are young.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If someone is young and not green then they are quiet.
((("someone" "is" "young" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "quiet" "+"))
Erin is cold.
True
1
proof
[(triple2)]
("Erin" "is" "cold" "+")
triple2
Charlie is not nice.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "nice" "-")
triple1
Charlie is kind.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
True
3
proof
[(((((triple1) -> rule3)) -> rule5))]
("Charlie" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not cold.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5))]
("Charlie" "is" "cold" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is green.
Unknown
rconc
[@3: Erin is green.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule4 <- FAIL)]]
("Erin" "is" "green" "+")
@0: Charlie is nice.[(triple1)] Erin is cold.[(triple2)] @1: Charlie is kind.[(((triple1) -> rule3))] @2: Charlie is cold.[(((((triple1) -> rule3)) -> rule5))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2