Charlie is smart. Erin is nice. If someone is smart then they are red. Cold, smart people are quiet. All round, red people are nice. Red people are round. If someone is cold and not round then they are white. If Erin is not smart and Erin is not quiet then Erin is not nice.
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is nice.
("Erin" "is" "nice" "+")
If someone is smart then they are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Cold, smart people are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
All round, red people are nice.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is cold and not round then they are white.
((("someone" "is" "cold" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "white" "+"))
If Erin is not smart and Erin is not quiet then Erin is not nice.
((("Erin" "is" "smart" "~") ("Erin" "is" "quiet" "~")) -> ("Erin" "is" "nice" "-"))
Erin is nice.
True
1
proof
[(triple2)]
("Erin" "is" "nice" "+")
triple2
Charlie is not smart.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "smart" "-")
triple1
Charlie is red.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "red" "+")
((triple1) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "red" "-")
((triple1) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Charlie" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not round.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Charlie" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is nice.
True
6
proof
[(((((((triple1) -> rule1)) -> rule4) ((triple1) -> rule1)) -> rule3))]
("Charlie" "is" "nice" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is not nice.
False
6
inv-proof
[(((((((triple1) -> rule1)) -> rule4) ((triple1) -> rule1)) -> rule3))]
("Charlie" "is" "nice" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Erin is not round.
Unknown
inv-rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Erin" "is" "round" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "quiet" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Charlie is smart.[(triple1)] Erin is nice.[(triple2)] @1: Charlie is red.[(((triple1) -> rule1))] @2: Charlie is round.[(((((triple1) -> rule1)) -> rule4))] @3: Charlie is nice.[(((((((triple1) -> rule1)) -> rule4) ((triple1) -> rule1)) -> rule3))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3