Anne is nice. Charlie is furry. Gary is rough. If something is big and nice then it is not rough. All nice things are rough. Nice things are furry. All big, rough things are not nice. If something is young then it is not big. Furry things are not kind. Young things are smart. If something is rough and not kind then it is smart.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If something is big and nice then it is not rough.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "-"))
All nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
All big, rough things are not nice.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "-"))
If something is young then it is not big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "-"))
Furry things are not kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "-"))
Young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is rough and not kind then it is smart.
((("something" "is" "rough" "+") ("something" "is" "kind" "~")) -> ("something" "is" "smart" "+"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Anne is rough.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "rough" "-")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("Anne" "is" "kind" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is kind.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("Anne" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is smart.
True
6
proof
[(((((triple1) -> rule2) ((((triple1) -> rule3)) -> rule6)) -> rule8))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule2 % int4)) ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not kind.
("Anne" "is" "kind" "-")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is not smart.
False
6
inv-proof
[(((((triple1) -> rule2) ((((triple1) -> rule3)) -> rule6)) -> rule8))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule2 % int4)) ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not kind.
("Anne" "is" "kind" "-")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "furry" "+")
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Anne is nice.[(triple1)] Charlie is furry.[(triple2)] Gary is rough.[(triple3)] @1: Anne is furry.[(((triple1) -> rule3))] Anne is rough.[(((triple1) -> rule2))] Charlie is not kind.[(((triple2) -> rule6))] @2: Anne is not kind.[(((((triple1) -> rule3)) -> rule6))] @3: Anne is smart.[(((((triple1) -> rule2) ((((triple1) -> rule3)) -> rule6)) -> rule8))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Charlie is not kind.
("Charlie" "is" "kind" "-")
((triple2) -> (rule6 % int1))
Charlie is not kind.
("Charlie" "is" "kind" "-")
int1
Anne is not kind.
("Anne" "is" "kind" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule2 % int4)) ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not kind.
("Anne" "is" "kind" "-")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4