Charlie is furry. Gary is kind. Gary is nice. Smart things are quiet. If something is nice and young then it is smart. If Gary is quiet and Gary is nice then Gary is kind. Quiet things are smart. All furry, smart things are big. All furry things are quiet. If something is furry and smart then it is quiet. If something is smart and nice then it is kind.
Charlie is furry.
("Charlie" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is nice and young then it is smart.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If Gary is quiet and Gary is nice then Gary is kind.
((("Gary" "is" "quiet" "+") ("Gary" "is" "nice" "+")) -> ("Gary" "is" "kind" "+"))
Quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
All furry, smart things are big.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
All furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is furry and smart then it is quiet.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is smart and nice then it is kind.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Gary is nice.
True
1
proof
[(triple3)]
("Gary" "is" "nice" "+")
triple3
Gary is not nice.
False
1
inv-proof
[(triple3)]
("Gary" "is" "nice" "-")
triple3
Charlie is quiet.
True
2
proof
[(((triple1) -> rule6))]
("Charlie" "is" "quiet" "+")
((triple1) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule6))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
True
3
proof
[(((((triple1) -> rule6)) -> rule4))]
("Charlie" "is" "smart" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not smart.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule4))]
("Charlie" "is" "smart" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
True
5
proof
[(((triple1 ((((triple1) -> rule6)) -> rule4)) -> rule5))]
("Charlie" "is" "big" "+")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is not big.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule6)) -> rule4)) -> rule5))]
("Charlie" "is" "big" "-")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Gary is not quiet.
Unknown
inv-rconc
[@3: Gary is quiet.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule6 <- FAIL)]]
("Gary" "is" "quiet" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "kind" "+")
Gary is not smart.
Unknown
inv-rconc
[@3: Gary is smart.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule2 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "big" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Charlie is furry.[(triple1)] Gary is kind.[(triple2)] Gary is nice.[(triple3)] @1: Charlie is quiet.[(((triple1) -> rule6))] @2: Charlie is smart.[(((((triple1) -> rule6)) -> rule4))] @3: Charlie is big.[(((triple1 ((((triple1) -> rule6)) -> rule4)) -> rule5))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3