Erin is rough. Erin is white. Erin is young. All white things are furry. If Erin is smart and Erin is young then Erin is white. Quiet things are furry. All white things are red. If something is rough then it is furry. If something is young and rough then it is white.
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
All white things are furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If Erin is smart and Erin is young then Erin is white.
((("Erin" "is" "smart" "+") ("Erin" "is" "young" "+")) -> ("Erin" "is" "white" "+"))
Quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All white things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If something is rough then it is furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
If something is young and rough then it is white.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Erin is white.
True
1
proof
[(triple2 OR ((triple3 triple1) -> rule6))]
("Erin" "is" "white" "+")
triple2
((triple3 triple1) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not young.
False
1
inv-proof
[(triple3)]
("Erin" "is" "young" "-")
triple3
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Erin is rough.[(triple1)] Erin is white.[(triple2 OR ((triple3 triple1) -> rule6))] Erin is young.[(triple3)] @1: Erin is furry.[(((triple1) -> rule5) OR ((triple2) -> rule1) OR ((((triple3 triple1) -> rule6)) -> rule1))] Erin is red.[(((triple2) -> rule4) OR ((((triple3 triple1) -> rule6)) -> rule4))]
Erin is rough.
("Erin" "is" "rough" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
((triple3 triple1) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple2) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple3 triple1) -> (rule6 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((triple2) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple3 triple1) -> (rule6 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2