Erin is young. If something is nice then it is red. All round things are nice. All young things are nice. If something is nice then it is green. If Erin is young then Erin is nice. If Erin is kind then Erin is nice. Blue, green things are round. All young, kind things are green.
Erin is young.
("Erin" "is" "young" "+")
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
All young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If Erin is young then Erin is nice.
((("Erin" "is" "young" "+")) -> ("Erin" "is" "nice" "+"))
If Erin is kind then Erin is nice.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "nice" "+"))
Blue, green things are round.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
All young, kind things are green.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "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 nice.
True
2
proof
[(((triple1) -> rule3) OR ((triple1) -> rule5))]
("Erin" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple1) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple1) -> rule5))]
("Erin" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple1) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Erin is young.[(triple1)] @1: Erin is nice.[(((triple1) -> rule3) OR ((triple1) -> rule5))] @2: Erin is green.[(((((triple1) -> rule3)) -> rule4) OR ((((triple1) -> rule5)) -> rule4))] Erin is red.[(((((triple1) -> rule3)) -> rule1) OR ((((triple1) -> rule5)) -> rule1))]
Erin is young.
("Erin" "is" "young" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple1) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2