Anne is blue. Bob is cold. Dave is cold. Dave is furry. Dave is quiet. Dave is rough. Dave is white. Harry is cold. Harry is rough. Harry is white. If something is quiet then it is rough. If something is rough and round then it is blue. If Harry is rough and Harry is blue then Harry is white. If something is cold then it is quiet. If something is white and quiet then it is round. Furry, white things are blue. All quiet, white things are cold. If Bob is furry then Bob is blue.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is rough and round then it is blue.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If Harry is rough and Harry is blue then Harry is white.
((("Harry" "is" "rough" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "white" "+"))
If something is cold then it is quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If something is white and quiet then it is round.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
Furry, white things are blue.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
All quiet, white things are cold.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If Bob is furry then Bob is blue.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "blue" "+"))
Dave is furry.
True
1
proof
[(triple4)]
("Dave" "is" "furry" "+")
triple4
Harry is not rough.
False
1
inv-proof
[(triple9 OR ((((triple8) -> rule4)) -> rule1))]
("Harry" "is" "rough" "-")
triple9
((((triple8) -> (rule4 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Bob is quiet.
True
2
proof
[(((triple2) -> rule4))]
("Bob" "is" "quiet" "+")
((triple2) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple2) -> rule4))]
("Bob" "is" "quiet" "-")
((triple2) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
True
3
proof
[(((((triple2) -> rule4)) -> rule1))]
("Bob" "is" "rough" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not rough.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule1))]
("Bob" "is" "rough" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Harry is blue.
True
6
proof
[(((triple9 ((triple10 ((triple8) -> rule4)) -> rule5)) -> rule2) OR ((((((triple8) -> rule4)) -> rule1) ((triple10 ((triple8) -> rule4)) -> rule5)) -> rule2))]
("Harry" "is" "blue" "+")
((triple9 ((triple10 ((triple8) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple8) -> (rule4 % int4))) -> (rule1 % int3)) ((triple10 ((triple8) -> (rule4 % int4))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is not blue.
False
6
inv-proof
[(((triple9 ((triple10 ((triple8) -> rule4)) -> rule5)) -> rule2) OR ((((((triple8) -> rule4)) -> rule1) ((triple10 ((triple8) -> rule4)) -> rule5)) -> rule2))]
("Harry" "is" "blue" "-")
((triple9 ((triple10 ((triple8) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple8) -> (rule4 % int4))) -> (rule1 % int3)) ((triple10 ((triple8) -> (rule4 % int4))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "round" "-")
Anne is cold.
Unknown
rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "cold" "+")
Anne is not quiet.
Unknown
inv-rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is rough.
Unknown
rconc
[@3: Anne is rough.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule7 <- FAIL)]]
("Anne" "is" "rough" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is blue.[(triple1)] Bob is cold.[(triple2)] Dave is cold.[(triple3 OR ((triple5 triple7) -> rule7))] Dave is furry.[(triple4)] Dave is quiet.[(triple5 OR ((triple3) -> rule4))] Dave is rough.[(triple6 OR ((triple5) -> rule1) OR ((((triple3) -> rule4)) -> rule1))] Dave is white.[(triple7)] Harry is cold.[(triple8)] Harry is rough.[(triple9 OR ((((triple8) -> rule4)) -> rule1))] Harry is white.[(triple10)] @1: Bob is quiet.[(((triple2) -> rule4))] Dave is blue.[(((triple4 triple7) -> rule6) OR ((triple6 ((triple7 triple5) -> rule5)) -> rule2) OR ((((triple5) -> rule1) ((triple7 triple5) -> rule5)) -> rule2) OR ((triple6 ((triple7 ((triple3) -> rule4)) -> rule5)) -> rule2) OR ((((triple5) -> rule1) ((triple7 ((triple3) -> rule4)) -> rule5)) -> rule2) OR ((((((triple3) -> rule4)) -> rule1) ((triple7 triple5) -> rule5)) -> rule2) OR ((((((triple3) -> rule4)) -> rule1) ((triple7 ((triple3) -> rule4)) -> rule5)) -> rule2))] Dave is round.[(((triple7 triple5) -> rule5) OR ((triple7 ((triple3) -> rule4)) -> rule5))] Harry is quiet.[(((triple8) -> rule4))] @2: Bob is rough.[(((((triple2) -> rule4)) -> rule1))] Harry is round.[(((triple10 ((triple8) -> rule4)) -> rule5))] @3: Harry is blue.[(((triple9 ((triple10 ((triple8) -> rule4)) -> rule5)) -> rule2) OR ((((((triple8) -> rule4)) -> rule1) ((triple10 ((triple8) -> rule4)) -> rule5)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
((triple5 triple7) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
((triple3) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple6
((triple5) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple9
((((triple8) -> (rule4 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
triple10
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple4 triple7) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple6 ((triple7 triple5) -> (rule5 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple7 triple5) -> (rule5 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((triple6 ((triple7 ((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((triple5) -> (rule1 % int4)) ((triple7 ((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((((triple3) -> (rule4 % int4))) -> (rule1 % int3)) ((triple7 triple5) -> (rule5 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
((((((triple3) -> (rule4 % int4))) -> (rule1 % int3)) ((triple7 ((triple3) -> (rule4 % int4))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
((triple7 triple5) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple7 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple8) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple10 ((triple8) -> (rule4 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((triple9 ((triple10 ((triple8) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple8) -> (rule4 % int4))) -> (rule1 % int3)) ((triple10 ((triple8) -> (rule4 % int4))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4