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