Erin is young. If Erin is kind then Erin is not blue. All smart people are kind. If Erin is blue and Erin is smart then Erin is kind. If someone is young then they are smart. All green, red people are blue. If someone is smart and green then they are blue. If someone is young and kind then they are not cold. All red, smart people are green.
Erin is young.
("Erin" "is" "young" "+")
If Erin is kind then Erin is not blue.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "blue" "-"))
All smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If Erin is blue and Erin is smart then Erin is kind.
((("Erin" "is" "blue" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "kind" "+"))
If someone is young then they are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All green, red people are blue.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart and green then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is young and kind then they are not cold.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "-"))
All red, smart people are green.
((("someone" "is" "red" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Erin is young.
True
1
proof
[(triple1)]
("Erin" "is" "young" "+")
triple1
Erin is not young.
False
1
inv-proof
[(triple1)]
("Erin" "is" "young" "-")
triple1
Erin is smart.
True
2
proof
[(((triple1) -> rule4))]
("Erin" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple1) -> rule4))]
("Erin" "is" "smart" "-")
((triple1) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("Erin" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not kind.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("Erin" "is" "kind" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not cold.
True
5
proof
[(((triple1 ((((triple1) -> rule4)) -> rule2)) -> rule7))]
("Erin" "is" "cold" "-")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is cold.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule4)) -> rule2)) -> rule7))]
("Erin" "is" "cold" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Erin is young.[(triple1)] @1: Erin is smart.[(((triple1) -> rule4))] @2: Erin is kind.[(((((triple1) -> rule4)) -> rule2))] @3: Erin is not blue.[(((((((triple1) -> rule4)) -> rule2)) -> rule1))] Erin is not cold.[(((triple1 ((((triple1) -> rule4)) -> rule2)) -> rule7))]
Erin is young.
("Erin" "is" "young" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not cold.
("Erin" "is" "cold" "-")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3