Anne is nice. Bob is not quiet. Charlie is nice. Gary is quiet. If something is quiet then it is kind. If Gary is kind then Gary is big.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If something is quiet then it is kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If Gary is kind then Gary is big.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "big" "+"))
Gary is quiet.
True
1
proof
[(triple4)]
("Gary" "is" "quiet" "+")
triple4
Charlie is not nice.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "nice" "-")
triple3
Gary is kind.
True
2
proof
[(((triple4) -> rule1))]
("Gary" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple4) -> rule1))]
("Gary" "is" "kind" "-")
((triple4) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("Gary" "is" "big" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("Gary" "is" "big" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "kind" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "kind" "+")
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Bob is not quiet.[(triple2)] Charlie is nice.[(triple3)] Gary is quiet.[(triple4)] @1: Gary is kind.[(((triple4) -> rule1))] @2: Gary is big.[(((((triple4) -> rule1)) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Gary is kind.
("Gary" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2