Charlie is nice. Erin is cold. Erin is white. If Charlie is smart and Charlie is young then Charlie is white. All smart things are red. Smart things are young. All white things are nice. All nice, cold things are young. All young things are quiet. Red, nice things are white. If Charlie is cold then Charlie is smart.
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is white.
("Erin" "is" "white" "+")
If Charlie is smart and Charlie is young then Charlie is white.
((("Charlie" "is" "smart" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "white" "+"))
All smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
All white things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
All nice, cold things are young.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
All young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Red, nice things are white.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If Charlie is cold then Charlie is smart.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "smart" "+"))
Erin is cold.
True
1
proof
[(triple2)]
("Erin" "is" "cold" "+")
triple2
Erin is not cold.
False
1
inv-proof
[(triple2)]
("Erin" "is" "cold" "-")
triple2
Erin is nice.
True
2
proof
[(((triple3) -> rule4))]
("Erin" "is" "nice" "+")
((triple3) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple3) -> rule4))]
("Erin" "is" "nice" "-")
((triple3) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
True
4
proof
[(((((triple3) -> rule4) triple2) -> rule5))]
("Erin" "is" "young" "+")
((((triple3) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not young.
False
4
inv-proof
[(((((triple3) -> rule4) triple2) -> rule5))]
("Erin" "is" "young" "-")
((((triple3) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is quiet.
True
5
proof
[(((((((triple3) -> rule4) triple2) -> rule5)) -> rule6))]
("Erin" "is" "quiet" "+")
((((((triple3) -> (rule4 % int3)) triple2) -> (rule5 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is not quiet.
False
5
inv-proof
[(((((((triple3) -> rule4) triple2) -> rule5)) -> rule6))]
("Erin" "is" "quiet" "-")
((((((triple3) -> (rule4 % int3)) triple2) -> (rule5 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Charlie is not white.
Unknown
inv-rconc
[@3: Charlie is white.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule8 <- FAIL)]]
("Charlie" "is" "white" "-")
Erin is red.
Unknown
rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "red" "+")
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is red.
Unknown
rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("Charlie" "is" "red" "+")
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 nice.[(triple1)] Erin is cold.[(triple2)] Erin is white.[(triple3)] @1: Erin is nice.[(((triple3) -> rule4))] @2: Erin is young.[(((((triple3) -> rule4) triple2) -> rule5))] @3: Erin is quiet.[(((((((triple3) -> rule4) triple2) -> rule5)) -> rule6))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
((triple3) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((((triple3) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple3) -> (rule4 % int3)) triple2) -> (rule5 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3