Charlie is not white. Fiona is big. Harry is not furry. If Charlie is not white then Charlie is big. If Fiona is white and Fiona is not green then Fiona is big. White, furry things are cold.
Charlie is not white.
("Charlie" "is" "white" "-")
Fiona is big.
("Fiona" "is" "big" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
If Charlie is not white then Charlie is big.
((("Charlie" "is" "white" "~")) -> ("Charlie" "is" "big" "+"))
If Fiona is white and Fiona is not green then Fiona is big.
((("Fiona" "is" "white" "+") ("Fiona" "is" "green" "~")) -> ("Fiona" "is" "big" "+"))
White, furry things are cold.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Charlie is not white.
True
1
proof
[(triple1)]
("Charlie" "is" "white" "-")
triple1
Charlie is white.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "white" "+")
triple1
Charlie is big.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "big" "+")
((triple1) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "big" "-")
((triple1) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "cold" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "cold" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Charlie is not white.[(triple1)] Fiona is big.[(triple2)] Harry is not furry.[(triple3)] @1: Charlie is big.[(((triple1) -> rule1))]
Charlie is not white.
("Charlie" "is" "white" "-")
triple1
Fiona is big.
("Fiona" "is" "big" "+")
triple2
Harry is not furry.
("Harry" "is" "furry" "-")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1