Charlie is furry. Charlie is green. Charlie is smart. All smart things are not young. Furry things are smart. Rough things are cold. All quiet, smart things are rough. If something is young and cold then it is green. If Charlie is not furry then Charlie is green. If Charlie is cold then Charlie is green. If something is green and not young then it is not quiet.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
All smart things are not young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "-"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
All quiet, smart things are rough.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is young and cold then it is green.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If Charlie is not furry then Charlie is green.
((("Charlie" "is" "furry" "~")) -> ("Charlie" "is" "green" "+"))
If Charlie is cold then Charlie is green.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "green" "+"))
If something is green and not young then it is not quiet.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "is" "quiet" "-"))
Charlie is smart.
True
1
proof
[(triple3 OR ((triple1) -> rule2))]
("Charlie" "is" "smart" "+")
triple3
((triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not furry.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "furry" "-")
triple1
Charlie is not young.
True
2
proof
[(((triple3) -> rule1) OR ((((triple1) -> rule2)) -> rule1))]
("Charlie" "is" "young" "-")
((triple3) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
False
2
inv-proof
[(((triple3) -> rule1) OR ((((triple1) -> rule2)) -> rule1))]
("Charlie" "is" "young" "+")
((triple3) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not quiet.
True
4
proof
[(((triple2 ((triple3) -> rule1)) -> rule8) OR ((triple2 ((((triple1) -> rule2)) -> rule1)) -> rule8))]
("Charlie" "is" "quiet" "-")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
int2
((triple2 ((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is quiet.
False
4
inv-proof
[(((triple2 ((triple3) -> rule1)) -> rule8) OR ((triple2 ((((triple1) -> rule2)) -> rule1)) -> rule8))]
("Charlie" "is" "quiet" "+")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
int2
((triple2 ((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not cold.
Unknown
inv-rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is furry.[(triple1)] Charlie is green.[(triple2)] Charlie is smart.[(triple3 OR ((triple1) -> rule2))] @1: Charlie is not young.[(((triple3) -> rule1) OR ((((triple1) -> rule2)) -> rule1))] @2: Charlie is not quiet.[(((triple2 ((triple3) -> rule1)) -> rule8) OR ((triple2 ((((triple1) -> rule2)) -> rule1)) -> rule8))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
((triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
((triple3) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
int2
((triple2 ((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3