Bob is rough. Bob is white. Erin is furry. Erin is red. Erin is rough. Erin is smart. Erin is white. If something is white then it is rough. Rough things are furry. All rough things are kind.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
If something is white then it is rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
Rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
All rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Erin is rough.
True
1
proof
[(triple5 OR ((triple7) -> rule1))]
("Erin" "is" "rough" "+")
triple5
((triple7) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not red.
False
1
inv-proof
[(triple4)]
("Erin" "is" "red" "-")
triple4
Erin is kind.
True
2
proof
[(((triple5) -> rule3) OR ((((triple7) -> rule1)) -> rule3))]
("Erin" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not kind.
False
2
inv-proof
[(((triple5) -> rule3) OR ((((triple7) -> rule1)) -> rule3))]
("Erin" "is" "kind" "-")
((triple5) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is rough.[(triple1 OR ((triple2) -> rule1))] Bob is white.[(triple2)] Erin is furry.[(triple3 OR ((triple5) -> rule2) OR ((((triple7) -> rule1)) -> rule2))] Erin is red.[(triple4)] Erin is rough.[(triple5 OR ((triple7) -> rule1))] Erin is smart.[(triple6)] Erin is white.[(triple7)] @1: Bob is furry.[(((triple1) -> rule2) OR ((((triple2) -> rule1)) -> rule2))] Bob is kind.[(((triple1) -> rule3) OR ((((triple2) -> rule1)) -> rule3))] Erin is kind.[(((triple5) -> rule3) OR ((((triple7) -> rule1)) -> rule3))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
((triple2) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
((triple5) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
((triple7) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2