Anne is green. Anne is kind. Charlie is furry. Charlie is white. Gary is big. Gary is not cold. Gary is not kind. Harry is big. Harry is not cold. Harry is not green. Green people are kind. All blue people are green. Blue people are green. Green people are blue. All kind people are not white. If someone is green and not big then they are furry. If Harry is kind then Harry is green. If someone is kind and not white then they are cold.
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is not kind.
("Gary" "is" "kind" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is not green.
("Harry" "is" "green" "-")
Green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
All kind people are not white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "-"))
If someone is green and not big then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "furry" "+"))
If Harry is kind then Harry is green.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "green" "+"))
If someone is kind and not white then they are cold.
((("someone" "is" "kind" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "cold" "+"))
Gary is big.
True
1
proof
[(triple5)]
("Gary" "is" "big" "+")
triple5
Gary is cold.
False
1
inv-proof
[(triple6)]
("Gary" "is" "cold" "+")
triple6
Anne is not white.
True
2
proof
[(((triple2) -> rule5) OR ((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "white" "-")
((triple2) -> (rule5 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is white.
False
2
inv-proof
[(((triple2) -> rule5) OR ((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "white" "+")
((triple2) -> (rule5 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is cold.
True
4
proof
[(((triple2 ((triple2) -> rule5)) -> rule8) OR ((((triple1) -> rule1) ((triple2) -> rule5)) -> rule8) OR ((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule8) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule5)) -> rule8))]
("Anne" "is" "cold" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
((((triple1) -> (rule1 % int3)) ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((triple2 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is not cold.
False
4
inv-proof
[(((triple2 ((triple2) -> rule5)) -> rule8) OR ((((triple1) -> rule1) ((triple2) -> rule5)) -> rule8) OR ((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule8) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule5)) -> rule8))]
("Anne" "is" "cold" "-")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
((((triple1) -> (rule1 % int3)) ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((triple2 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "furry" "-")
Charlie is kind.
Unknown
rconc
[@4: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule4 <- rule3 <- FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not blue.
Unknown
inv-rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Anne is green.[(triple1)] Anne is kind.[(triple2 OR ((triple1) -> rule1))] Charlie is furry.[(triple3)] Charlie is white.[(triple4)] Gary is big.[(triple5)] Gary is not cold.[(triple6)] Gary is not kind.[(triple7)] Harry is big.[(triple8)] Harry is not cold.[(triple9)] Harry is not green.[(triple10)] @1: Anne is blue.[(((triple1) -> rule4))] Anne is not white.[(((triple2) -> rule5) OR ((((triple1) -> rule1)) -> rule5))] @2: Anne is cold.[(((triple2 ((triple2) -> rule5)) -> rule8) OR ((((triple1) -> rule1) ((triple2) -> rule5)) -> rule8) OR ((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule8) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule5)) -> rule8))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is not cold.
("Gary" "is" "cold" "-")
triple6
Gary is not kind.
("Gary" "is" "kind" "-")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is not cold.
("Harry" "is" "cold" "-")
triple9
Harry is not green.
("Harry" "is" "green" "-")
triple10
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
((triple2) -> (rule5 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
((((triple1) -> (rule1 % int3)) ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((triple2 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3