Bob is blue. Bob is cold. Bob is furry. Bob is kind. Bob is nice. Bob is red. Dave is blue. Dave is white. Erin is cold. Erin is nice. Erin is red. Harry is blue. Harry is furry. Harry is kind. Harry is nice. Harry is white. If Erin is red then Erin is kind. If something is cold and kind then it is furry. Red things are cold. If Dave is blue then Dave is cold. Blue, white things are nice. All furry, red things are cold. If Harry is cold then Harry is nice. If something is furry then it is white.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
If Erin is red then Erin is kind.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "kind" "+"))
If something is cold and kind then it is furry.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If Dave is blue then Dave is cold.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "cold" "+"))
Blue, white things are nice.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
All furry, red things are cold.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If Harry is cold then Harry is nice.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "nice" "+"))
If something is furry then it is white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Erin is nice.
True
1
proof
[(triple10)]
("Erin" "is" "nice" "+")
triple10
Erin is not cold.
False
1
inv-proof
[(triple9 OR ((triple11) -> rule3))]
("Erin" "is" "cold" "-")
triple9
((triple11) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Bob is white.
True
2
proof
[(((triple3) -> rule8) OR ((((triple2 triple4) -> rule2)) -> rule8) OR ((((((triple6) -> rule3) triple4) -> rule2)) -> rule8))]
("Bob" "is" "white" "+")
((triple3) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple2 triple4) -> (rule2 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple6) -> (rule3 % int3)) triple4) -> (rule2 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not white.
False
2
inv-proof
[(((triple3) -> rule8) OR ((((triple2 triple4) -> rule2)) -> rule8) OR ((((((triple6) -> rule3) triple4) -> rule2)) -> rule8))]
("Bob" "is" "white" "-")
((triple3) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple2 triple4) -> (rule2 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple6) -> (rule3 % int3)) triple4) -> (rule2 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Erin is furry.
True
4
proof
[(((triple9 ((triple11) -> rule1)) -> rule2) OR ((((triple11) -> rule3) ((triple11) -> rule1)) -> rule2))]
("Erin" "is" "furry" "+")
((triple9 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple11) -> (rule3 % int3)) ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not furry.
False
4
inv-proof
[(((triple9 ((triple11) -> rule1)) -> rule2) OR ((((triple11) -> rule3) ((triple11) -> rule1)) -> rule2))]
("Erin" "is" "furry" "-")
((triple9 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple11) -> (rule3 % int3)) ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is white.
True
5
proof
[(((((triple9 ((triple11) -> rule1)) -> rule2)) -> rule8) OR ((((((triple11) -> rule3) ((triple11) -> rule1)) -> rule2)) -> rule8))]
("Erin" "is" "white" "+")
((((triple9 ((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple11) -> (rule3 % int4)) ((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is not white.
False
5
inv-proof
[(((((triple9 ((triple11) -> rule1)) -> rule2)) -> rule8) OR ((((((triple11) -> rule3) ((triple11) -> rule1)) -> rule2)) -> rule8))]
("Erin" "is" "white" "-")
((((triple9 ((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple11) -> (rule3 % int4)) ((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "furry" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "cold" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2 OR ((triple6) -> rule3) OR ((triple3 triple6) -> rule6))] Bob is furry.[(triple3 OR ((triple2 triple4) -> rule2) OR ((((triple6) -> rule3) triple4) -> rule2))] Bob is kind.[(triple4)] Bob is nice.[(triple5 OR ((triple1 ((triple3) -> rule8)) -> rule5) OR ((triple1 ((((triple2 triple4) -> rule2)) -> rule8)) -> rule5) OR ((triple1 ((((((triple6) -> rule3) triple4) -> rule2)) -> rule8)) -> rule5))] Bob is red.[(triple6)] Dave is blue.[(triple7)] Dave is white.[(triple8)] Erin is cold.[(triple9 OR ((triple11) -> rule3))] Erin is nice.[(triple10)] Erin is red.[(triple11)] Harry is blue.[(triple12)] Harry is furry.[(triple13)] Harry is kind.[(triple14)] Harry is nice.[(triple15 OR ((triple12 triple16) -> rule5) OR ((triple12 ((triple13) -> rule8)) -> rule5))] Harry is white.[(triple16 OR ((triple13) -> rule8))] @1: Bob is white.[(((triple3) -> rule8) OR ((((triple2 triple4) -> rule2)) -> rule8) OR ((((((triple6) -> rule3) triple4) -> rule2)) -> rule8))] Dave is cold.[(((triple7) -> rule4))] Dave is nice.[(((triple7 triple8) -> rule5))] Erin is kind.[(((triple11) -> rule1))] @2: Erin is furry.[(((triple9 ((triple11) -> rule1)) -> rule2) OR ((((triple11) -> rule3) ((triple11) -> rule1)) -> rule2))] @3: Erin is white.[(((((triple9 ((triple11) -> rule1)) -> rule2)) -> rule8) OR ((((((triple11) -> rule3) ((triple11) -> rule1)) -> rule2)) -> rule8))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple6) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple3 triple6) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple2 triple4) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple6) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
triple5
((triple1 ((triple3) -> (rule8 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((triple1 ((((triple2 triple4) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((triple1 ((((((triple6) -> (rule3 % int4)) triple4) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
triple6
Dave is blue.
("Dave" "is" "blue" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
triple8
Erin is cold.
("Erin" "is" "cold" "+")
triple9
((triple11) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Erin is red.
("Erin" "is" "red" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is nice.
("Harry" "is" "nice" "+")
triple15
((triple12 triple16) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple12 ((triple13) -> (rule8 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
triple16
((triple13) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple3) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple2 triple4) -> (rule2 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple6) -> (rule3 % int3)) triple4) -> (rule2 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((triple7) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple7 triple8) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple11) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple9 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple11) -> (rule3 % int3)) ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((((triple9 ((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple11) -> (rule3 % int4)) ((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4