Charlie is young. Erin is white. Fiona is furry. All young people are kind. If someone is kind then they are white. Kind, young people are white. If Fiona is young then Fiona is not white. If someone is white then they are not quiet. If someone is furry and quiet then they are cold. If someone is kind and young then they are not cold. If someone is big and not quiet then they are not furry.
Charlie is young.
("Charlie" "is" "young" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
All young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind then they are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Kind, young people are white.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If Fiona is young then Fiona is not white.
((("Fiona" "is" "young" "+")) -> ("Fiona" "is" "white" "-"))
If someone is white then they are not quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "-"))
If someone is furry and quiet then they are cold.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is kind and young then they are not cold.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "-"))
If someone is big and not quiet then they are not furry.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "furry" "-"))
Charlie is young.
True
1
proof
[(triple1)]
("Charlie" "is" "young" "+")
triple1
Erin is not white.
False
1
inv-proof
[(triple2)]
("Erin" "is" "white" "-")
triple2
Erin is not quiet.
True
2
proof
[(((triple2) -> rule5))]
("Erin" "is" "quiet" "-")
((triple2) -> (rule5 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "kind" "-")
((triple1) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not cold.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule7))]
("Charlie" "is" "cold" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule7 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2) OR ((((triple1) -> rule1) triple1) -> rule3))]
("Charlie" "is" "white" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not quiet.
True
4
proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule5) OR ((((((triple1) -> rule1) triple1) -> rule3)) -> rule5))]
("Charlie" "is" "quiet" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple1) -> (rule1 % int3)) triple1) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is quiet.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule5) OR ((((((triple1) -> rule1) triple1) -> rule3)) -> rule5))]
("Charlie" "is" "quiet" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple1) -> (rule1 % int3)) triple1) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is white.
Unknown
rconc
[@2: Fiona is white.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "cold" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "kind" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Charlie is young.[(triple1)] Erin is white.[(triple2)] Fiona is furry.[(triple3)] @1: Charlie is kind.[(((triple1) -> rule1))] Erin is not quiet.[(((triple2) -> rule5))] @2: Charlie is not cold.[(((((triple1) -> rule1) triple1) -> rule7))] Charlie is white.[(((((triple1) -> rule1)) -> rule2) OR ((((triple1) -> rule1) triple1) -> rule3))] @3: Charlie is not quiet.[(((((((triple1) -> rule1)) -> rule2)) -> rule5) OR ((((((triple1) -> rule1) triple1) -> rule3)) -> rule5))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is not quiet.
("Erin" "is" "quiet" "-")
((triple2) -> (rule5 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Charlie is not cold.
("Charlie" "is" "cold" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule7 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple1) -> (rule1 % int3)) triple1) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3