Anne is quiet. Bob is furry. Dave is nice. Gary is nice. Nice things are quiet. All young, furry things are cold. Quiet things are furry. All nice, quiet things are rough. If something is quiet then it is young. If Bob is nice then Bob is rough.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
All young, furry things are cold.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All nice, quiet things are rough.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is quiet then it is young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If Bob is nice then Bob is rough.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "rough" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Dave is not nice.
False
1
inv-proof
[(triple3)]
("Dave" "is" "nice" "-")
triple3
Gary is quiet.
True
2
proof
[(((triple4) -> rule1))]
("Gary" "is" "quiet" "+")
((triple4) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "furry" "-")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
True
5
proof
[(((((triple1) -> rule5) ((triple1) -> rule3)) -> rule2))]
("Anne" "is" "cold" "+")
((((triple1) -> (rule5 % int3)) ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Gary is not furry.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule3))]
("Gary" "is" "furry" "-")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Dave is cold.
True
7
proof
[(((((((triple3) -> rule1)) -> rule5) ((((triple3) -> rule1)) -> rule3)) -> rule2))]
("Dave" "is" "cold" "+")
((((((triple3) -> (rule1 % int4))) -> (rule5 % int3)) ((((triple3) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is not cold.
False
7
inv-proof
[(((((((triple3) -> rule1)) -> rule5) ((((triple3) -> rule1)) -> rule3)) -> rule2))]
("Dave" "is" "cold" "-")
((((((triple3) -> (rule1 % int4))) -> (rule5 % int3)) ((((triple3) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Bob is not cold.
Unknown
inv-rconc
[@3: Bob is cold.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule1 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "quiet" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Anne is quiet.[(triple1)] Bob is furry.[(triple2)] Dave is nice.[(triple3)] Gary is nice.[(triple4)] @1: Anne is furry.[(((triple1) -> rule3))] Anne is young.[(((triple1) -> rule5))] Dave is quiet.[(((triple3) -> rule1))] Gary is quiet.[(((triple4) -> rule1))] @2: Anne is cold.[(((((triple1) -> rule5) ((triple1) -> rule3)) -> rule2))] Dave is furry.[(((((triple3) -> rule1)) -> rule3))] Dave is rough.[(((triple3 ((triple3) -> rule1)) -> rule4))] Dave is young.[(((((triple3) -> rule1)) -> rule5))] Gary is furry.[(((((triple4) -> rule1)) -> rule3))] Gary is rough.[(((triple4 ((triple4) -> rule1)) -> rule4))] Gary is young.[(((((triple4) -> rule1)) -> rule5))] @3: Dave is cold.[(((((((triple3) -> rule1)) -> rule5) ((((triple3) -> rule1)) -> rule3)) -> rule2))] Gary is cold.[(((((((triple4) -> rule1)) -> rule5) ((((triple4) -> rule1)) -> rule3)) -> rule2))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple4) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule5 % int3)) ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple3) -> (rule1 % int4))) -> (rule5 % int3)) ((((triple3) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple4) -> (rule1 % int4))) -> (rule5 % int3)) ((((triple4) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4