Anne is young. Dave is furry. Erin is kind. If something is rough then it is white. If Dave is furry then Dave is rough. If Dave is white then Dave is rough. If something is kind and white then it is round. All round, kind things are rough. All smart things are young.
Anne is young.
("Anne" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
If something is rough then it is white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If Dave is furry then Dave is rough.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "rough" "+"))
If Dave is white then Dave is rough.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "rough" "+"))
If something is kind and white then it is round.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
All round, kind things are rough.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Erin is kind.
True
1
proof
[(triple3)]
("Erin" "is" "kind" "+")
triple3
Erin is not kind.
False
1
inv-proof
[(triple3)]
("Erin" "is" "kind" "-")
triple3
Dave is rough.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "rough" "-")
((triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Dave" "is" "white" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not white.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Dave" "is" "white" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "young" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "round" "+")
Erin is not white.
Unknown
inv-rconc
[@3: Erin is white.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule4 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Anne is young.[(triple1)] Dave is furry.[(triple2)] Erin is kind.[(triple3)] @1: Dave is rough.[(((triple2) -> rule2))] @2: Dave is white.[(((((triple2) -> rule2)) -> rule1))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2