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