Anne is not young. Gary is furry. Furry things are young. All kind things are smart. Young things are furry. If something is kind and furry then it is quiet. Young things are kind. If something is young and furry then it is not cold.
Anne is not young.
("Anne" "is" "young" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
All kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If something is kind and furry then it is quiet.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something is young and furry then it is not cold.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "-"))
Gary is furry.
True
1
proof
[(triple2)]
("Gary" "is" "furry" "+")
triple2
Anne is young.
False
1
inv-proof
[(triple1)]
("Anne" "is" "young" "+")
triple1
Gary is young.
True
2
proof
[(((triple2) -> rule1))]
("Gary" "is" "young" "+")
((triple2) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple2) -> rule1))]
("Gary" "is" "young" "-")
((triple2) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not cold.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule6))]
("Gary" "is" "cold" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule6 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule6))]
("Gary" "is" "cold" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule6 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
True
4
proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule2))]
("Gary" "is" "smart" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is not smart.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule2))]
("Gary" "is" "smart" "-")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Anne is not smart.
Unknown
inv-rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "kind" "+")
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is quiet.
Unknown
rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Anne is not young.[(triple1)] Gary is furry.[(triple2)] @1: Gary is young.[(((triple2) -> rule1))] @2: Gary is kind.[(((((triple2) -> rule1)) -> rule5))] Gary is not cold.[(((((triple2) -> rule1) triple2) -> rule6))] @3: Gary is quiet.[(((((((triple2) -> rule1)) -> rule5) triple2) -> rule4))] Gary is smart.[(((((((triple2) -> rule1)) -> rule5)) -> rule2))]
Anne is not young.
("Anne" "is" "young" "-")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
((triple2) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not cold.
("Gary" "is" "cold" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule6 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2)) triple2) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3