Charlie is quiet. Erin is white. Fiona is green. Green things are kind. All big things are kind. If something is white and furry then it is big. White, big things are green. If Charlie is big then Charlie is furry. Big things are kind. If something is white and furry then it is big. If something is big then it is white.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
All big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is white and furry then it is big.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
White, big things are green.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If Charlie is big then Charlie is furry.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "furry" "+"))
Big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is white and furry then it is big.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Erin is white.
True
1
proof
[(triple2)]
("Erin" "is" "white" "+")
triple2
Erin is not white.
False
1
inv-proof
[(triple2)]
("Erin" "is" "white" "-")
triple2
Fiona is kind.
True
2
proof
[(((triple3) -> rule1))]
("Fiona" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not kind.
False
2
inv-proof
[(((triple3) -> rule1))]
("Fiona" "is" "kind" "-")
((triple3) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "big" "-")
Charlie is kind.
Unknown
rconc
[@4: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule8 <- rule3 <- FAIL)]]
("Charlie" "is" "kind" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Charlie is quiet.[(triple1)] Erin is white.[(triple2)] Fiona is green.[(triple3)] @1: Fiona is kind.[(((triple3) -> rule1))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1