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