Anne is quiet. Bob is nice. Charlie is furry. If someone is quiet then they are round. If someone is quiet then they are big. Round people are blue.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
If someone is quiet then they are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is quiet then they are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Anne is round.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "big" "-")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not blue.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "round" "-")
Bob is round.
Unknown
rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "round" "+")
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "big" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Anne is quiet.[(triple1)] Bob is nice.[(triple2)] Charlie is furry.[(triple3)] @1: Anne is big.[(((triple1) -> rule2))] Anne is round.[(((triple1) -> rule1))] @2: Anne is blue.[(((((triple1) -> rule1)) -> rule3))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2