Anne is red. Bob is round. Charlie is red. Gary is round. Round people are white. If someone is young and red then they are white. All young, white people are not quiet. If someone is red and not round then they are young. If someone is round then they are young. If someone is cold and not red then they are not young. Cold, round people are not furry. If someone is white and not quiet then they are furry.
Anne is red.
("Anne" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If someone is young and red then they are white.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
All young, white people are not quiet.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "-"))
If someone is red and not round then they are young.
((("someone" "is" "red" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "young" "+"))
If someone is round then they are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is cold and not red then they are not young.
((("someone" "is" "cold" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "young" "-"))
Cold, round people are not furry.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "-"))
If someone is white and not quiet then they are furry.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "furry" "+"))
Gary is round.
True
1
proof
[(triple4)]
("Gary" "is" "round" "+")
triple4
Charlie is not red.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "red" "-")
triple3
Gary is white.
True
2
proof
[(((triple4) -> rule1))]
("Gary" "is" "white" "+")
((triple4) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple4) -> rule1))]
("Gary" "is" "white" "-")
((triple4) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not quiet.
True
5
proof
[(((((triple4) -> rule5) ((triple4) -> rule1)) -> rule3))]
("Gary" "is" "quiet" "-")
((((triple4) -> (rule5 % int3)) ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is quiet.
False
5
inv-proof
[(((((triple4) -> rule5) ((triple4) -> rule1)) -> rule3))]
("Gary" "is" "quiet" "+")
((((triple4) -> (rule5 % int3)) ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is furry.
True
8
proof
[(((((triple4) -> rule1) ((((triple4) -> rule5) ((triple4) -> rule1)) -> rule3)) -> rule8))]
("Gary" "is" "furry" "+")
((((triple4) -> (rule1 % int4)) ((((triple4) -> (rule5 % int3)) ((triple4) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is not furry.
False
8
inv-proof
[(((((triple4) -> rule1) ((((triple4) -> rule5) ((triple4) -> rule1)) -> rule3)) -> rule8))]
("Gary" "is" "furry" "-")
((((triple4) -> (rule1 % int4)) ((((triple4) -> (rule5 % int3)) ((triple4) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "furry" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "furry" "+")
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "young" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "young" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Anne is red.[(triple1)] Bob is round.[(triple2)] Charlie is red.[(triple3)] Gary is round.[(triple4)] @1: Bob is white.[(((triple2) -> rule1))] Bob is young.[(((triple2) -> rule5))] Gary is white.[(((triple4) -> rule1))] Gary is young.[(((triple4) -> rule5))] @2: Bob is not quiet.[(((((triple2) -> rule5) ((triple2) -> rule1)) -> rule3))] Gary is not quiet.[(((((triple4) -> rule5) ((triple4) -> rule1)) -> rule3))] @3: Bob is furry.[(((((triple2) -> rule1) ((((triple2) -> rule5) ((triple2) -> rule1)) -> rule3)) -> rule8))] Gary is furry.[(((((triple4) -> rule1) ((((triple4) -> rule5) ((triple4) -> rule1)) -> rule3)) -> rule8))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
((triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple2) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple4) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple4) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Bob is not quiet.
("Bob" "is" "quiet" "-")
((((triple2) -> (rule5 % int3)) ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Gary is not quiet.
("Gary" "is" "quiet" "-")
((((triple4) -> (rule5 % int3)) ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2) -> (rule1 % int4)) ((((triple2) -> (rule5 % int3)) ((triple2) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not quiet.
("Bob" "is" "quiet" "-")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
((((triple4) -> (rule1 % int4)) ((((triple4) -> (rule5 % int3)) ((triple4) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4