Anne is kind. Bob is furry. Dave is young. Erin is rough. Furry, green things are smart. All rough things are furry. All furry things are kind. All big things are rough. All smart, big things are young. All rough things are kind.
Anne is kind.
("Anne" "is" "kind" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Furry, green things are smart.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
All rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
All furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
All big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
All smart, big things are young.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
All rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Erin is rough.
True
1
proof
[(triple4)]
("Erin" "is" "rough" "+")
triple4
Dave is not young.
False
1
inv-proof
[(triple3)]
("Dave" "is" "young" "-")
triple3
Erin is kind.
True
2
proof
[(((triple4) -> rule6) OR ((((triple4) -> rule2)) -> rule3))]
("Erin" "is" "kind" "+")
((triple4) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not kind.
False
2
inv-proof
[(((triple4) -> rule6) OR ((((triple4) -> rule2)) -> rule3))]
("Erin" "is" "kind" "-")
((triple4) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "smart" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "young" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Anne is kind.[(triple1)] Bob is furry.[(triple2)] Dave is young.[(triple3)] Erin is rough.[(triple4)] @1: Bob is kind.[(((triple2) -> rule3))] Erin is furry.[(((triple4) -> rule2))] Erin is kind.[(((triple4) -> rule6) OR ((((triple4) -> rule2)) -> rule3))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple4) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple4) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2