Anne is round. Bob is kind. Gary is green. Kind people are green. All round people are smart. If someone is green and not furry then they are kind. If Anne is not furry then Anne is quiet. All green people are round. If someone is round and not quiet then they are not nice.
Anne is round.
("Anne" "is" "round" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Gary is green.
("Gary" "is" "green" "+")
Kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
All round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If someone is green and not furry then they are kind.
((("someone" "is" "green" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "kind" "+"))
If Anne is not furry then Anne is quiet.
((("Anne" "is" "furry" "~")) -> ("Anne" "is" "quiet" "+"))
All green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone is round and not quiet then they are not nice.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "nice" "-"))
Bob is kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "+")
triple2
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Gary is round.
True
2
proof
[(((triple3) -> rule5))]
("Gary" "is" "round" "+")
((triple3) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is round.
True
3
proof
[(((((triple2) -> rule1)) -> rule5))]
("Bob" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not round.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5))]
("Bob" "is" "round" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
True
4
proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule2))]
("Bob" "is" "smart" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not smart.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule2))]
("Bob" "is" "smart" "-")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "kind" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "kind" "+")
Anne is not green.
Unknown
inv-rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "quiet" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is round.[(triple1)] Bob is kind.[(triple2)] Gary is green.[(triple3)] @1: Anne is smart.[(((triple1) -> rule2))] Bob is green.[(((triple2) -> rule1))] Gary is round.[(((triple3) -> rule5))] @2: Bob is round.[(((((triple2) -> rule1)) -> rule5))] Gary is smart.[(((((triple3) -> rule5)) -> rule2))] @3: Bob is smart.[(((((((triple2) -> rule1)) -> rule5)) -> rule2))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple3) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3