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