Erin is blue. Erin is cold. Erin is red. If someone is white then they are red. Smart, young people are kind. All smart people are kind. If Erin is smart and Erin is red then Erin is cold. Blue people are smart. All cold people are blue.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
If someone is white then they are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Smart, young people are kind.
((("someone" "is" "smart" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
All smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If Erin is smart and Erin is red then Erin is cold.
((("Erin" "is" "smart" "+") ("Erin" "is" "red" "+")) -> ("Erin" "is" "cold" "+"))
Blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
All cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Erin is cold.
True
1
proof
[(triple2 OR ((((triple1) -> rule5) triple3) -> rule4))]
("Erin" "is" "cold" "+")
triple2
((((triple1) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not red.
False
1
inv-proof
[(triple3)]
("Erin" "is" "red" "-")
triple3
Erin is smart.
True
2
proof
[(((triple1) -> rule5) OR ((((triple2) -> rule6)) -> rule5))]
("Erin" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not smart.
False
2
inv-proof
[(((triple1) -> rule5) OR ((((triple2) -> rule6)) -> rule5))]
("Erin" "is" "smart" "-")
((triple1) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
True
3
proof
[(((((triple1) -> rule5)) -> rule3) OR ((((((triple2) -> rule6)) -> rule5)) -> rule3))]
("Erin" "is" "kind" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not kind.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3) OR ((((((triple2) -> rule6)) -> rule5)) -> rule3))]
("Erin" "is" "kind" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Erin is blue.[(triple1 OR ((triple2) -> rule6))] Erin is cold.[(triple2 OR ((((triple1) -> rule5) triple3) -> rule4))] Erin is red.[(triple3)] @1: Erin is smart.[(((triple1) -> rule5) OR ((((triple2) -> rule6)) -> rule5))] @2: Erin is kind.[(((((triple1) -> rule5)) -> rule3) OR ((((((triple2) -> rule6)) -> rule5)) -> rule3))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((triple2) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((((triple1) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3