Anne is smart. Bob is nice. Dave is white. Harry is white. Red, furry things are nice. All red, furry things are white. If something is red and nice then it is furry. All nice things are red. Rough things are nice. If something is white then it is nice.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is white.
("Harry" "is" "white" "+")
Red, furry things are nice.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
All red, furry things are white.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If something is red and nice then it is furry.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
All nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
Rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Bob is nice.
True
1
proof
[(triple2)]
("Bob" "is" "nice" "+")
triple2
Dave is not white.
False
1
inv-proof
[(triple3)]
("Dave" "is" "white" "-")
triple3
Dave is nice.
True
2
proof
[(((triple3) -> rule6))]
("Dave" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple3) -> rule6))]
("Dave" "is" "nice" "-")
((triple3) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Bob is furry.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule3))]
("Bob" "is" "furry" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Dave is not red.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule4))]
("Dave" "is" "red" "-")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Bob is white.
True
7
proof
[(((((triple2) -> rule4) ((((triple2) -> rule4) triple2) -> rule3)) -> rule2))]
("Bob" "is" "white" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not white.
False
7
inv-proof
[(((((triple2) -> rule4) ((((triple2) -> rule4) triple2) -> rule3)) -> rule2))]
("Bob" "is" "white" "-")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Anne is not red.
Unknown
inv-rconc
[@3: Anne is red.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule2 <- FAIL)]]
("Anne" "is" "red" "-")
Anne is white.
Unknown
rconc
[@3: Anne is white.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule1 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not nice.
Unknown
inv-rconc
[@4: Anne is nice.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule6 <- rule2 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is furry.
Unknown
rconc
[@3: Anne is furry.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule2 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Anne is smart.[(triple1)] Bob is nice.[(triple2)] Dave is white.[(triple3)] Harry is white.[(triple4)] @1: Bob is red.[(((triple2) -> rule4))] Dave is nice.[(((triple3) -> rule6))] Harry is nice.[(((triple4) -> rule6))] @2: Bob is furry.[(((((triple2) -> rule4) triple2) -> rule3))] Dave is red.[(((((triple3) -> rule6)) -> rule4))] Harry is red.[(((((triple4) -> rule6)) -> rule4))] @3: Bob is white.[(((((triple2) -> rule4) ((((triple2) -> rule4) triple2) -> rule3)) -> rule2))] Dave is furry.[(((((((triple3) -> rule6)) -> rule4) ((triple3) -> rule6)) -> rule3))] Harry is furry.[(((((((triple4) -> rule6)) -> rule4) ((triple4) -> rule6)) -> rule3))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple4) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple3) -> (rule6 % int3))) -> (rule4 % int2)) ((triple3) -> (rule6 % int3))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2)) ((triple4) -> (rule6 % int3))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3