Anne is cold. Anne is furry. Anne is red. Charlie is big. Charlie is blue. Charlie is cold. Charlie is red. Charlie is white. Charlie is young. Harry is young. All furry, cold things are white. If something is white then it is young. If something is young then it is big. White things are blue. White, furry things are blue. White, blue things are cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is young.
("Harry" "is" "young" "+")
All furry, cold things are white.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is white then it is young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is young then it is big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
White things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
White, furry things are blue.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
White, blue things are cold.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Anne is furry.
True
1
proof
[(triple2)]
("Anne" "is" "furry" "+")
triple2
Anne is not red.
False
1
inv-proof
[(triple3)]
("Anne" "is" "red" "-")
triple3
Anne is white.
True
3
proof
[(((triple2 triple1) -> rule1))]
("Anne" "is" "white" "+")
((triple2 triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
3
inv-proof
[(((triple2 triple1) -> rule1))]
("Anne" "is" "white" "-")
((triple2 triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
True
4
proof
[(((((triple2 triple1) -> rule1)) -> rule2))]
("Anne" "is" "young" "+")
((((triple2 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not young.
False
4
inv-proof
[(((((triple2 triple1) -> rule1)) -> rule2))]
("Anne" "is" "young" "-")
((((triple2 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is big.
True
5
proof
[(((((((triple2 triple1) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "big" "+")
((((((triple2 triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not big.
False
5
inv-proof
[(((((((triple2 triple1) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "big" "-")
((((((triple2 triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is blue.
Unknown
rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Harry" "is" "blue" "+")
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2)] Anne is red.[(triple3)] Charlie is big.[(triple4 OR ((triple9) -> rule3) OR ((((triple8) -> rule2)) -> rule3))] Charlie is blue.[(triple5 OR ((triple8) -> rule4))] Charlie is cold.[(triple6 OR ((triple8 triple5) -> rule6) OR ((triple8 ((triple8) -> rule4)) -> rule6))] Charlie is red.[(triple7)] Charlie is white.[(triple8)] Charlie is young.[(triple9 OR ((triple8) -> rule2))] Harry is young.[(triple10)] @1: Anne is white.[(((triple2 triple1) -> rule1))] Harry is big.[(((triple10) -> rule3))] @2: Anne is blue.[(((((triple2 triple1) -> rule1)) -> rule4) OR ((((triple2 triple1) -> rule1) triple2) -> rule5))] Anne is young.[(((((triple2 triple1) -> rule1)) -> rule2))] @3: Anne is big.[(((((((triple2 triple1) -> rule1)) -> rule2)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
((triple9) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
((triple8) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
((triple8 triple5) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple8 ((triple8) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
triple8
Charlie is young.
("Charlie" "is" "young" "+")
triple9
((triple8) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple10
Anne is white.
("Anne" "is" "white" "+")
((triple2 triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple10) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple2 triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple2 triple1) -> (rule1 % int2)) triple2) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple2 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((((((triple2 triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3