Anne is blue. Anne is smart. Bob is blue. Bob is quiet. Gary is furry. Gary is smart. Gary is white. All quiet people are round. All round people are not young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
All quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
All round people are not young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "-"))
Bob is quiet.
True
1
proof
[(triple4)]
("Bob" "is" "quiet" "+")
triple4
Bob is not quiet.
False
1
inv-proof
[(triple4)]
("Bob" "is" "quiet" "-")
triple4
Bob is round.
True
2
proof
[(((triple4) -> rule1))]
("Bob" "is" "round" "+")
((triple4) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple4) -> rule1))]
("Bob" "is" "round" "-")
((triple4) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not young.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("Bob" "is" "young" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("Bob" "is" "young" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "round" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is blue.[(triple1)] Anne is smart.[(triple2)] Bob is blue.[(triple3)] Bob is quiet.[(triple4)] Gary is furry.[(triple5)] Gary is smart.[(triple6)] Gary is white.[(triple7)] @1: Bob is round.[(((triple4) -> rule1))] @2: Bob is not young.[(((((triple4) -> rule1)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
Bob is round.
("Bob" "is" "round" "+")
((triple4) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not young.
("Bob" "is" "young" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2